Merge

6 files changed, 175 insertions, 16 deletions

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 671c7c91..140f642f 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -332,10 +332,10 @@ Execution trace:
 Definedness.dfy(86,5): Error: possible violation of function precondition

 Execution trace:

     (0,0): anon0

-Definedness.dfy(86,10): Error: assignment may update an object not in the enclosing context's modifies clause

+Definedness.dfy(86,10): Error: target object may be null

 Execution trace:

     (0,0): anon0

-Definedness.dfy(86,10): Error: target object may be null

+Definedness.dfy(86,10): Error: assignment may update an object not in the enclosing context's modifies clause

 Execution trace:

     (0,0): anon0

 Definedness.dfy(87,10): Error: possible violation of function precondition

@@ -542,7 +542,16 @@ ResolutionErrors.dfy(309,18): Error: ghost fields are allowed only in specificat
 ResolutionErrors.dfy(318,15): Error: ghost variables are allowed only in specification contexts

 ResolutionErrors.dfy(343,2): Error: incorrect type of method in-parameter 1 (expected GenericClass<int>, got GenericClass<bool>)

 ResolutionErrors.dfy(355,18): Error: incorrect type of datatype constructor argument (found GList<_T0>, expected GList<int>)

-48 resolution/type errors detected in ResolutionErrors.dfy

+ResolutionErrors.dfy(363,4): Error: arguments to + must be int or a collection type (instead got bool)

+ResolutionErrors.dfy(368,4): Error: all lines in a calculation must have the same type (got int after bool)

+ResolutionErrors.dfy(371,4): Error: first argument to ==> must be of type bool (instead got int)

+ResolutionErrors.dfy(371,4): Error: second argument to ==> must be of type bool (instead got int)

+ResolutionErrors.dfy(372,8): Error: first argument to ==> must be of type bool (instead got int)

+ResolutionErrors.dfy(372,8): Error: second argument to ==> must be of type bool (instead got int)

+ResolutionErrors.dfy(377,8): Error: first argument to ==> must be of type bool (instead got int)

+ResolutionErrors.dfy(377,8): Error: second argument to ==> must be of type bool (instead got int)

+ResolutionErrors.dfy(382,4): Error: print statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)

+57 resolution/type errors detected in ResolutionErrors.dfy

 

 -------------------- ParseErrors.dfy --------------------

 ParseErrors.dfy(4,19): error: a chain cannot have more than one != operator

@@ -553,7 +562,13 @@ ParseErrors.dfy(15,18): error: this operator cannot be part of a chain
 ParseErrors.dfy(16,19): error: this operator cannot be part of a chain

 ParseErrors.dfy(17,18): error: this operator cannot be part of a chain

 ParseErrors.dfy(18,18): error: chaining not allowed from the previous operator

-8 parse errors detected in ParseErrors.dfy

+ParseErrors.dfy(46,8): error: the main operator of a calculation must be transitive

+ParseErrors.dfy(62,2): error: this operator cannot continue this calculation

+ParseErrors.dfy(63,2): error: this operator cannot continue this calculation

+ParseErrors.dfy(68,2): error: this operator cannot continue this calculation

+ParseErrors.dfy(69,2): error: this operator cannot continue this calculation

+ParseErrors.dfy(75,2): error: this operator cannot continue this calculation

+14 parse errors detected in ParseErrors.dfy

 

 -------------------- Array.dfy --------------------

 Array.dfy(10,8): Error: assignment may update an array element not in the enclosing context's modifies clause

@@ -857,19 +872,19 @@ Execution trace:
 Dafny program verifier finished with 32 verified, 11 errors

 

 -------------------- ControlStructures.dfy --------------------

-ControlStructures.dfy(5,3): Error: missing case in case statement: Blue

+ControlStructures.dfy(5,3): Error: missing case in case statement: Purple

 Execution trace:

     (0,0): anon0

     (0,0): anon6_Else

     (0,0): anon7_Else

-    (0,0): anon8_Else

