Added explies support to calculations.

6 files changed, 74 insertions, 29 deletions

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 6b77d4a6..f67ae73f 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -1396,6 +1396,7 @@ CalcOp<out IToken x, out BinaryExpr.Opcode/*!*/ op>
   | '\u2265'       (. x = t;  op = BinaryExpr.Opcode.Ge; .)

   | EquivOp        (. x = t;  op = BinaryExpr.Opcode.Iff; .)

   | ImpliesOp      (. x = t;  op = BinaryExpr.Opcode.Imp; .)

+  | ExpliesOp      (. x = t;  op = BinaryExpr.Opcode.Exp; .) 

   )

   .

 Hint<out BlockStmt s>

@@ -1433,9 +1434,9 @@ ImpliesExpliesExpression<out Expression/*!*/ e0>
   [ ImpliesOp                                  (. x = t; .)

     ImpliesExpression<out e1>                  (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.Imp, e0, e1); .)

   | ExpliesOp                                  (. x = t; .)

-    LogicalExpression<out e1>                  (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.Exp, e1, e0); .)

+    LogicalExpression<out e1>                  (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.Exp, e0, e1); .)

     { ExpliesOp                                (. x = t; .)

-      LogicalExpression<out e1>                (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.Exp, e1, e0); .)

+      LogicalExpression<out e1>                (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.Exp, e0, e1); .)

     }

   ]

   .

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index b0450d7a..c5bd0abb 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -8,6 +8,7 @@ using System.Text;
 using System.Collections.Generic;

 using System.Diagnostics.Contracts;

 using System.Numerics;

+using System.Linq;

 using Microsoft.Boogie;

 

 namespace Microsoft.Dafny {

@@ -3107,13 +3108,36 @@ namespace Microsoft.Dafny {
     }

 

     /// <summary>

-    /// Is op a valid calculation operator (i.e. a transitive relational operator)?

+    /// The line whose well-formedness is independant from other lines.

+    /// (Last line in case of explies-calculation, first line otherwise).

+    /// </summary>

+    public Expression InitalLine() 

+    {

+      Contract.Requires(Lines.Count > 0);

+      Contract.Requires(Result != null);  // Available after resolution

+      if (Result.Op == BinaryExpr.Opcode.Exp) {

+        return Lines.Last();

+      } else {

+        return Lines.First();

+      }

+    }

+

+    /// <summary>

+    /// Is op a valid calculation operator?

     /// </summary>

     [Pure]

     public static bool ValidOp(BinaryExpr.Opcode op) {

       return op == BinaryExpr.Opcode.Eq || op == BinaryExpr.Opcode.Lt || op == BinaryExpr.Opcode.Le || op == BinaryExpr.Opcode.Gt || op == BinaryExpr.Opcode.Ge

         || op == BinaryExpr.Opcode.Neq

-        || op == BinaryExpr.Opcode.Iff || op == BinaryExpr.Opcode.Imp;

+        || LogicOp(op);

+    }

+

+    /// <summary>

+    /// Is op a valid operator only for Boolean lines?

+    /// </summary>

+    [Pure]

+    public static bool LogicOp(BinaryExpr.Opcode op) {

+      return op == BinaryExpr.Opcode.Iff || op == BinaryExpr.Opcode.Imp || op == BinaryExpr.Opcode.Exp;

     }

 

     /// <summary>

@@ -3126,9 +3150,10 @@ namespace Microsoft.Dafny {
         return op2 == BinaryExpr.Opcode.Eq;

       if (op1 == op2) 

         return true;

-      if (op1 == BinaryExpr.Opcode.Iff || op1 == BinaryExpr.Opcode.Imp || op2 == BinaryExpr.Opcode.Iff || op2 == BinaryExpr.Opcode.Imp)

+      if (LogicOp(op1) || LogicOp(op2))

         return op2 == BinaryExpr.Opcode.Eq ||

           (op1 == BinaryExpr.Opcode.Imp && op2 == BinaryExpr.Opcode.Iff) ||

+          (op1 == BinaryExpr.Opcode.Exp && op2 == BinaryExpr.Opcode.Iff) ||

           (op1 == BinaryExpr.Opcode.Eq && op2 == BinaryExpr.Opcode.Iff);

       return op2 == BinaryExpr.Opcode.Eq ||

         (op1 == BinaryExpr.Opcode.Lt && op2 == BinaryExpr.Opcode.Le) ||

@@ -3833,7 +3858,7 @@ namespace Microsoft.Dafny {
     public enum Opcode {

       Iff,

       Imp,

-      Exp, // turned into Imp during resolution; the order of subexpressions is reversed

+      Exp, // turned into Imp during resolution

       And,

       Or,

       Eq,

@@ -4068,8 +4093,14 @@ namespace Microsoft.Dafny {
       Contract.Requires(e0 != null);

       Contract.Requires(e1 != null);

       this.Op = op;

-      this.E0 = e0;

-      this.E1 = e1;

+      if (op == Opcode.Exp) {

+        // The order of operands is reversed so that it can be turned into implication during resolution

+        this.E0 = e1;

+        this.E1 = e0;

+      } else {

+        this.E0 = e0;

+        this.E1 = e1;

+      }

     }

 

     public override IEnumerable<Expression> SubExpressions {

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index 17d4b0b9..d79ef23c 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -2270,6 +2270,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			x = t;  op = BinaryExpr.Opcode.Imp; 

 			break;

 		}

+		case 93: case 94: {

+			ExpliesOp();

+			x = t;  op = BinaryExpr.Opcode.Exp; 

+			break;

+		}

 		default: SynErr(192); break;

 		}

 	}

@@ -2311,6 +2316,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		} else SynErr(194);

 	}

 

