New well-formedness checks for calculations (no cascading).

4 files changed, 28 insertions, 21 deletions

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 1b9408a8..e1b1ed15 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -3151,14 +3151,6 @@ namespace Microsoft.Dafny {
       }

       return null;

     }

-

-    /// <summary>

-    /// Should line i be used as a well-formedness context for the following lines and hints?

-    /// (The line must be boolean).

-    /// </summary>

-    public bool IsContextLine(int i) {

-       return Steps[i].ResolvedOp == BinaryExpr.ResolvedOpcode.Imp;

-    }

   }

 

   public class MatchStmt : Statement

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 21e60d33..9252cde5 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -1853,6 +1853,7 @@ namespace Microsoft.Dafny {
     ModuleDefinition currentModule = null;  // the name of the module whose members are currently being translated

     ICodeContext codeContext = null;  // the method/iterator whose implementation is currently being translated

     LocalVariable yieldCountVariable = null;  // non-null when an iterator body is being translated

+    bool assertAsAssume = false; // generate assume statements instead of assert statements

     int loopHeapVarCount = 0;

     int otherTmpVarCount = 0;

     Dictionary<string, Bpl.IdentifierExpr> _tmpIEs = new Dictionary<string, Bpl.IdentifierExpr>();

@@ -4406,7 +4407,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(errorMessage != null);

       Contract.Ensures(Contract.Result<Bpl.PredicateCmd>() != null);

 

-      if (RefinementToken.IsInherited(refinesToken, currentModule) && (codeContext == null || !codeContext.MustReverify)) {

+      if (assertAsAssume || (RefinementToken.IsInherited(refinesToken, currentModule) && (codeContext == null || !codeContext.MustReverify))) {

         // produce an assume instead

         return new Bpl.AssumeCmd(tok, condition);

       } else {

@@ -4445,7 +4446,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(condition != null);

       Contract.Ensures(Contract.Result<Bpl.PredicateCmd>() != null);

 

-      if (RefinementToken.IsInherited(tok, currentModule) && (codeContext == null || !codeContext.MustReverify)) {

+      if (assertAsAssume || (RefinementToken.IsInherited(tok, currentModule) && (codeContext == null || !codeContext.MustReverify))) {

         // produce an assume instead

         return new Bpl.AssumeCmd(tok, condition, kv);

       } else {

@@ -4826,12 +4827,16 @@ namespace Microsoft.Dafny {
         if (*) {

             assert wf(line0);

         } else if (*) {

+            assume wf(line0);

+            // if op is ==>: assume line0;

             hint0;

             assert wf(line1);

             assert line0 op line1;

             assume false;

         } else if (*) { ...

         } else if (*) {

+            assume wf(line<n-1>);

+            // if op is ==>: assume line<n-1>;

             hint<n-1>;

             assert wf(line<n>);

             assert line<n-1> op line<n>;

@@ -4848,19 +4853,26 @@ namespace Microsoft.Dafny {
           // check steps:

           for (int i = s.Steps.Count; 0 <= --i; ) {            

             b = new Bpl.StmtListBuilder();

-            // assume all previous context lines:

-            for (int j = 0; j <= i; j++) {

-              if (s.IsContextLine(j)) {

-                b.Add(new Bpl.AssumeCmd(s.Tok, etran.TrExpr(s.Lines[j])));

-              }

+            // assume wf[line<i>]:

+            AddComment(b, stmt, "assume wf[line" + i.ToString() + "]");

+            assertAsAssume = true;

+            TrStmt_CheckWellformed(s.Lines[i], b, locals, etran, false);

+            assertAsAssume = false;

+            if (s.Steps[i].ResolvedOp == BinaryExpr.ResolvedOpcode.Imp) {

+              // assume line<i>:

+              AddComment(b, stmt, "assume line" + i.ToString());

+              b.Add(new Bpl.AssumeCmd(s.Tok, etran.TrExpr(s.Lines[i]))); 

             }

             // hint:

+            AddComment(b, stmt, "Hint" + i.ToString());

             TrStmt(s.Hints[i], b, locals, etran);

             // check well formedness of the goal line:

+            AddComment(b, stmt, "assert wf[line" + (i + 1).ToString() + "]");

             TrStmt_CheckWellformed(s.Lines[i + 1], b, locals, etran, false);

             bool splitHappened;

             var ss = TrSplitExpr(s.Steps[i], etran, out splitHappened);

             // assert step:

+            AddComment(b, stmt, "assert line" + i.ToString() + " " + s.Steps[i].ResolvedOp.ToString() + " line" + (i + 1).ToString());

             if (!splitHappened) {

               b.Add(AssertNS(s.Lines[i + 1].tok, etran.TrExpr(s.Steps[i]), "the calculation step between the previous line and this line might not hold"));

             } else {

@@ -4875,6 +4887,7 @@ namespace Microsoft.Dafny {
           }

           // check well formedness of the first line:

           b = new Bpl.StmtListBuilder();

+          AddComment(b, stmt, "assume wf[line0]");

           TrStmt_CheckWellformed(s.Lines.First(), b, locals, etran, false);

           b.Add(new Bpl.AssumeCmd(s.Tok, Bpl.Expr.False));

           ifCmd = new Bpl.IfCmd(s.Tok, null, b.Collect(s.Tok), ifCmd, null);

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 6e775b43..e31ef49c 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -1796,10 +1796,10 @@ Calculations.dfy(8,17): Error: assertion violation
 Execution trace:

     (0,0): anon0

     (0,0): anon19_Then

-Calculations.dfy(42,11): Error: assertion violation

+Calculations.dfy(44,11): Error: assertion violation

 Execution trace:

     (0,0): anon0

-    Calculations.dfy(37,2): anon5_Else

+    Calculations.dfy(39,2): anon5_Else

 

 Dafny program verifier finished with 5 verified, 4 errors

 

diff --git a/Test/dafny0/Calculations.dfy b/Test/dafny0/Calculations.dfy
index aa447d9f..8ef36139 100644
--- a/Test/dafny0/Calculations.dfy
+++ b/Test/dafny0/Calculations.dfy
@@ -17,10 +17,12 @@ method CalcTest0(s: seq<int>) {
 		}
 	}
 	assume forall x :: x in s ==> x >= 0;
-	calc ==> {
+	calc {
 		0 < |s|;
-		{ assert s[0] >= 0; } // OK: well-formed after previous line
-		s[0] >= 0; // OK: well-formed after previous line
+	==>	{ assert s[0] >= 0; }   // OK: well-formed after previous line
+		s[0] >= 0;                // OK: well-formed after previous line
+  <==> { assert s[0] >= 0; }  // OK: well-formed when the previous line is well-formed
+    s[0] > 0 || s[0] == 0;    // OK: well-formed when the previous line is well-formed
 	}
 }
 
@@ -43,7 +45,7 @@ method CalcTest2(x: int, y: int) {
 }
 
 // calc expression:
-function CalcTest(s: seq<int>): int {
+function CalcTest3(s: seq<int>): int {
 	calc < {
 		0;
 		{ assume |s| == 5; }