diff options
| author |  Rustan Leino <leino@microsoft.com> | 2012-10-04 18:58:20 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2012-10-04 18:58:20 -0700 |
| commit | a4af24114ae44ee34246fdc8bd16ce05d5518c20 (patch) | |
| tree | 1056d4375d6554ec8b0792ab76a59138956dd50a /Test/dafny3/Iter.dfy | |
| parent | 0a76a9953bd35663e20cc197ae5247a25cadc4bd (diff) | |
Added Test/dafny3 and another test file for iterators (hey, you can even run Iter.dfy!)
Fixed migration issues
Diffstat (limited to 'Test/dafny3/Iter.dfy')
| -rw-r--r-- | Test/dafny3/Iter.dfy | 115 |
1 files changed, 115 insertions, 0 deletions
diff --git a/Test/dafny3/Iter.dfy b/Test/dafny3/Iter.dfy new file mode 100644 index 00000000..543a889a --- /dev/null +++ b/Test/dafny3/Iter.dfy @@ -0,0 +1,115 @@ +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];
+ parallel (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.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);
+}
|