-    (0,0): anon9_Then

-ControlStructures.dfy(5,3): Error: missing case in case statement: Purple

+    (0,0): anon8_Then

+ControlStructures.dfy(5,3): Error: missing case in case statement: Blue

 Execution trace:

     (0,0): anon0

     (0,0): anon6_Else

     (0,0): anon7_Else

-    (0,0): anon8_Then

+    (0,0): anon8_Else

+    (0,0): anon9_Then

 ControlStructures.dfy(14,3): Error: missing case in case statement: Purple

 Execution trace:

     (0,0): anon0

@@ -1305,7 +1320,7 @@ CoPredicates.dfy(30,22): Related location: Related location
 Execution trace:

     (0,0): anon0

 

-Dafny program verifier finished with 14 verified, 1 error

+Dafny program verifier finished with 12 verified, 1 error

 

 -------------------- TypeAntecedents.dfy --------------------

 TypeAntecedents.dfy(32,13): Error: assertion violation

@@ -1615,6 +1630,25 @@ TailCalls.dfy(42,12): Error: 'decreases *' is allowed only on tail-recursive met
 TailCalls.dfy(64,12): Error: 'decreases *' is allowed only on tail-recursive methods

 5 resolution/type errors detected in TailCalls.dfy

 

+-------------------- Calculations.dfy --------------------

+Calculations.dfy(3,4): Error: index out of range

+Execution trace:

+    (0,0): anon0

+    (0,0): anon11_Then

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

+Execution trace:

+    (0,0): anon0

+    (0,0): anon13_Then

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

+Execution trace:

+    (0,0): anon0

+    (0,0): anon13_Then

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

+Execution trace:

+    (0,0): anon0

+    Calculations.dfy(31,2): anon5_Else

+

+Dafny program verifier finished with 4 verified, 4 errors

 -------------------- IteratorResolution.dfy --------------------

 IteratorResolution.dfy(59,11): Error: LHS of assignment does not denote a mutable field

 IteratorResolution.dfy(64,18): Error: arguments must have the same type (got _T0 and int)

diff --git a/Test/dafny0/Calculations.dfy b/Test/dafny0/Calculations.dfy
new file mode 100644
index 00000000..9e44f62e
--- /dev/null
+++ b/Test/dafny0/Calculations.dfy
@@ -0,0 +1,37 @@
+method CalcTest0(s: seq<int>) {
+	calc {
+		s[0]; // error: ill-formed line
+	}
+	
+	calc {
+		2;
+		{ assert s[0] == 1; } // error: ill-formed hint
+		1 + 1;
+	}
+	
+	if (|s| > 0) {
+		calc {
+			s[0]; // OK: well-formed in this context
+			{ assert s[0] == s[0]; }
+			<= s[0];
+		}
+	}
+}
+
+method CalcTest1(x: int, y: int) {
+	calc {
+		x + y;
+		{ assume x == 0; }
+		y;
+	}
+	assert x == 0; // OK: follows from x + y == y;
+}
+
+method CalcTest2(x: int, y: int) {
+	calc {
+		x + y;
+		{ assume x == 0; }
+		y + x;
+	}
+	assert x == 0; // error: even though assumed above, is not exported by the calculation
+}
\ No newline at end of file
diff --git a/Test/dafny0/CoPredicates.dfy b/Test/dafny0/CoPredicates.dfy
index 67dff91b..c5651c90 100644
--- a/Test/dafny0/CoPredicates.dfy
+++ b/Test/dafny0/CoPredicates.dfy
@@ -51,8 +51,9 @@ function U2(n: int): Stream<int>
   UpwardBy2(n)

 }

 

-ghost method Lemma2(n: int)

-  ensures Even(UpwardBy2(2*n));  // this is true, but Dafny can't prove it

-{

-  assert Even(U2(2*n));  // ... thanks to this lemma

-}

+// Postponed:

+//ghost method Lemma2(n: int)

+//  ensures Even(UpwardBy2(2*n));  // this is true, and Dafny can prove it