+	void ExpliesOp() {

+		if (la.kind == 93) {

+			Get();

+		} else if (la.kind == 94) {

+			Get();

+		} else SynErr(195);

+	}

+

 	void EquivExpression(out Expression/*!*/ e0) {

 		Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x;  Expression/*!*/ e1; 

 		ImpliesExpliesExpression(out e0);

@@ -2335,12 +2348,12 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 				ExpliesOp();

 				x = t; 

 				LogicalExpression(out e1);

-				e0 = new BinaryExpr(x, BinaryExpr.Opcode.Exp, e1, e0); 

+				e0 = new BinaryExpr(x, BinaryExpr.Opcode.Exp, e0, e1); 

 				while (la.kind == 93 || la.kind == 94) {

 					ExpliesOp();

 					x = t; 

 					LogicalExpression(out e1);

-					e0 = new BinaryExpr(x, BinaryExpr.Opcode.Exp, e1, e0); 

+					e0 = new BinaryExpr(x, BinaryExpr.Opcode.Exp, e0, e1); 

 				}

 			}

 		}

@@ -2387,14 +2400,6 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		}

 	}

 

-	void ExpliesOp() {

-		if (la.kind == 93) {

-			Get();

-		} else if (la.kind == 94) {

-			Get();

-		} else SynErr(195);

-	}

-

 	void RelationalExpression(out Expression/*!*/ e) {

 		Contract.Ensures(Contract.ValueAtReturn(out e) != null);

 		IToken x, firstOpTok = null;  Expression e0, e1, acc = null;  BinaryExpr.Opcode op;

@@ -3315,8 +3320,8 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		{T,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, T,T,x,x, T,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,x,T,x, x,x,x,T, x,x,x,T, x,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x},

 		{x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,T,x,x, x,x,T,x, T,x,x,x, x,x,T,x, T,x,x,T, x,x,x,x, x,T,T,x, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,T, x,x,T,T, T,T,T,T, T,x,x,T, T,T,x,x, x,x},

 		{x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,T,x,x, x,x,T,x, T,x,x,x, x,x,T,x, T,x,x,T, x,x,x,x, x,T,T,x, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,T, x,x,T,T, T,T,T,T, T,x,x,T, T,T,x,x, x,x},

-		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},

-		{x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,T,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,T,x,x, x,x,x,x, T,x,x,x, x,x,T,x, T,x,x,T, x,x,x,x, x,T,T,x, T,x,T,T, T,T,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,T,x,T, x,x,T,T, T,T,T,T, T,x,x,T, T,T,x,x, x,x},

+		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},

+		{x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,T,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,T,x,x, x,x,x,x, T,x,x,x, x,x,T,x, T,x,x,T, x,x,x,x, x,T,T,x, T,x,T,T, T,T,T,T, T,T,T,T, T,T,T,x, x,x,x,x, x,T,x,T, x,x,T,T, T,T,T,T, T,x,x,T, T,T,x,x, x,x},

 		{x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,T,x,x, x,x,T,x, T,x,x,x, x,x,T,T, T,x,T,T, x,x,x,x, x,T,T,x, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,T, x,x,T,T, T,T,T,T, T,x,x,T, T,T,x,x, x,x},

 		{x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x},

 		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 03cee979..b73fad1e 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -4872,19 +4872,19 @@ namespace Microsoft.Dafny {
             // assume wf[line<i>]:

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

             assertAsAssume = true;

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

+            TrStmt_CheckWellformed(s.Steps[i].E0, 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]))); 

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

             }

             // 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);

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

             bool splitHappened;

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

             // assert step:

@@ -4904,7 +4904,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);

+          TrStmt_CheckWellformed(s.InitalLine(), 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);

           builder.Add(ifCmd);

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 26d4de73..cdb63528 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -1800,19 +1800,19 @@ TailCalls.dfy(64,12): Error: 'decreases *' is allowed only on tail-recursive met
 Calculations.dfy(3,4): Error: index out of range

 Execution trace:

     (0,0): anon0

-    (0,0): anon20_Then

+    (0,0): anon24_Then

 Calculations.dfy(8,13): Error: index out of range

 Execution trace:

     (0,0): anon0

-    (0,0): anon22_Then

+    (0,0): anon26_Then

 Calculations.dfy(8,17): Error: assertion violation

 Execution trace:

     (0,0): anon0

-    (0,0): anon22_Then

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

+    (0,0): anon26_Then

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

 Execution trace:

     (0,0): anon0

-    Calculations.dfy(39,2): anon5_Else

+    Calculations.dfy(47,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 8ef36139..54a9a3d4 100644
--- a/Test/dafny0/Calculations.dfy
+++ b/Test/dafny0/Calculations.dfy
@@ -24,6 +24,14 @@ method CalcTest0(s: seq<int>) {
   <==> { 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
 	}
+  
+  calc { // same as the last one, but well-formedness is checked in reverse order
+    s[0] + 1 > 0;
+  <==>
+    s[0] >= 0;
+  <== { assert s[0] >= 0; }
+    0 < |s|;
+  }  
 }
 
 method CalcTest1(x: int, y: int) {