1 files changed, 58 insertions, 0 deletions
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;
+  }
+}