Added some co- test cases. Fixed some bugs.

4 files changed, 154 insertions, 1 deletions

diff --git a/Test/dafny3/Answer b/Test/dafny3/Answer
index 9cd8fc82..c4e75986 100644
--- a/Test/dafny3/Answer
+++ b/Test/dafny3/Answer
@@ -14,3 +14,11 @@ Dafny program verifier finished with 11 verified, 0 errors
 -------------------- CachedContainer.dfy --------------------

 

 Dafny program verifier finished with 47 verified, 0 errors

+

+-------------------- SimpleCoinduction.dfy --------------------

+

+Dafny program verifier finished with 28 verified, 0 errors

+

+-------------------- CalcExample.dfy --------------------

+

+Dafny program verifier finished with 6 verified, 0 errors

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;

+  }

+}

diff --git a/Test/dafny3/SimpleCoinduction.dfy b/Test/dafny3/SimpleCoinduction.dfy
new file mode 100644
index 00000000..5a8ab288
--- /dev/null
+++ b/Test/dafny3/SimpleCoinduction.dfy
@@ -0,0 +1,115 @@
+codatatype Stream<T> = Cons(head: T, tail: Stream);

+codatatype IList<T> = Nil | ICons(head: T, tail: IList);

+

+// -----------------------------------------------------------------------

+

+copredicate Pos(s: Stream<int>)

+{

+  s.head > 0 && Pos(s.tail)

+}

+

+function Up(n: int): Stream<int>

+{

+  Cons(n, Up(n+1))

+}

+

+function Inc(s: Stream<int>): Stream<int>

+{

+  Cons(s.head + 1, Inc(s.tail))

+}

+

+ghost method {:induction false} UpLemma(k: nat, n: int)

+  ensures Inc(Up(n)) ==#[k] Up(n+1);

+{

+  if (k != 0) {

+    UpLemma(k-1, n+1);

+  }

+}

+

+comethod {:induction false} CoUpLemma(n: int)

+  ensures Inc(Up(n)) == Up(n+1);

+{

+  CoUpLemma(n+1);

+}

+

+ghost method UpLemma_Auto(k: nat, n: int)

+  ensures Inc(Up(n)) ==#[k] Up(n+1);

+{

+}

+

+comethod CoUpLemma_Auto(n: int)

+  ensures Inc(Up(n)) == Up(n+1);

+{

+}

+

+// -----------------------------------------------------------------------

+

+function Repeat(n: int): Stream<int>

+{

+  Cons(n, Repeat(n))

+}

+

+comethod RepeatLemma(n: int)

+  ensures Inc(Repeat(n)) == Repeat(n+1);

+{

+}

+

+// -----------------------------------------------------------------------

+

+copredicate True(s: Stream)

+{

+  True(s.tail)

+}

+

+comethod AlwaysTrue(s: Stream)

+  ensures True(s);

+{

+  AlwaysTrue(s.tail);  // WHY does this not happen automatically? (Because 's' is not quantified over)

+}

+

+copredicate AlsoTrue(s: Stream)

+{

+  AlsoTrue(s)

+}

+

+comethod AlsoAlwaysTrue(s: Stream)

+  ensures AlsoTrue(s);

+{

+  // AlsoAlwaysTrue(s);  // here, the recursive call is not needed, because it uses the same 's', so 's' does not need to be quantified over

+}

+

+// -----------------------------------------------------------------------

+

+function Append(M: IList, N: IList): IList

+{

+  match M

+  case Nil => N

+  case ICons(x, M') => ICons(x, Append(M', N))

+}

+

+function zeros(): IList<int>

+{

+  ICons(0, zeros())

+}

+

+function ones(): IList<int>

+{

+  ICons(1, ones())

+}

+

+copredicate AtMost(a: IList<int>, b: IList<int>)

+{

+  match a

+  case Nil => true

+  case ICons(h,t) => b.ICons? && h <= b.head && AtMost(t, b.tail)

+}

+

+comethod ZerosAndOnes_Theorem0()

+  ensures AtMost(zeros(), ones());

+{

+}

+

+comethod ZerosAndOnes_Theorem1()

+  ensures Append(zeros(), ones()) == zeros();

+{

+}

diff --git a/Test/dafny3/runtest.bat b/Test/dafny3/runtest.bat
index 2ebba74a..83d2bba9 100644
--- a/Test/dafny3/runtest.bat
+++ b/Test/dafny3/runtest.bat
@@ -4,7 +4,10 @@ setlocal
 set BINARIES=..\..\Binaries

 set DAFNY_EXE=%BINARIES%\Dafny.exe

 

-for %%f in (Iter.dfy Streams.dfy Dijkstra.dfy CachedContainer.dfy) do (

+for %%f in (

+  Iter.dfy Streams.dfy Dijkstra.dfy CachedContainer.dfy

+  SimpleCoinduction.dfy CalcExample.dfy

+) do (

   echo.

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

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