From d3e8fdae367e29bc9fae675b3befe5a3bbc5daa0 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Tue, 22 Jan 2013 23:20:40 -0800 Subject: Examples from co-induction paper --- Test/dafny3/Answer | 12 +++ Test/dafny3/InductionVsCoinduction.dfy | 133 +++++++++++++++++++++++++++++++++ Test/dafny3/SimpleInduction.dfy | 85 +++++++++++++++++++++ Test/dafny3/Zip.dfy | 97 ++++++++++++++++++++++++ Test/dafny3/runtest.bat | 3 +- 5 files changed, 329 insertions(+), 1 deletion(-) create mode 100644 Test/dafny3/InductionVsCoinduction.dfy create mode 100644 Test/dafny3/SimpleInduction.dfy create mode 100644 Test/dafny3/Zip.dfy (limited to 'Test/dafny3') 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 = SNil | SCons(head: T, tail: Stream); + +/* + 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 +{ + 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 + 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) +{ + 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 = Nil | Cons(head: T, tail: List); + +function Append(xs: List, ys: List): List + 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 = 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 +{ + Cons(n, const(n)) +} + +function blink(): Stream +{ + 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 -------------------- -- cgit v1.2.3