Dafny: added test case for refinement and predicates (and fixed a parsing bug)

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;
+    }
+  }
+}
+*/