-
Notifications
You must be signed in to change notification settings - Fork 26
/
predicate.gobra
45 lines (37 loc) · 1.13 KB
/
predicate.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
// Any copyright is dedicated to the Public Domain.
// http://creativecommons.org/publicdomain/zero/1.0/
package tutorial
type node struct {
value int
next *node
}
pred list(ptr *node) {
acc(&ptr.value) && acc(&ptr.next) && (ptr.next != nil ==> list(ptr.next))
}
requires list(ptr)
ensures list(ptr)
func testPredFail(ptr * node) {
assert list(ptr) // succeeds
// assert acc(&ptr.value) && acc(&ptr.next) // fails if uncommented
}
requires list(ptr)
ensures list(ptr)
func testPred(ptr * node) {
assert list(ptr)
unfold list(ptr) // exchanges list(ptr) with its body
assert acc(&ptr.value) && acc(&ptr.next) // succeeds
fold list(ptr)
}
requires list(ptr)
pure func head(ptr *node) int {
return unfolding list(ptr) in ptr.value
}
requires p > 0
requires acc(list(ptr), p)
pure func (ptr *node) contains(value int, ghost p perm) bool {
return unfolding acc(list(ptr), p) in ptr.value == value || (ptr.next != nil && ptr.next.contains(value, p))
}
requires acc(list(ptr), _)
pure func (ptr *node) contains2(value int) bool {
return unfolding acc(list(ptr), _) in ptr.value == value || (ptr.next != nil && ptr.next.contains2(value))
}