-
Notifications
You must be signed in to change notification settings - Fork 26
/
interfaces.gobra
56 lines (45 loc) · 1.03 KB
/
interfaces.gobra
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
// Any copyright is dedicated to the Public Domain.
// http://creativecommons.org/publicdomain/zero/1.0/
package tutorial
type stream interface {
pred mem()
requires acc(mem(), 1/2)
pure hasNext() bool
requires mem() && hasNext()
ensures mem()
next() interface{}
}
// implementation
type counter struct{ f, max int }
requires acc(x, 1/2)
pure func (x *counter) hasNext() bool {
return x.f < x.max
}
requires acc(&x.f) && acc(&x.max, 1/2)
requires x.hasNext()
ensures acc(&x.f) && acc(&x.max, 1/2) && x.f == old(x.f)+1
ensures typeOf(y) == type[int] && y.(int) == old(x.f)
func (x *counter) next() (y interface{}) {
y = x.f
x.f += 1
return
}
// implementation proof
pred (x *counter) mem() { acc(x) }
(*counter) implements stream {
pure (x *counter) hasNext() bool {
return unfolding acc(x.mem(), 1/2) in x.hasNext()
}
(x *counter) next() (res interface{}) {
unfold x.mem()
res = x.next()
fold x.mem()
}
}
// client code
func client() {
x := &counter{0, 50}
var y stream = x
fold y.mem()
var z interface{} = y.next()
}