Dafny: added support for simple superposition refinements

4 files changed, 59 insertions, 246 deletions

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 00231d4c..ce58ffe7 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -1292,6 +1292,23 @@ Execution trace:
 

 Dafny program verifier finished with 23 verified, 9 errors

 

+-------------------- Refinement.dfy --------------------

+Refinement.dfy(12,5): Error BP5003: A postcondition might not hold on this return path.

+Refinement.dfy(11,17): Related location: This is the postcondition that might not hold.

+Execution trace:

+    (0,0): anon0

+Refinement.dfy[B](12,5): Error BP5003: A postcondition might not hold on this return path.

+Refinement.dfy(30,20): Related location: This is the postcondition that might not hold.

+Execution trace:

+    (0,0): anon0

+

+Dafny program verifier finished with 8 verified, 2 errors

+

+-------------------- RefinementErrors.dfy --------------------

+RefinementErrors.dfy(13,11): Error: a refining method is not allowed to extend the modifies clause

+RefinementErrors.dfy(13,11): Error: a refining method is not allowed to add preconditions

+2 resolution/type errors detected in RefinementErrors.dfy

+

 -------------------- ReturnErrors.dfy --------------------

 ReturnErrors.dfy(30,10): Error: cannot have method call in return statement.

 ReturnErrors.dfy(36,10): Error: cannot have effectful parameter in multi-return statement.

