diff options
| author |  rustanleino <unknown> | 2010-06-08 18:05:23 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2010-06-08 18:05:23 +0000 |
| commit | 2e8f477b81b1c5c6d3c3f600abac3874548a9e4d (patch) | |
| tree | 03e89bdb4df3a689b7217c5e913557c5b6c6df99 /Test/dafny1/ListContents.dfy | |
| parent | 22e67dc18705c19b617678358c8e859349938ac3 (diff) | |
Boogie:
* Look for Z3 versions up to 2.15 (but did not implement a better algorithm for it).
* Added prover-path output as part of /trace flag (that probably isn't the best command-line option for it).
Dafny:
* Split off some tests from Test/dafny0 into Test/dafny1.
* Added Test/dafny1/UltraFilter.dfy.
Diffstat (limited to 'Test/dafny1/ListContents.dfy')
| -rw-r--r-- | Test/dafny1/ListContents.dfy | 93 |
1 files changed, 93 insertions, 0 deletions
diff --git a/Test/dafny1/ListContents.dfy b/Test/dafny1/ListContents.dfy new file mode 100644 index 00000000..62636ce5 --- /dev/null +++ b/Test/dafny1/ListContents.dfy @@ -0,0 +1,93 @@ +class Node<T> {
+ var list: seq<T>;
+ var footprint: set<Node<T>>;
+
+ var data: T;
+ var next: Node<T>;
+
+ function Valid(): bool
+ reads this, footprint;
+ {
+ this in this.footprint && null !in this.footprint &&
+ (next == null ==> list == [data]) &&
+ (next != null ==>
+ next in footprint && next.footprint <= footprint &&
+ this !in next.footprint &&
+ list == [data] + next.list &&
+ next.Valid())
+ }
+
+ method Init(d: T)
+ modifies this;
+ ensures Valid() && fresh(footprint - {this});
+ ensures list == [d];
+ {
+ data := d;
+ next := null;
+ list := [d];
+ footprint := {this};
+ }
+
+ method SkipHead() returns (r: Node<T>)
+ requires Valid();
+ ensures r == null ==> |list| == 1;
+ ensures r != null ==> r.Valid() && r.footprint <= footprint;
+ ensures r != null ==> r.list == list[1..];
+ {
+ r := next;
+ }
+
+ method Prepend(d: T) returns (r: Node<T>)
+ requires Valid();
+ ensures r != null && r.Valid() && fresh(r.footprint - old(footprint));
+ ensures r.list == [d] + list;
+ {
+ r := new Node<T>;
+ r.data := d;
+ r.next := this;
+ r.footprint := {r} + this.footprint;
+ r.list := [r.data] + this.list;
+ }
+
+ method ReverseInPlace() returns (reverse: Node<T>)
+ requires Valid();
+ modifies footprint;
+ ensures reverse != null && reverse.Valid();
+ ensures fresh(reverse.footprint - old(footprint));
+ ensures |reverse.list| == |old(list)|;
+ ensures (forall i :: 0 <= i && i < |old(list)| ==> old(list)[i] == reverse.list[|old(list)|-1-i]);
+ {
+ var current := next;
+ reverse := this;
+ reverse.next := null;
+ reverse.footprint := {reverse};
+ reverse.list := [data];
+
+ while (current != null)
+ invariant reverse != null && reverse.Valid();
+ invariant reverse.footprint <= old(footprint);
+ invariant current == null ==> |old(list)| == |reverse.list|;
+ invariant current != null ==>
+ current.Valid() &&
+ current in old(footprint) && current.footprint <= old(footprint) &&
+ current.footprint !! reverse.footprint &&
+ |old(list)| == |reverse.list| + |current.list| &&
+ (forall i :: 0 <= i && i < |current.list| ==> current.list[i] == old(list)[|reverse.list|+i]);
+ invariant
+ (forall i :: 0 <= i && i < |reverse.list| ==> old(list)[i] == reverse.list[|reverse.list|-1-i]);
+ decreases if current != null then |current.list| else -1;
+ {
+ var nx := current.next;
+ assert nx != null ==> (forall i :: 0 <= i && i < |nx.list| ==> current.list[1+i] == nx.list[i]); // lemma
+
+ // ..., reverse, current, nx, ...
+ assert current.data == current.list[0]; // lemma
+ current.next := reverse;
+ current.footprint := {current} + reverse.footprint;
+ current.list := [current.data] + reverse.list;
+
+ reverse := current;
+ current := nx;
+ }
+ }
+}
|