summaryrefslogtreecommitdiff
path: root/Test/dafny0
diff options
context:
space:
mode:
authorGravatar Rustan Leino <leino@microsoft.com>2012-01-10 16:19:10 -0800
committerGravatar Rustan Leino <leino@microsoft.com>2012-01-10 16:19:10 -0800
commitd9cff4a1a868e7caa7e25ffdffba33a3324b2cd7 (patch)
tree393141f562b0df1f210a1690c26cfaaee794b937 /Test/dafny0
parenta8c6c46651be5647af3d9db66c37a4f91a7781cc (diff)
Dafny: added test case for refinement and predicates (and fixed a parsing bug)
Diffstat (limited to 'Test/dafny0')
-rw-r--r--Test/dafny0/Answer8
-rw-r--r--Test/dafny0/Predicates.dfy74
-rw-r--r--Test/dafny0/Refinement.dfy71
3 files changed, 152 insertions, 1 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index deb4a2fc..8e4c2f12 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -1370,8 +1370,14 @@ Predicates.dfy[B](17,15): Related location: This is the postcondition that might
Predicates.dfy(28,9): Related location: Related location
Execution trace:
(0,0): anon0
+Predicates.dfy(85,18): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+Predicates.dfy(89,16): Error: assertion violation
+Execution trace:
+ (0,0): anon0
-Dafny program verifier finished with 9 verified, 1 error
+Dafny program verifier finished with 26 verified, 3 errors
-------------------- SmallTests.dfy --------------------
SmallTests.dfy(30,11): Error: index out of range
diff --git a/Test/dafny0/Predicates.dfy b/Test/dafny0/Predicates.dfy
index 76666ef0..2583ef19 100644
--- a/Test/dafny0/Predicates.dfy
+++ b/Test/dafny0/Predicates.dfy
@@ -29,3 +29,77 @@ module B refines A {
}
}
}
+
+// ------------------------------------------------
+
+module Loose {
+ class MyNumber {
+ var N: int;
+ ghost var Repr: set<object>;
+ predicate Valid
+ reads this, Repr;
+ {
+ this in Repr && null !in Repr &&
+ 0 <= N
+ }
+ constructor Init()
+ modifies this;
+ ensures Valid && fresh(Repr - {this});
+ {
+ N, Repr := 0, {this};
+ }
+ method Inc()
+ requires Valid;
+ modifies Repr;
+ ensures old(N) < N;
+ ensures Valid && fresh(Repr - old(Repr));
+ {
+ N := N + 2;
+ }
+ method Get() returns (n: int)
+ requires Valid;
+ ensures n == N;
+ {
+ n := N;
+ }
+ }
+}
+
+module Tight refines Loose {
+ class MyNumber {
+ predicate Valid
+ {
+ N % 2 == 0
+ }
+ constructor Init()
+ ensures N == 0;
+ method Inc()
+ ensures N == old(N) + 2;
+ }
+}
+
+module UnawareClient imports Loose {
+ class Client {
+ method Main() {
+ var n := new MyNumber.Init();
+ assert n.N == 0; // error: this is not known
+ n.Inc();
+ n.Inc();
+ var k := n.Get();
+ assert k == 4; // error: this is not known
+ }
+ }
+}
+
+module AwareClient imports Tight {
+ class Client {
+ method Main() {
+ var n := new MyNumber.Init();
+ assert n.N == 0;
+ n.Inc();
+ n.Inc();
+ var k := n.Get();
+ assert k == 4;
+ }
+ }
+}
diff --git a/Test/dafny0/Refinement.dfy b/Test/dafny0/Refinement.dfy
index e46fba0d..fb379c33 100644
--- a/Test/dafny0/Refinement.dfy
+++ b/Test/dafny0/Refinement.dfy
@@ -31,3 +31,74 @@ module B refines A {
// inherited method body
}
}
+
+// ------------------------------------------------
+/* SOON
+module Abstract {
+ class MyNumber {
+ var N: int;
+ ghost var Repr: set<object>;
+ predicate Valid
+ reads this, Repr;
+ {
+ this in Repr && null !in Repr
+ }
+ constructor Init()
+ modifies this;
+ ensures N == 0;
+ ensures Valid && fresh(Repr - {this});
+ {
+ N, Repr := 0, {this};
+ }
+ method Inc()
+ requires Valid;
+ modifies Repr;
+ ensures N == old(N) + 1;
+ ensures Valid && fresh(Repr - old(Repr));
+ {
+ N := N + 1;
+ }
+ method Get() returns (n: int)
+ requires Valid;
+ ensures n == N;
+ {
+ n := N;
+ }
+ }
+}
+
+module Concrete refines Abstract {
+ class MyNumber {
+ var a: int;
+ var b: int;
+ predicate Valid
+ {
+ N == a - b
+ }
+ constructor Init()
+ {
+ a := b;
+ }
+ method Inc()
+ {
+ if (*) { a := a + 1; } else { b := b - 1; }
+ }
+ method Get() returns (n: int)
+ {
+ n := a - b;
+ }
+ }
+}
+
+module Client imports Concrete {
+ class TheClient {
+ method Main() {
+ var n := new MyNumber.Init();
+ n.Inc();
+ n.Inc();
+ var k := n.Get();
+ assert k == 2;
+ }
+ }
+}
+*/