Examples from co-induction paper

5 files changed, 329 insertions, 1 deletions

diff --git a/Test/dafny3/Answer b/Test/dafny3/Answer
index 418ca164..8812f389 100644
--- a/Test/dafny3/Answer
+++ b/Test/dafny3/Answer
@@ -15,6 +15,10 @@ Dafny program verifier finished with 11 verified, 0 errors
 

 Dafny program verifier finished with 47 verified, 0 errors

 

+-------------------- SimpleInduction.dfy --------------------

+

+Dafny program verifier finished with 12 verified, 0 errors

+

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

 

 Dafny program verifier finished with 31 verified, 0 errors

@@ -22,3 +26,11 @@ Dafny program verifier finished with 31 verified, 0 errors
 -------------------- CalcExample.dfy --------------------

 

 Dafny program verifier finished with 6 verified, 0 errors

+

+-------------------- InductionVsCoinduction.dfy --------------------

+

+Dafny program verifier finished with 20 verified, 0 errors

+

+-------------------- Zip.dfy --------------------

+

+Dafny program verifier finished with 24 verified, 0 errors

diff --git a/Test/dafny3/InductionVsCoinduction.dfy b/Test/dafny3/InductionVsCoinduction.dfy
new file mode 100644
index 00000000..26e57c7f
--- /dev/null
+++ b/Test/dafny3/InductionVsCoinduction.dfy
@@ -0,0 +1,133 @@
+// A definition of a co-inductive datatype Stream, whose values are possibly

+// infinite lists.

+codatatype Stream<T> = SNil | SCons(head: T, tail: Stream<T>);

+

+/*

+  A function that returns a stream consisting of all integers upwards of n.

+  The self-call sits in a productive position and is therefore not subject to

+  termination checks.  The Dafny compiler turns this co-recursive call into a

+  lazily evaluated call, evaluated at the time during the program execution

+  when the SCons is destructed (if ever).

+*/

+

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

+{

+  SCons(n, Up(n+1))

+}

+

+/*

+  A function that returns a stream consisting of all multiples

+  of 5 upwards of n.  Note that the first self-call sits in a

+  productive position and is thus co-recursive.  The second self-call

+  is not in a productive position and therefore it is subject to

+  termination checking; in particular, each recursive call must

+  decrease the specific variant function.

+ */

+

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

+  decreases (n + 4) / 5 * 5 - n;

+{

+  if n % 5 == 0 then SCons(n, FivesUp(n+1))

+  else FivesUp(n+1)

+}

+

+// A co-predicate that holds for those integer streams where every value is greater than 0.

+copredicate Pos(s: Stream<int>)

+{

+  match s

+  case SNil => true

+  case SCons(x, rest) => x > 0 && Pos(rest)

+}

+

+// SAppend looks almost exactly like Append, but cannot have 'decreases'

+// clause, as it is possible it will never terminate.

+function SAppend(xs: Stream, ys: Stream): Stream

+{

+  match xs

+  case SNil => ys

+  case SCons(x, rest) => SCons(x, SAppend(rest, ys))

+}

+

+/*

+  Example: associativity of append on streams.

+

+  The first method proves that append is associative when we consider first

+  \S{k} elements of the resulting streams.  Equality is treated as any other

+  recursive co-predicate, and has it k-th unfolding denoted as ==#[k].

+

+  The second method invokes the first one for all ks, which lets us prove the

+  assertion (included for clarity only).  The assertion implies the

+  postcondition (by (F_=)).  Interestingly, in the SNil case in the first

+  method, we actually prove ==, but by (F_=) applied in the opposite direction

+  we also get ==#[k].

+*/

+

+ghost method {:induction false} SAppendIsAssociativeK(k:nat, a:Stream, b:Stream, c:Stream)

+  ensures SAppend(SAppend(a, b), c) ==#[k] SAppend(a, SAppend(b, c));

+  decreases k;

+{

+  match (a) {

+  case SNil =>

+  case SCons(h, t) => if (k > 0) { SAppendIsAssociativeK(k - 1, t, b, c); }

+  }

+}

+

+ghost method SAppendIsAssociative(a:Stream, b:Stream, c:Stream)

+  ensures SAppend(SAppend(a, b), c) == SAppend(a, SAppend(b, c));

