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/UnboundedStack.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/UnboundedStack.dfy')
| -rw-r--r-- | Test/dafny1/UnboundedStack.dfy | 98 |
1 files changed, 98 insertions, 0 deletions
diff --git a/Test/dafny1/UnboundedStack.dfy b/Test/dafny1/UnboundedStack.dfy new file mode 100644 index 00000000..4c3b095a --- /dev/null +++ b/Test/dafny1/UnboundedStack.dfy @@ -0,0 +1,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;
+ }
+ }
+}
|