From f56e7c77e860f86e536f1695fbd7b28f78ee4322 Mon Sep 17 00:00:00 2001
From: Rustan Leino <unknown>
Date: Tue, 25 Feb 2014 18:30:50 -0800
Subject: Added examples mentioned in a paper on circular coinduction.

---
 Test/dafny4/Answer      |  4 +++
 Test/dafny4/Circ.dfy    | 84 +++++++++++++++++++++++++++++++++++++++++++++++++
 Test/dafny4/runtest.bat |  2 +-
 3 files changed, 89 insertions(+), 1 deletion(-)
 create mode 100644 Test/dafny4/Circ.dfy

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
-- 
cgit v1.2.3