diff options
| author |  Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-08-09 16:48:36 -0700 |
|---|---|---|
| committer | Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-08-09 16:48:36 -0700 |
| commit | 1a108fbd3a2699702437c6cc0f98d68d1836bc9a (patch) | |
| tree | da9d523f95088c4aa90ee541e5e5823752252ce6 /Test/dafny2 | |
| parent | 3703abf436a8f863de74d7aa009d52fe8bf96dad (diff) | |
Dafny: added MonotonicHeapstate refinement example
Diffstat (limited to 'Test/dafny2')
| -rw-r--r-- | Test/dafny2/Answer | 4 | ||||
| -rw-r--r-- | Test/dafny2/MonotonicHeapstate.dfy | 143 | ||||
| -rw-r--r-- | Test/dafny2/runtest.bat | 1 |
3 files changed, 148 insertions, 0 deletions
diff --git a/Test/dafny2/Answer b/Test/dafny2/Answer index f466d813..447f4365 100644 --- a/Test/dafny2/Answer +++ b/Test/dafny2/Answer @@ -50,3 +50,7 @@ Dafny program verifier finished with 11 verified, 0 errors -------------------- SegmentSum.dfy --------------------
Dafny program verifier finished with 3 verified, 0 errors
+
+-------------------- MonotonicHeapstate.dfy --------------------
+
+Dafny program verifier finished with 36 verified, 0 errors
diff --git a/Test/dafny2/MonotonicHeapstate.dfy b/Test/dafny2/MonotonicHeapstate.dfy new file mode 100644 index 00000000..4844086e --- /dev/null +++ b/Test/dafny2/MonotonicHeapstate.dfy @@ -0,0 +1,143 @@ +module M0 {
+ datatype Kind = Constant | Ident | Binary;
+
+ class Expr {
+ var kind: Kind;
+ var value: int; // value if kind==Constant; id if kind==VarDecl; operator if kind==Binary
+ var left: Expr; // if kind==Binary
+ var right: Expr; // if kind==Binary
+
+ ghost var Repr: set<object>;
+
+ predicate Valid()
+ reads this, Repr;
+ {
+ this in Repr && null !in Repr &&
+ (left != null ==> left in Repr && this !in left.Repr && right !in left.Repr && left.Repr <= Repr && left.Valid()) &&
+ (right != null ==> right in Repr && this !in right.Repr && left !in right.Repr && right.Repr <= Repr && right.Valid()) &&
+ (kind == Binary ==> left != null && right != null && left.Repr !! right.Repr)
+ }
+
+ constructor CreateConstant(x: int)
+ modifies this;
+ ensures Valid() && fresh(Repr - {this});
+ {
+ kind, value := Constant, x;
+ left, right := null, null;
+ Repr := {this};
+ }
+
+ constructor CreateIdent(name: int)
+ modifies this;
+ ensures Valid() && fresh(Repr - {this});
+ {
+ kind, value := Ident, name;
+ left, right := null, null;
+ Repr := {this};
+ }
+
+ constructor CreateBinary(op: int, left: Expr, right: Expr)
+ requires left != null && left.Valid() && this !in left.Repr;
+ requires right != null && right.Valid() && this !in right.Repr;
+ requires left.Repr !! right.Repr;
+ modifies this;
+ ensures Valid() && fresh(Repr - {this} - left.Repr - right.Repr);
+ {
+ kind, value := Binary, op;
+ this.left, this.right := left, right;
+ Repr := {this} + left.Repr + right.Repr;
+ }
+ }
+}
+
+// Introduce the idea of resolved
+module M1 refines M0 {
+ class Expr {
+ ghost var resolved: bool;
+
+ predicate Valid()
+ {
+ resolved ==>
+ (kind == Binary ==> left.resolved && right.resolved)
+ }
+
+ constructor CreateConstant...
+ {
+ resolved := false;
+ }
+
+ constructor CreateIdent...
+ {
+ resolved := false;
+ }
+
+ constructor CreateBinary...
+ {
+ resolved := false;
+ }
+
+ method Resolve()
+ requires Valid(); // it's okay if it's already resolved
+ modifies Repr;
+ ensures Valid() && fresh(Repr - old(Repr));
+ ensures resolved;
+ decreases Repr;
+ {
+ if (kind == Binary) {
+ left.Resolve();
+ right.Resolve();
+ }
+ Repr := Repr + (if left != null then left.Repr else {}) + (if right != null then right.Repr else {});
+ resolved := true;
+ }
+ }
+}
+
+// Give "resolved" some meaning
+module M2 refines M1 {
+ class VarDecl {
+ }
+
+ class Expr {
+ var decl: VarDecl; // if kind==Ident, filled in during resolution
+
+ predicate Valid()
+ {
+ resolved ==>
+ (kind == Ident ==> decl != null)
+ }
+
+ method Resolve...
+ {
+ if (kind == Ident) {
+ decl := new VarDecl;
+ }
+ }
+ }
+}
+
+// Finally, supposing each VarDecl has a value, evaluate a resolved expression
+module M3 refines M2 {
+ class VarDecl {
+ var val: int;
+ }
+
+ class Expr {
+ method Eval() returns (r: int)
+ requires Valid();
+ requires resolved;
+ decreases Repr;
+ {
+ match (kind) {
+ case Constant =>
+ r := value;
+ case Ident =>
+ r := decl.val; // note how this statement relies on "decl" being non-null, which follows from the expression being resolved
+ case Binary =>
+ var x := left.Eval();
+ var y := right.Eval();
+ r := x + y;
+ }
+ }
+ }
+}
diff --git a/Test/dafny2/runtest.bat b/Test/dafny2/runtest.bat index 25dbed54..909f67f5 100644 --- a/Test/dafny2/runtest.bat +++ b/Test/dafny2/runtest.bat @@ -16,6 +16,7 @@ for %%f in ( StoreAndRetrieve.dfy
Intervals.dfy TreeFill.dfy TuringFactorial.dfy
MajorityVote.dfy SegmentSum.dfy
+ MonotonicHeapstate.dfy
) do (
echo.
echo -------------------- %%f --------------------
|