+//{

+//  assert Even(U2(2*n));  // ... thanks to this lemma

+//}

diff --git a/Test/dafny0/ParseErrors.dfy b/Test/dafny0/ParseErrors.dfy
index 41df50eb..9a3cc18b 100644
--- a/Test/dafny0/ParseErrors.dfy
+++ b/Test/dafny0/ParseErrors.dfy
@@ -18,3 +18,61 @@ method TestChaining1<T>(s: set<T>, t: set<T>, u: set<T>, x: T, SuperSet: set<set
   ensures x in s == t;  // error: 'in' is not chaining

 {

 }

+

+// ---------------------- calc statements -----------------------------------

+

+method TestCalc()

+{

+  calc {} // OK, empty calculations are allowed

+  calc {

+	2 + 3; // OK, single-line calculations are allowed

+  }

+  calc {

+	2 + 3;

+	calc {  // OK: a calc statement is allowed as a sub-hint

+		2;

+		1 + 1;

+	}

+	calc {

+		3;

+		1 + 2;

+	}

+	{ assert true; } // OK: multiple subhints are allowed between two lines

+	1 + 1 + 1 + 2;

+	{ assert 1 + 1 + 1 == 3; }

+	{ assert true; }

+	3 + 2;

+  }

+  calc != { // error: != is not allowed as the main operator of a calculation

+	2 + 3;

+	4;

+  }

+  calc { // OK, these operators are compatible

+	2 + 3;

+	> 4;

+	>= 2 + 2;

+  }

+  calc < { // OK, these operators are compatible

+	2 + 3;

+	== 5;

+	<= 3 + 3;

+  }

+  calc < { // error: cannot mix < and >= or >

+	2 + 3;

+	>= 5;

+	> 2 + 2;

+	6;

+  }

+  calc >= { // error: cannot mix >= and <= or !=

+	2 + 3;

+	<= 5;

+	!= 2 + 2;

+	3;

+  }

+  calc { // error: cannot have more than one != per calc

+	2 + 3;

+	!= 4;

+	!= 1 + 2;

+	3;

+  }

+}

diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index 274cc95a..c615c5ec 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -354,3 +354,32 @@ method MG1(l: GList, n: nat)
   var t := GCons(100, GNil);

   t := GCons(120, l);  // error: types don't match up (List<T$0> versus List<int>)

 }

+

+// ------------------- calc statements ------------------------------

+

+method TestCalc(m: int, n: int, a: bool, b: bool)

+{

+	calc {

+		a + b; // error: invalid line

+		n + m;

+	}

+	calc {

+		a && b;

+		n + m; // error: all lines must have the same type

+	}

+	calc ==> {

+		n + m; // error: ==> operator requires boolean lines

+		n + m + 1;

+		n + m + 2;

+	}		

+	calc {

+		n + m;

+		n + m + 1;

+		==> n + m + 2; // error: ==> operator requires boolean lines

+	}

+	calc {

+		n + m;

+		{ print n + m; } // error: non-ghost statements are not allowed in hints

+		m + n;

+	}			

+}

diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat
index 9789e7d7..9118e388 100644
--- a/Test/dafny0/runtest.bat
+++ b/Test/dafny0/runtest.bat
@@ -24,7 +24,7 @@ for %%f in (TypeTests.dfy NatTypes.dfy SmallTests.dfy Definedness.dfy
             CallStmtTests.dfy MultiSets.dfy PredExpr.dfy LetExpr.dfy

             Predicates.dfy Skeletons.dfy Maps.dfy LiberalEquality.dfy

             RefinementModificationChecking.dfy TailCalls.dfy

-            IteratorResolution.dfy Iterators.dfy) do (

+            Calculations.dfy IteratorResolution.dfy Iterators.dfy) do (

   echo.

   echo -------------------- %%f --------------------

   %DAFNY_EXE% /compile:0 /print:out.bpl.tmp /dprint:out.dfy.tmp %* %%f