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
115
116
117
118
|
// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
class List<T> {
ghost var Contents: seq<T>;
ghost var Repr: set<object>;
var a: array<T>;
var n: nat;
predicate Valid()
reads this, Repr;
{
this in Repr && null !in Repr &&
a in Repr &&
n <= a.Length != 0 &&
Contents == a[..n]
}
constructor Init()
modifies this;
ensures Valid() && fresh(Repr - {this});
ensures Contents == [];
{
Contents, Repr, n := [], {this}, 0;
a := new T[25];
Repr := Repr + {a};
}
method Add(t: T)
requires Valid();
modifies Repr;
ensures Valid() && fresh(Repr - old(Repr));
ensures Contents == old(Contents) + [t];
{
if (n == a.Length) {
var b := new T[2 * a.Length];
forall i | 0 <= i < a.Length {
b[i] := a[i];
}
assert b[..n] == a[..n] == Contents;
a, Repr := b, Repr + {b};
assert b[..n] == Contents;
}
a[n], n, Contents := t, n + 1, Contents + [t];
}
}
class Cell { var data: int; }
iterator M<T>(l: List<T>, c: Cell) yields (x: T)
requires l != null && l.Valid() && c != null;
reads l.Repr;
modifies c;
yield requires true;
yield ensures xs <= l.Contents; // this is needed in order for the next line to be well-formed
yield ensures x == l.Contents[|xs|-1];
ensures xs == l.Contents;
{
var i := 0;
while (i < l.n)
invariant i <= l.n && i == |xs| && xs <= l.Contents;
{
if (*) { assert l.Valid(); } // this property is maintained, due to the reads clause
if (*) {
x := l.a[i]; yield; // or, equivalently, 'yield l.a[i]'
i := i + 1;
} else {
x, i := l.a[i], i + 1;
yield;
}
}
}
method Client<T(==)>(l: List, stop: T) returns (s: seq<T>)
requires l != null && l.Valid();
{
var c := new Cell;
var iter := new M(l, c);
s := [];
while (true)
invariant iter.Valid() && fresh(iter._new);
invariant iter.xs <= l.Contents;
decreases |l.Contents| - |iter.xs|;
{
var more := iter.MoveNext();
if (!more) { break; }
s := s + [iter.x];
if (iter.x == stop) { return; } // if we ever see 'stop', then just end
}
}
method PrintSequence<T>(s: seq<T>)
{
var i := 0;
while (i < |s|)
{
print s[i], " ";
i := i + 1;
}
print "\n";
}
method Main()
{
var myList := new List.Init();
var i := 0;
while (i < 100)
invariant myList.Valid() && fresh(myList.Repr);
{
myList.Add(i);
i := i + 2;
}
var s := Client(myList, 89);
PrintSequence(s);
s := Client(myList, 14);
PrintSequence(s);
}
|
