blob: 4c3b095a6ecf9c8f9faa46a392a6c6e37b863a14 (
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
|
class UnboundedStack<T> {
ghost var representation: set<object>;
ghost var content: seq<T>;
var top: Node<T>;
function IsUnboundedStack(): bool
reads this, representation;
{
this in representation &&
(top == null ==>
content == []) &&
(top != null ==>
top in representation && this !in top.footprint && top.footprint <= representation &&
content == top.content &&
top.Valid())
}
method InitUnboundedStack()
modifies this;
ensures IsUnboundedStack();
ensures content == [];
{
this.top := null;
this.content := [];
this.representation := {this};
}
method Push(val: T)
requires IsUnboundedStack();
modifies this;
ensures IsUnboundedStack();
ensures content == [val] + old(content);
{
var tmp := new Node<T>;
call tmp.InitNode(val,top);
top := tmp;
representation := representation + top.footprint;
content := [val] + content;
}
method Pop() returns (result: T)
requires IsUnboundedStack();
requires content != [];
modifies this;
ensures IsUnboundedStack();
ensures content == old(content)[1..];
{
result := top.val;
top := top.next;
content := content[1..];
}
method isEmpty() returns (result: bool)
requires IsUnboundedStack();
ensures result <==> content == [];
{
result := top == null;
}
}
class Node<T> {
ghost var footprint: set<object>;
ghost var content: seq<T>;
var val: T;
var next: Node<T>;
function Valid(): bool
reads this, footprint;
{
this in footprint &&
(next == null ==>
content == [val]) &&
(next != null ==>
next in footprint && next.footprint <= footprint && this !in next.footprint &&
content == [val] + next.content &&
next.Valid())
}
method InitNode(val: T, next: Node<T>)
requires next != null ==> next.Valid() && !(this in next.footprint);
modifies this;
ensures Valid();
ensures next != null ==> content == [val] + next.content &&
footprint == {this} + next.footprint;
ensures next == null ==> content == [val] &&
footprint == {this};
{
this.val := val;
this.next := next;
if (next == null) {
this.footprint := {this};
this.content := [val];
} else {
this.footprint := {this} + next.footprint;
this.content := [val] + next.content;
}
}
}
|
