Dafny: added support for simple superposition refinements

5 files changed, 132 insertions, 247 deletions

diff --git a/Dafny/RefinementTransformer.cs b/Dafny/RefinementTransformer.cs
index fb956883..d7fde895 100644
--- a/Dafny/RefinementTransformer.cs
+++ b/Dafny/RefinementTransformer.cs
@@ -104,6 +104,7 @@ namespace Microsoft.Dafny {
       }

 

       // Merge the declarations of prev into the declarations of m

+

       foreach (var d in prev.TopLevelDecls) {

         int index;

         if (!declaredNames.TryGetValue(d.Name, out index)) {

@@ -513,7 +514,78 @@ namespace Microsoft.Dafny {
     // -------------------------------------------------- Merging ---------------------------------------------------------------

 

     ClassDecl MergeClass(ClassDecl nw, ClassDecl prev) {

-      // TODO

+      // Create a simple name-to-member dictionary.  Ignore any duplicates at this time.

+      var declaredNames = new Dictionary<string, int>();

+      for (int i = 0; i < nw.Members.Count; i++) {

+        var member = nw.Members[i];

+        if (!declaredNames.ContainsKey(member.Name)) {

+          declaredNames.Add(member.Name, i);

+        }

+      }

+

+      // Merge the declarations of prev into the declarations of m

+      foreach (var member in prev.Members) {

+        int index;

+        if (!declaredNames.TryGetValue(member.Name, out index)) {

+          nw.Members.Add(CloneMember(member));

+        } else {

+          var nwMember = nw.Members[index];

+          if (nwMember is Field) {

+            reporter.Error(nwMember, "a field declaration ({0}) in a refining class ({1}) is not allowed replace an existing declaration in the refinement base", nwMember.Name, nw.Name);

+

+          } else if (nwMember is Function) {

+            var f = (Function)nwMember;

+            if (!(member is Function)) {

+              reporter.Error(nwMember, "a function declaration ({0}) can only refine a function", nwMember.Name);

+            } else {

+              var clone = (Function)CloneMember(member);

+              if (f.Decreases.Expressions.Count != 0) {

+                reporter.Error(nwMember, "decreases clause on refining function not supported");

+              }

+              if (f.Reads.Count != 0) {

+                reporter.Error(nwMember, "a refining function is not allowed to extend the reads clause");

+              }

+              if (f.Req.Count != 0) {

+                reporter.Error(nwMember, "a refining function is not allowed to add preconditions");

+              }

+              // TODO: check agreement for f.TypeArgs, f.ResultType, f.Formals, and flags.  For now, they are ignored and assumed to be the same.

+              foreach (var e in f.Ens) {

+                clone.Ens.Add(e);

+              }

+              if (f.Body != null) {

+                reporter.Error(nwMember, "body of refining function is not yet supported");  // TODO

+              }

+              nw.Members[index] = clone;

+            }

+

+          } else {

+            var m = (Method)nwMember;

+            if (!(member is Method)) {

+              reporter.Error(nwMember, "a method declaration ({0}) can only refine a method", nwMember.Name);

+            } else {

+              var clone = (Method)CloneMember(member);

+              if (m.Decreases.Expressions.Count != 0) {

+                reporter.Error(nwMember, "decreases clause on refining method not supported");

+              }

+              if (m.Mod.Expressions.Count != 0) {

+                reporter.Error(nwMember, "a refining method is not allowed to extend the modifies clause");

+              }

+              if (m.Req.Count != 0) {

+                reporter.Error(nwMember, "a refining method is not allowed to add preconditions");

+              }

+              // TODO: check agreement for m.TypeArgs, m.Ins, m.Outs, and flags.  For now, they are ignored and assumed to be the same.

+              foreach (var e in m.Ens) {

+                clone.Ens.Add(e);

+              }

+              if (m.Body != null) {

+                reporter.Error(nwMember, "body of refining method is not yet supported");  // TODO

+              }

+              nw.Members[index] = clone;

+            }

+          }

+        }

+      }

+

       return nw;

     }

   }

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.