Bugfix in the translation of calc statements (oops), added more resolution and verification tests

1 files changed, 37 insertions, 0 deletions

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