blob: 3e67db5883929e558a9ff0c46213c10f2afc09f2 (
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
|
class UnboundedStack<T> {
var top: Node<T>;
ghost var footprint: set<object>;
ghost var content: seq<T>;
function IsUnboundedStack(): bool
reads {this} + footprint;
{
this in footprint &&
(top == null ==> content == []) &&
(top != null ==> top in footprint && top.footprint <= footprint &&
top.prev == null && content == top.content && top.Valid())
}
function IsEmpty(): bool
reads {this};
{ content == [] }
method Pop() returns (result: T)
requires IsUnboundedStack() && !IsEmpty();
modifies footprint;
ensures IsUnboundedStack() && content == old(content)[1..];
{
result := top.val;
// The following assert does the trick, because it gets inlined and thus
// exposes top.next.Valid() (if top.next != null):
footprint := footprint - top.footprint; top := top.next;
// In a previous version of the implementation of the SplitExpr transformation, the
// following assert did not have the intended effect of being used as a lemma:
assert top != null ==> top.Valid();
if (top != null) {
footprint := footprint + top.footprint; top.prev := null;
}
content := content[1..];
} }
class Node<T> {
var val: T;
var next: Node<T>;
var prev: Node<T>;
var footprint: set<Node<T>>;
var content: seq<T>;
function Valid(): bool
reads this, footprint;
{
this in footprint && !(null in footprint) &&
(next == null ==> content == [val]) &&
(next != null ==> next in footprint &&
next.footprint < footprint &&
!(this in next.footprint) &&
next.prev == this &&
content == [val] + next.content &&
next.Valid())
}
}
// ---------------------------------------------------------------------------------------
// The following examples requires that quantifiers are boosted (that is, #2) when checked
// versus not boosted (#1) when assumed.
function F(x: nat): int
{
if x == 0 then 0 else 1 + F(x-1)
}
method M(N: nat)
{
var i := 0;
while (i < N)
invariant forall x {:induction false} :: 0 <= x <= i ==> F(x) == x;
{
i := i + 1;
}
}
|
