Added some co- test cases. Fixed some bugs.

1 files changed, 27 insertions, 0 deletions

diff --git a/Test/dafny3/CalcExample.dfy b/Test/dafny3/CalcExample.dfy
new file mode 100644
index 00000000..c94c18d2
--- /dev/null
+++ b/Test/dafny3/CalcExample.dfy
@@ -0,0 +1,27 @@
+function f(x: int, y: int): int

+

+ghost method Associativity(x: int, y: int, z: int)

+  ensures f(x, f(y, z)) == f(f(x, y), z);

+

+ghost method Monotonicity(y: int, z: int)

+  requires y <= z;

+  ensures forall x :: f(x, y) <= f(x, z);

+

+ghost method DiagonalIdentity(x: int)

+  ensures f(x, x) == x;

+

+method M(a: int, b: int, c: int, x: int)

+  requires c <= x == f(a, b);

+{

+  calc {

+    f(a, f(b, c));

+    { Associativity(a, b, c); }

+    f(f(a, b), c);

+    { assert f(a, b) == x; }

+    f(x, c);

+    { assert c <= x; Monotonicity(c, x); }

+    <= f(x, x);

+    { DiagonalIdentity(x); }

+    x;

+  }

+}