blob: 8afbff5cee069ea69334281b0a27b1db089773f2 (
plain)
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
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
|
/* Recursive implementation and specification of a linked list. */
class Node {
var next: Node;
var value: int;
predicate valid {
rd*(next) && rd*(value) && (next!=null ==> next.valid)
}
method testNestingUnfold()
requires acc(this.valid)
{
unfold this.valid;
assert this != this.next;
if(this.next != null) {
unfold this.next.valid;
assert this.next != this.next.next;
assert this != this.next.next;
}
}
method testNestingFold() // this test shows that we build in the assumption that predicate instances with infinite expansions cannot be exist (in reachable code)
requires rd*(this.next) && rd*(this.value) && rd*(this.next.next) && rd*(this.next.value) && this.next != null && this.next.next != null && this.next.next.valid
{
fold this.next.valid;
assert this.next != this.next.next; // definition of valid "proves" that this.next and this.next.next cannot be aliases
fold this.valid;
assert this != this.next;
assert this != this.next.next;
}
method testNestingUnfolding()
requires acc(this.valid)
{
assert this != (unfolding this.valid in this.next);
if((unfolding this.valid in this.next) != null) {
assert (unfolding this.valid in this.next) != (unfolding this.valid in (unfolding this.next.valid in this.next.next));
assert this != (unfolding this.valid in (unfolding this.next.valid in this.next.next));
}
}
predicate p {
rd*(next) && rd*(value) && (next!=null ==> next.q)
}
predicate q {
rd*(next) && rd*(value) && (next!=null ==> next.p)
}
method testNestingUnfoldTwo()
requires acc(this.p)
{
unfold this.p;
assert this != this.next; // should fail
if(this.next != null) {
unfold this.next.q;
assert this.next != this.next.next; // should fail
assert this != this.next.next; // should succeed
}
}
method testNestingFoldTwo() // this test shows that we build in the assumption that predicate instances with infinite expansions cannot be exist (in reachable code)
requires rd*(this.next) && rd*(this.value) && rd*(this.next.next) && rd*(this.next.value) && this.next != null && this.next.next != null && this.next.next.p
{
fold this.next.q;
assert this != this.next; // should fail
assert this.next != this.next.next; // should fail
assert this != this.next.next; // should fail
}
method testNestingFoldThree() // this test shows that we build in the assumption that predicate instances with infinite expansions cannot be exist (in reachable code)
requires rd*(this.next) && rd*(this.value) && rd*(this.next.next) && rd*(this.next.value) && this.next != null && this.next.next != null && this.next.next.p
{
fold this.next.q;
fold this.p;
assert this != this.next; // should succeed, since this == this.next ==> this == this.next.next
assert this.next != this.next.next; // should fail - we haven't seen a cycle which would follow from this fact
assert this != this.next.next; // should succeed
}
method testNestingUnfoldingTwo()
requires acc(this.p)
{
assert this != (unfolding this.p in this.next); // should fail
if((unfolding this.p in this.next) != null) {
assert (unfolding this.p in this.next) != (unfolding this.p in (unfolding this.next.q in this.next.next)); // should fail
assert this != (unfolding this.p in (unfolding this.next.q in this.next.next)); // should succeed
}
}
method testNestingUnfoldingPrecondition(x: Node)
requires acc(this.valid) && (unfolding this.valid in this.next == x);
{
assert this != x;
}
function getNext() : Node
requires this.valid;
{
unfolding this.valid in this.next
}
method testNestingUnfoldingPostcondition(x: Node)
requires acc(this.valid);
ensures acc(this.valid) && (unfolding this.valid in true) && this != this.getNext()
{
// nothing
}
}
|
