diff options
| author |  Rustan Leino <unknown> | 2014-02-25 18:30:50 -0800 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2014-02-25 18:30:50 -0800 |
| commit | f56e7c77e860f86e536f1695fbd7b28f78ee4322 (patch) | |
| tree | 7b6854909cef545bd597191e70ed3a2b5ea662bd | |
| parent | f8f1e54a403e5b52bfc33fb43287b273e357488e (diff) | |
Added examples mentioned in a paper on circular coinduction.
| -rw-r--r-- | Test/dafny4/Answer | 4 | ||||
| -rw-r--r-- | Test/dafny4/Circ.dfy | 84 | ||||
| -rw-r--r-- | Test/dafny4/runtest.bat | 2 |
3 files changed, 89 insertions, 1 deletions
diff --git a/Test/dafny4/Answer b/Test/dafny4/Answer index 88a0a4c4..61eedf16 100644 --- a/Test/dafny4/Answer +++ b/Test/dafny4/Answer @@ -29,3 +29,7 @@ Dafny program verifier finished with 80 verified, 1 error -------------------- NumberRepresentations.dfy --------------------
Dafny program verifier finished with 33 verified, 0 errors
+
+-------------------- Circ.dfy --------------------
+
+Dafny program verifier finished with 16 verified, 0 errors
diff --git a/Test/dafny4/Circ.dfy b/Test/dafny4/Circ.dfy new file mode 100644 index 00000000..ab8d04e4 --- /dev/null +++ b/Test/dafny4/Circ.dfy @@ -0,0 +1,84 @@ +// A couple of examples from Grigore Rosu and Dorel Lucanu, "Circular coinduction: A proof theoretical
+// foundation", CALCO 2009.
+
+codatatype Stream<T> = Cons(head: T, tail: Stream)
+
+// ----- standard examples -----
+
+function zeros(): Stream<int> { Cons(0, zeros()) }
+function ones(): Stream<int> { Cons(1, ones()) }
+function blink(): Stream<int> { Cons(0, Cons(1, blink())) }
+function zip(a: Stream, b: Stream): Stream { Cons(a.head, zip(b, a.tail)) }
+
+colemma BlinkZipProperty()
+ ensures zip(zeros(), ones()) == blink();
+{
+}
+
+// ----- Thue-Morse sequence -----
+
+datatype Bit = O | I
+function bitnot(b: Bit): Bit
+{
+ if b == O then I else O
+}
+
+function not(s: Stream<Bit>): Stream<Bit>
+{
+ Cons(bitnot(s.head), not(s.tail))
+}
+
+/* Function morse() is essentially this:
+
+function morse(): Stream<int>
+{
+ Cons(0, morseTail())
+}
+function morseTail(): Stream<int>
+{
+ Cons(1, zip(morseTail(), not(morseTail())))
+}
+
+ * However, this definition of morseTail() is not allowed in Dafny, because it violates Dafny's
+ * syntactic guardedness checks. Instead, we give the defining properties of morse() and
+ * morseTail() as an axiom (that is, an unproved lemma).
+ */
+
+function morse(): Stream<Bit>
+function morseTail(): Stream<Bit>
+lemma MorseProperties()
+ ensures morse().head == O;
+ ensures morseTail() == morse().tail;
+ ensures morseTail().head == I;
+ ensures morseTail().tail == zip(morseTail(), not(morseTail()));
+
+// We will now define a function f and show that morse() is a fix-point of f.
+
+function f(s: Stream<Bit>): Stream<Bit>
+{
+ Cons(s.head, Cons(bitnot(s.head), f(s.tail)))
+}
+
+// The insightful property about f is that it satisfies the following property, which
+// we prove by co-induction.
+
+colemma FProperty(s: Stream<Bit>)
+ ensures f(s) == zip(s, not(s));
+{
+ calc {
+ zip(s, not(s));
+ // def. zip
+ Cons(s.head, zip(not(s), s.tail));
+ // def. zip
+ Cons(s.head, Cons(not(s).head, zip(s.tail, not(s).tail)));
+ }
+}
+
+// The fix-point theorem now follows easily.
+
+lemma Fixpoint()
+ ensures f(morse()) == morse();
+{
+ MorseProperties();
+ FProperty(morseTail());
+}
diff --git a/Test/dafny4/runtest.bat b/Test/dafny4/runtest.bat index 7160d9e2..c6778179 100644 --- a/Test/dafny4/runtest.bat +++ b/Test/dafny4/runtest.bat @@ -4,4 +4,4 @@ setlocal set BINARIES=..\..\Binaries
set DAFNY_EXE=%BINARIES%\Dafny.exe
-%DAFNY_EXE% /compile:0 /verifySeparately /dprint:out.dfy.tmp %* CoqArt-InsertionSort.dfy GHC-MergeSort.dfy Fstar-QuickSort.dfy Primes.dfy KozenSilva.dfy SoftwareFoundations-Basics.dfy NumberRepresentations.dfy
+%DAFNY_EXE% /compile:0 /verifySeparately /dprint:out.dfy.tmp %* CoqArt-InsertionSort.dfy GHC-MergeSort.dfy Fstar-QuickSort.dfy Primes.dfy KozenSilva.dfy SoftwareFoundations-Basics.dfy NumberRepresentations.dfy Circ.dfy
|