diff options
| author |  Rustan Leino <leino@microsoft.com> | 2013-01-22 23:20:40 -0800 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2013-01-22 23:20:40 -0800 |
| commit | d3e8fdae367e29bc9fae675b3befe5a3bbc5daa0 (patch) | |
| tree | c7b0992bbe1ff6fec231b3f34857201cbfa46a96 /Test/dafny3/Zip.dfy | |
| parent | 3934a2bf234377d26a199a3e7ae98c6eebf4a9ab (diff) | |
Examples from co-induction paper
Diffstat (limited to 'Test/dafny3/Zip.dfy')
| -rw-r--r-- | Test/dafny3/Zip.dfy | 97 |
1 files changed, 97 insertions, 0 deletions
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);
+}
|