Added some co- test cases. Fixed some bugs.

6 files changed, 210 insertions, 2 deletions

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 760e6880..13e7a8b0 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -1336,6 +1336,20 @@ CoResolution.dfy(92,4): Error: a recursive call from a comethod can go only to o
 10 resolution/type errors detected in CoResolution.dfy

 

 -------------------- CoPrefix.dfy --------------------

+CoPrefix.dfy(161,3): Error BP5003: A postcondition might not hold on this return path.

+CoPrefix.dfy(160,15): Related location: This is the postcondition that might not hold.

+Execution trace:

+    (0,0): anon0

+    (0,0): anon3_Else

+CoPrefix.dfy(166,3): Error BP5003: A postcondition might not hold on this return path.

+CoPrefix.dfy(165,15): Related location: This is the postcondition that might not hold.

+Execution trace:

+    (0,0): anon0

+    (0,0): anon3_Else

+CoPrefix.dfy(173,5): Error: cannot prove termination; try supplying a decreases clause

+Execution trace:

+    (0,0): anon0

+    (0,0): anon3_Then

 CoPrefix.dfy(60,7): Error: failure to decrease termination measure

 Execution trace:

     (0,0): anon0

@@ -1370,7 +1384,7 @@ Execution trace:
     (0,0): anon0

     (0,0): anon3_Else

 

-Dafny program verifier finished with 24 verified, 6 errors

+Dafny program verifier finished with 41 verified, 9 errors

 

 -------------------- CoinductiveProofs.dfy --------------------

 CoinductiveProofs.dfy(26,12): Error: assertion violation

diff --git a/Test/dafny0/CoPrefix.dfy b/Test/dafny0/CoPrefix.dfy
index 991e160f..d3cecc28 100644
--- a/Test/dafny0/CoPrefix.dfy
+++ b/Test/dafny0/CoPrefix.dfy
@@ -148,3 +148,44 @@ comethod {:induction false} BadTheorem(s: IList)
 {  // error: postcondition violation

   BadTheorem(s.tail);

 }

+

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

+

+// Make sure recursive calls get checked for termination

+module Recursion {

+  comethod X() { Y(); }

+  comethod Y() { X(); }

+

+  comethod G(x: int)

+    ensures x < 100;

+  {  // error: postcondition violation (when _k == 0)

+    H(x);

+  }

+  comethod H(x: int)

+    ensures x < 100;

+  {  // error: postcondition violation (when _k == 0)

+    G(x);

+  }

+  

+  comethod A(x: int) { B(x); }

+  comethod B(x: int)

+  {

+    A#[10](x);  // error: this is a recursive call, and the termination metric may not be going down

+  }

+  

+  comethod A'(x: int) { B'(x); }

+  comethod B'(x: int)

+  {

+    if (10 < _k) {

+      A'#[10](x);

+    }

+  }

+  

+  comethod A''(x: int) { B''(x); }

+  comethod B''(x: int)

+  {

+    if (0 < x) {

+      A''#[_k](x-1);

+    }

+  }

+}

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