+{

+  parallel (k:nat) { SAppendIsAssociativeK(k, a, b, c); }

+  // assert for clarity only, postcondition follows directly from it

+  assert (forall k:nat :: SAppend(SAppend(a, b), c) ==#[k] SAppend(a, SAppend(b, c)));

+}

+

+// Equivalent proof using the comethod syntax.

+comethod {:induction false} SAppendIsAssociativeC(a:Stream, b:Stream, c:Stream)

+  ensures SAppend(SAppend(a, b), c) == SAppend(a, SAppend(b, c));

+{

+  match (a) {

+  case SNil =>

+  case SCons(h, t) => SAppendIsAssociativeC(t, b, c);

+  }

+}

+

+// In fact the proof can be fully automatic.

+comethod SAppendIsAssociative_Auto(a:Stream, b:Stream, c:Stream)

+  ensures SAppend(SAppend(a, b), c) == SAppend(a, SAppend(b, c));

+{

+}

+

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

+  requires n > 0;

+  ensures Pos(Up(n));

+{

+  UpPos(n+1);

+}

+

+comethod UpPos_Auto(n:int)

+  requires n > 0;

+  ensures Pos(Up(n));

+{

+}

+

+// This does induction and coinduction in the same proof.

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

+  requires n > 0;

+  ensures Pos(FivesUp(n));

+  decreases (n + 4) / 5 * 5 - n;

+{

+  if (n % 5 == 0) {

+    FivesUpPos#[_k - 1](n + 1);

+  } else {

+    FivesUpPos#[_k](n + 1);

+  }

+}

+

+// Again, Dafny can just employ induction tactic and do it automatically.

+// The only hint required is the decrease clause.

+comethod FivesUpPos_Auto(n:int)

+  requires n > 0;

+  ensures Pos(FivesUp(n));

+  decreases (n + 4) / 5 * 5 - n;

+{

+}

+

diff --git a/Test/dafny3/SimpleInduction.dfy b/Test/dafny3/SimpleInduction.dfy
new file mode 100644
index 00000000..5331b808
--- /dev/null
+++ b/Test/dafny3/SimpleInduction.dfy
@@ -0,0 +1,85 @@
+/*

+  The well-known Fibonacci function defined in Dafny.  The postcondition of

+  method FibLemma states a property about Fib, and the body of the method is

+  code that convinces the program verifier that the postcondition does indeed

+  hold.  Thus, effectively, the method states a lemma and its body gives the

+  proof.

+  */

+

+function Fib(n: nat): nat

+  decreases n;

+{ if n < 2 then n else Fib(n-2) + Fib(n-1) }

+

+ghost method FibLemma(n: nat)

+  ensures Fib(n) % 2 == 0 <==> n % 3 == 0;

+  decreases n;

+{

+  if (n < 2) {

+  } else {

+    FibLemma(n-2);

+    FibLemma(n-1);

+  }

+}

+

+/*

+  The 'parallel' statement has the effect of applying its body simultaneously

+  to all values of the bound variables---in the first example, to all k

+  satisfying 0 <= k < n, and in the second example, to all non-negative n. 

+*/

+

+ghost method FibLemma_Alternative(n: nat)

+  ensures Fib(n) % 2 == 0 <==> n % 3 == 0;

+{

+  parallel (k | 0 <= k < n) {

+    FibLemma_Alternative(k);

+  }

+}

+

+ghost method FibLemma_All()

+  ensures forall n :: 0 <= n ==> (Fib(n) % 2 == 0 <==> n % 3 == 0);

+{

+  parallel (n | 0 <= n) {

+    FibLemma(n);

+  }

+}

+

+/*

+  A standard inductive definition of a generic List type and a function Append

+  that concatenates two lists.  The ghost method states the lemma that Append

+  is associative, and its recursive body gives the inductive proof. 

+  

+  We omitted the explicit declaration and uses of the List type parameter in

+  the signature of the method, since in simple cases like this, Dafny is able

+  to fill these in automatically.

+  */

+

+datatype List<T> = Nil | Cons(head: T, tail: List<T>);

+

+function Append<T>(xs: List<T>, ys: List<T>): List<T>

+  decreases xs;

+{

+  match xs

+  case Nil => ys

+  case Cons(x, rest) => Cons(x, Append(rest, ys))

+}

+

+// The {:induction false} attribute disables automatic induction tactic,

+// so we can make the proof explicit.

+ghost method {:induction false} AppendIsAssociative(xs: List, ys: List, zs: List)

+  ensures Append(Append(xs, ys), zs) == Append(xs, Append(ys, zs));

+  decreases xs;

+{

+  match (xs) {

+    case Nil =>

+    case Cons(x, rest) =>

+      AppendIsAssociative(rest, ys, zs);

+  }

+}

+

+// Here the proof is fully automatic - the body of the method is empty,

+// yet still verifies.

+ghost method AppendIsAssociative_Auto(xs: List, ys: List, zs: List)

+  ensures Append(Append(xs, ys), zs) == Append(xs, Append(ys, zs));

+{

+}

+

diff --git a/Test/dafny3/Zip.dfy b/Test/dafny3/Zip.dfy
new file mode 100644
index 00000000..371b012a
--- /dev/null
+++ b/Test/dafny3/Zip.dfy
@@ -0,0 +1,97 @@
+/*

+Here, we define infinite streams with some functions and prove a few

+properties, drawing from:

+

+  Daniel Hausmann, Till Mossakowski and Lutz Schroder:

+  Iterative Circular Coinduction for CoCasl in Isabelle/HOL.

+

+Some proofs are automatic (EvenZipLemma), whereas some others require a single

+recursive call to be made explicitly.

+

+Note that the automatically inserted parallel statement

+is in principle strong enough in all cases above, but the incompletness

+of reasoning with quantifiers in SMT solvers make the explicit calls

+necessary.

+*/

+

+codatatype Stream<T> = Cons(hd: T, tl: Stream);

+

+function zip(xs: Stream, ys: Stream): Stream

+  { Cons(xs.hd, Cons(ys.hd, zip(xs.tl, ys.tl))) }

+function even(xs: Stream): Stream

+  { Cons(xs.hd, even(xs.tl.tl)) }

+function odd(xs: Stream): Stream

+  { even(xs.tl) }

+

+comethod EvenOddLemma(xs: Stream)

+  ensures zip(even(xs), odd(xs)) == xs;

+{ EvenOddLemma(xs.tl.tl); }

+

+comethod EvenZipLemma(xs:Stream, ys:Stream)

+  ensures even(zip(xs, ys)) == xs;

+{ /* Automatic. */ }

+

+function bzip(xs: Stream, ys: Stream, f:bool) : Stream

+  { if f then Cons(xs.hd, bzip(xs.tl, ys, !f))

+    else      Cons(ys.hd, bzip(xs, ys.tl, !f)) }

+

+comethod BzipZipLemma(xs:Stream, ys:Stream)

+  ensures zip(xs, ys) == bzip(xs, ys, true);

+{ BzipZipLemma(xs.tl, ys.tl); }

+

+

+/*

+   More examples from CoCasl.

+ */

+

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

+{

+  Cons(n, const(n))

+}

+

+function blink(): Stream<int>

+{

+  Cons(0, Cons(1, blink()))

+}

+

+comethod BzipBlinkLemma()

+  ensures zip(const(0), const(1)) == blink();

+{

+  BzipBlinkLemma(); 

+}

+

+

+function zip2(xs: Stream, ys: Stream): Stream

+{ 

+  Cons(xs.hd, zip2(ys, xs.tl))

+}

+

+comethod Zip201Lemma()

+  ensures zip2(const(0), const(1)) == blink();

+{

+  Zip201Lemma();

+}

+

+comethod ZipZip2Lemma(xs:Stream, ys:Stream)

+  ensures zip(xs, ys) == zip2(xs, ys);

+{

+  ZipZip2Lemma(xs.tl, ys.tl);

+}

+

+function bswitch(xs: Stream, f:bool) : Stream

+{

+  if f then Cons(xs.tl.hd, bswitch(Cons(xs.hd, xs.tl.tl), !f))

+  else      Cons(xs.hd,      bswitch(xs.tl, !f))

+}

+

+comethod BswitchLemma(xs:Stream)

+  ensures zip(odd(xs), even(xs)) == bswitch(xs, true);

+{

+  BswitchLemma(xs.tl.tl);

+}

+

+comethod Bswitch2Lemma(xs:Stream, ys:Stream)

+  ensures zip(xs, ys) == bswitch(zip(ys, xs), true);

+{

+  Bswitch2Lemma(xs.tl, ys.tl);

+}

diff --git a/Test/dafny3/runtest.bat b/Test/dafny3/runtest.bat
index 83d2bba9..aeffee89 100644
--- a/Test/dafny3/runtest.bat
+++ b/Test/dafny3/runtest.bat
@@ -6,7 +6,8 @@ set DAFNY_EXE=%BINARIES%\Dafny.exe
 

 for %%f in (

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

-  SimpleCoinduction.dfy CalcExample.dfy

+  SimpleInduction.dfy SimpleCoinduction.dfy CalcExample.dfy

+  InductionVsCoinduction.dfy Zip.dfy

 ) do (

   echo.

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