diff options
| author |  peter mueller peter.mueller@inf.ethz.ch <unknown> | 2011-09-29 19:32:48 +0200 |
|---|---|---|
| committer | peter mueller peter.mueller@inf.ethz.ch <unknown> | 2011-09-29 19:32:48 +0200 |
| commit | 899d1f3d30abf3343b88c0e4c6e44db130c6345b (patch) | |
| tree | f72624898d89e5f8a3a6acf2ee3f9c544e8b00bd /Test/dafny2 | |
| parent | 0a8e7489a6a95495b8a36b4d46b747745f663318 (diff) | |
Dafny: Added TreeBarrier as a test case
Diffstat (limited to 'Test/dafny2')
| -rw-r--r-- | Test/dafny2/Answer | 6 | ||||
| -rw-r--r-- | Test/dafny2/TreeBarrier.dfy | 143 | ||||
| -rw-r--r-- | Test/dafny2/runtest.bat | 2 |
3 files changed, 150 insertions, 1 deletions
diff --git a/Test/dafny2/Answer b/Test/dafny2/Answer index 3eb32da8..bef70cf1 100644 --- a/Test/dafny2/Answer +++ b/Test/dafny2/Answer @@ -1,4 +1,10 @@ -------------------- SnapshotableTrees.dfy --------------------
+Dafny program verifier version 2.2.30705.1126, Copyright (c) 2003-2011, Microsoft.
Dafny program verifier finished with 37 verified, 0 errors
+
+-------------------- TreeBarrier.dfy --------------------
+Dafny program verifier version 2.2.30705.1126, Copyright (c) 2003-2011, Microsoft.
+
+Dafny program verifier finished with 8 verified, 0 errors
diff --git a/Test/dafny2/TreeBarrier.dfy b/Test/dafny2/TreeBarrier.dfy new file mode 100644 index 00000000..f4cc25d2 --- /dev/null +++ b/Test/dafny2/TreeBarrier.dfy @@ -0,0 +1,143 @@ +class Node {
+ var left: Node;
+ var right: Node;
+ var parent: Node;
+ var anc: set<Node>;
+ var desc: set<Node>;
+ var sense: bool;
+ var pc: int;
+
+
+ function validDown(): bool
+ reads this, desc;
+ {
+ this !in desc &&
+ null !in desc &&
+ left != right && // not needed, but speeds up verification
+
+ (right != null ==> right in desc && left !in right.desc) &&
+
+ (left != null ==>
+ left in desc &&
+ (right != null ==> desc == {left,right} + left.desc + right.desc) &&
+ (right == null ==> desc == {left} + left.desc) &&
+ left.validDown()) &&
+ (left == null ==>
+ (right != null ==> desc == {right} + right.desc) &&
+ (right == null ==> desc == {})) &&
+
+ (right != null ==> right.validDown()) &&
+
+ (blocked() ==> forall m :: m in desc ==> m.blocked()) &&
+ (after() ==> forall m :: m in desc ==> m.blocked() || m.after())
+// (left != null && right != null ==> left.desc !! right.desc) // not needed
+ }
+
+
+
+
+ function validUp(): bool
+ reads this, anc;
+ {
+ this !in anc &&
+ null !in anc &&
+ (parent != null ==> parent in anc && anc == { parent } + parent.anc && parent.validUp()) &&
+ (parent == null ==> anc == {}) &&
+ (after() ==> forall m :: m in anc ==> m.after())
+ }
+
+ function valid(): bool
+ reads this, desc, anc;
+ { validUp() && validDown() && desc !! anc }
+
+ function before(): bool
+ reads this;
+ { !sense && pc <= 2 }
+
+ function blocked(): bool
+ reads this;
+ { sense }
+
+ function after(): bool
+ reads this;
+ { !sense && 3 <= pc }
+
+
+ method barrier()
+ requires valid();
+ requires before();
+ modifies this, left, right;
+ {
+
+//A
+ pc := 1;
+ if(left != null) {
+ while(!left.sense)
+ modifies left;
+ invariant validDown(); // this seems necessary to get the necessary unfolding of functions
+ invariant valid();
+ decreases *; // to by-pass termination checking for this loop
+ {
+ // this loop body is supposed to model what the "left" thread
+ // might do to its node. This body models a transition from
+ // "before" to "blocked" by setting sense to true. A transition
+ // all the way to "after" is not permitted; this would require
+ // a change of pc.
+ // We assume that "left" preserves the validity of its subtree,
+ // which means in particular that it goes to "blocked" only if
+ // all its descendants are already blocked.
+ left.sense := *;
+ assume left.blocked() ==> forall m :: m in left.desc ==> m.blocked();
+ }
+ }
+ if(right != null) {
+ while(!right.sense)
+ modifies right;
+ invariant validDown(); // this seems necessary to get the necessary unfolding of functions
+ invariant valid();
+ decreases *; // to by-pass termination checking for this loop
+ {
+ // analogous to the previous loop
+ right.sense := *;
+ assume right.blocked() ==> forall m :: m in right.desc ==> m.blocked();
+ }
+ }
+
+//B
+ pc := 2;
+ if(parent != null) {
+ sense := true;
+ }
+//C
+ pc := 3;
+ while(sense)
+ modifies this;
+ invariant validUp(); // this seems necessary to get the necessary unfolding of functions
+ invariant valid();
+ invariant left == old(left);
+ invariant right == old(right);
+ invariant sense ==> parent != null;
+ decreases *; // to by-pass termination checking for this loop
+ {
+ // this loop body is supposed to model what the "parent" thread
+ // might do to its node. The body models a transition from
+ // "blocked" to "after" by setting sense to false.
+ // We assume that "parent" initiates this transition only
+ // after it went to state "after" itself.
+ sense := *;
+ assume !sense ==> parent.after();
+ }
+//D
+ pc := 4;
+ if(left != null) {
+ left.sense := false;
+ }
+//E
+ pc := 5;
+ if(right != null) {
+ right.sense := false;
+ }
+//F
+ pc := 6;
+ }
+}
diff --git a/Test/dafny2/runtest.bat b/Test/dafny2/runtest.bat index a58b03c6..62b0b6fe 100644 --- a/Test/dafny2/runtest.bat +++ b/Test/dafny2/runtest.bat @@ -5,7 +5,7 @@ set BOOGIEDIR=..\..\Binaries set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
set CSC=c:/Windows/Microsoft.NET/Framework/v4.0.30319/csc.exe
-for %%f in (SnapshotableTrees.dfy) do (
+for %%f in (SnapshotableTrees.dfy TreeBarrier.dfy) do (
echo.
echo -------------------- %%f --------------------
|