diff --git a/Test/dafny0/Refinement.dfy b/Test/dafny0/Refinement.dfy
index c10d86f3..e46fba0d 100644
--- a/Test/dafny0/Refinement.dfy
+++ b/Test/dafny0/Refinement.dfy
@@ -1,198 +1,33 @@
-// Concrete language syntax for a Dafny extension with refinement. 
-// IntegerCounter example.
-// 6/28/2010
-
-class A { 
-  var n : int;
-    
-  method Init() modifies this; 
-  { n := 0;}
-
-  method Inc() modifies this; 
-  { n := n + 1;}
-
-  method Dec() 
-    modifies this;
-    requires n > 0; 
-  { n := n - 1;}  
-  
-  method Test1(p: int) returns (i: int) 
-  {   
-    i := p;
-  }
-
-  method Test2() returns (o: object)
-  { o := this; }
-}
-
-class B refines A {
-  var inc : int, dec : int;
-    
-  replaces n by n == inc - dec;
-  // transforms n into inc - dec;
-    
-  refines Init() modifies this;
-  { inc := 0; dec := 0;}
-    
-  refines Inc() modifies this;
-  { inc := inc + 1; }  
-  
-  refines Dec() 
-    modifies this;
-    requires inc > dec; 
-  { dec := dec + 1; }
-
-  refines Test1(p: int) returns (i: int) 
-  {
-    i := p;
-  }
-}
-
-// Carrol Morgan's calculator
-// 7/2/2010 Kuat
-
-class Util {
-  static function method seqsum(x:seq<int>) : int
-    decreases x;
-  {
-    if (x == []) then 0 else x[0] + seqsum(x[1..])
+module A {
+  class X { }
+  class T {
+    method M(x: int) returns (y: int)
+      requires 0 <= x;
+      ensures 0 <= y;
+    {
+      y := 2 * x;
+    }
+    method Q() returns (q: int, r: int, s: int)
+      ensures 0 <= q && 0 <= r && 0 <= s;
+    {  // error: failure to establish postcondition about q
+      r, s := 100, 200;
+    }
   }
 }
 
-
-class ACalc {
-  var util: Util;
-  var vals: seq<int>;
-  
-  method reset() 
-    modifies this;
-  {
-    vals := [];
-  }
-  
-  method add(x: int) 
-    modifies this;
-  {
-    vals := [x] + vals;
-  }
-  
-  method mean() returns (m: int)     
-    requires |vals| > 0;
-  {
-    m := util.seqsum(vals)/|vals|;
+module B refines A {
+  class C { }
+  datatype Dt = Ax | Bx;
+  class T {
+    method P() returns (p: int)
+    {
+      p := 18;
+    }
+    method M(x: int) returns (y: int)
+      ensures y % 2 == 0;  // add a postcondition
+    method Q() returns (q: int, r: int, s: int)
+      ensures 12 <= r;
+      ensures 1200 <= s;  // error: postcondition is not established by
+                          // inherited method body
   }
 }
-
-
-
-class CCalc refines ACalc {
-  var util2: Util;
-  var sum: int;
-  var num: int;
-  replaces vals by sum == util2.seqsum(vals) && num == |vals|;
-
-  refines reset() 
-    modifies this;
-  {
-    sum := 0;
-    num := 0;
-  }
-
-  refines add(x: int)
-    modifies this;
-  {
-    sum := sum + x;
-    num := num + 1;
-  }
-
-  refines mean() returns (m: int)
-    requires num > 0;
-  {
-    m := sum/num;
-  }
-}
-
-// Sequence refined to a singly linked list
-// 6/22/2010: Kuat Yessenov
-
-class List<T> {
-  var rep: seq<T>;
-  method Clear() 
-    modifies this;
-  {
-    rep := [];
-  }
-  
-  method Append(x: T) 
-    modifies this; 
-  {
-    rep := rep + [x];
-  }
-  
-  method Prepend(x: T) 
-    modifies this; 
-  {
-    rep := [x] + rep;
-  }
-  
-  method Insert(i: int, x: T) 
-    requires 0 <= i && i < |rep|;
-    modifies this;
-  {
-    rep := rep[i:=x];
-  }
-}
-
-class Node<T> {
-  var data: T;
-  var next: Node<T>;
-}   
-
-class LinkedList refines List {
-  var first: Node<T>;
-  ghost var nodes: set<Node<T>>;
-    
-  function Abstraction(n: Node<T>, nodes: set<Node<T>>, rep: seq<T>) : bool
-  decreases nodes;
-  reads n, nodes;
-  {
-    if (n == null) then 
-            rep == [] &&
-            nodes == {}
-        else 
-            |rep| >= 1 &&
-            n.data == rep[0] &&
-            n in nodes &&
-            n.next in nodes + {null} &&
-            Abstraction(n.next, nodes - {n}, rep[1..])
-  }
-
-  replaces rep by Abstraction(first, nodes, rep);     
-
-  refines Clear() 
-    modifies this;
-  {
-    first := null;
-    nodes := {};
-  }
-
-  refines Prepend(x: T) 
-    modifies this;
-  {
-    var n := new Node<T>;
-    n.data := x;
-    n.next := first;
-    first := n;
-    nodes := {n} + nodes;
-    assert nodes - {n} == old(nodes); //set extensionality
-  }
-} 
-
-
-
-
-
-
-
-    
-    
diff --git a/Test/dafny0/RefinementErrors.dfy b/Test/dafny0/RefinementErrors.dfy
index de8694b3..b10c035e 100644
--- a/Test/dafny0/RefinementErrors.dfy
+++ b/Test/dafny0/RefinementErrors.dfy
@@ -1,57 +1,18 @@
-class A refines C {
-}
-
-class B refines A {
-}
-
-class C refines B {
-}
-
-
-class D {
-  refines M()
-  {
-  }
-}
-
-class E {
-  var x: int;
-  
-  method M() 
-  {
-    x := 0;
-  }
-}
-
-class F {  
-  replaces M by x == y;
-}
-
-class G refines E {
-  var y: int;
-  replaces x by x == y;
-  
-  refines M() returns (i: int)
-  {
+module A {
+  class C {
+    method M(y: int) returns (x: int)
+    {
+      x := 6;
+    }
   }
 }
 
-class H refines E {
-  var x: int;
-
-  method M() 
-  {
+module B refines A {
+  class C {
+    var k: int;
+    method M(y: int) returns (x: int)
+      requires 0 <= y;  // error: cannot add a precondition
+      modifies this;  // error: cannot add a modifies clause
+      ensures 0 <= x;  // fine
   }
 }
-
-class J refines E {
-  var y: int;
-  replaces x by x == y;
-
-  refines M()
-  {
-    y := 1;
-  }
-}
-
-
diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat
index 5b135190..45c434a5 100644
--- a/Test/dafny0/runtest.bat
+++ b/Test/dafny0/runtest.bat
@@ -18,7 +18,7 @@ for %%f in (TypeTests.dfy NatTypes.dfy SmallTests.dfy Definedness.dfy
             Comprehensions.dfy Basics.dfy ControlStructures.dfy

             Termination.dfy DTypes.dfy ParallelResolveErrors.dfy Parallel.dfy

             TypeParameters.dfy Datatypes.dfy TypeAntecedents.dfy SplitExpr.dfy

-            LoopModifies.dfy

+            LoopModifies.dfy Refinement.dfy RefinementErrors.dfy

             ReturnErrors.dfy ReturnTests.dfy ChainingDisjointTests.dfy

             CallStmtTests.dfy MultiSets.dfy PredExpr.dfy LetExpr.dfy) do (

   echo.