From 724cd08bb69546967483e13fdd1a7c7b9797f59b Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@microsoft.com>
Date: Sun, 20 Jan 2013 14:02:09 -0800
Subject: Added some co- test cases. Fixed some bugs.

---
 Test/dafny3/Answer                |   8 +++
 Test/dafny3/CalcExample.dfy       |  27 +++++++++
 Test/dafny3/SimpleCoinduction.dfy | 115 ++++++++++++++++++++++++++++++++++++++
 Test/dafny3/runtest.bat           |   5 +-
 4 files changed, 154 insertions(+), 1 deletion(-)
 create mode 100644 Test/dafny3/CalcExample.dfy
 create mode 100644 Test/dafny3/SimpleCoinduction.dfy

(limited to 'Test/dafny3')

diff --git a/Test/dafny3/Answer b/Test/dafny3/Answer
index 9cd8fc82..c4e75986 100644
--- a/Test/dafny3/Answer
+++ b/Test/dafny3/Answer
@@ -14,3 +14,11 @@ Dafny program verifier finished with 11 verified, 0 errors
 -------------------- CachedContainer.dfy --------------------
 
 Dafny program verifier finished with 47 verified, 0 errors
+
+-------------------- SimpleCoinduction.dfy --------------------
+
+Dafny program verifier finished with 28 verified, 0 errors
+
+-------------------- CalcExample.dfy --------------------
+
+Dafny program verifier finished with 6 verified, 0 errors
diff --git a/Test/dafny3/CalcExample.dfy b/Test/dafny3/CalcExample.dfy
new file mode 100644
index 00000000..c94c18d2
--- /dev/null
+++ b/Test/dafny3/CalcExample.dfy
@@ -0,0 +1,27 @@
+function f(x: int, y: int): int
+
+ghost method Associativity(x: int, y: int, z: int)
+  ensures f(x, f(y, z)) == f(f(x, y), z);
+
+ghost method Monotonicity(y: int, z: int)
+  requires y <= z;
+  ensures forall x :: f(x, y) <= f(x, z);
+
+ghost method DiagonalIdentity(x: int)
+  ensures f(x, x) == x;
+
+method M(a: int, b: int, c: int, x: int)
+  requires c <= x == f(a, b);
+{
+  calc {
+    f(a, f(b, c));
+    { Associativity(a, b, c); }
+    f(f(a, b), c);
+    { assert f(a, b) == x; }
+    f(x, c);
+    { assert c <= x; Monotonicity(c, x); }
+    <= f(x, x);
+    { DiagonalIdentity(x); }
+    x;
+  }
+}
diff --git a/Test/dafny3/SimpleCoinduction.dfy b/Test/dafny3/SimpleCoinduction.dfy
new file mode 100644
index 00000000..5a8ab288
--- /dev/null
+++ b/Test/dafny3/SimpleCoinduction.dfy
@@ -0,0 +1,115 @@
+codatatype Stream<T> = Cons(head: T, tail: Stream);
+codatatype IList<T> = Nil | ICons(head: T, tail: IList);
+
+// -----------------------------------------------------------------------
+
+copredicate Pos(s: Stream<int>)
+{
+  s.head > 0 && Pos(s.tail)
+}
+
+function Up(n: int): Stream<int>
+{
+  Cons(n, Up(n+1))
+}
+
+function Inc(s: Stream<int>): Stream<int>
+{
+  Cons(s.head + 1, Inc(s.tail))
+}
+
+ghost method {:induction false} UpLemma(k: nat, n: int)
+  ensures Inc(Up(n)) ==#[k] Up(n+1);
+{
+  if (k != 0) {
+    UpLemma(k-1, n+1);
+  }
+}
+
+comethod {:induction false} CoUpLemma(n: int)
+  ensures Inc(Up(n)) == Up(n+1);
+{
+  CoUpLemma(n+1);
+}
+
+ghost method UpLemma_Auto(k: nat, n: int)
+  ensures Inc(Up(n)) ==#[k] Up(n+1);
+{
+}
+
+comethod CoUpLemma_Auto(n: int)
+  ensures Inc(Up(n)) == Up(n+1);
+{
+}
+
+// -----------------------------------------------------------------------
+
+function Repeat(n: int): Stream<int>
+{
+  Cons(n, Repeat(n))
+}
+
+comethod RepeatLemma(n: int)
+  ensures Inc(Repeat(n)) == Repeat(n+1);
+{
+}
+
+// -----------------------------------------------------------------------
+
+copredicate True(s: Stream)
+{
+  True(s.tail)
+}
+
+comethod AlwaysTrue(s: Stream)
+  ensures True(s);
+{
+  AlwaysTrue(s.tail);  // WHY does this not happen automatically? (Because 's' is not quantified over)
+}
+
+copredicate AlsoTrue(s: Stream)
+{
+  AlsoTrue(s)
+}
+
+comethod AlsoAlwaysTrue(s: Stream)
+  ensures AlsoTrue(s);
+{
+  // AlsoAlwaysTrue(s);  // here, the recursive call is not needed, because it uses the same 's', so 's' does not need to be quantified over
+}
+
+// -----------------------------------------------------------------------
+
+function Append(M: IList, N: IList): IList
+{
+  match M
+  case Nil => N
+  case ICons(x, M') => ICons(x, Append(M', N))
+}
+
+function zeros(): IList<int>
+{
+  ICons(0, zeros())
+}
+
+function ones(): IList<int>
+{
+  ICons(1, ones())
+}
+
+copredicate AtMost(a: IList<int>, b: IList<int>)
+{
+  match a
+  case Nil => true
+  case ICons(h,t) => b.ICons? && h <= b.head && AtMost(t, b.tail)
+}
+
+comethod ZerosAndOnes_Theorem0()
+  ensures AtMost(zeros(), ones());
+{
+}
+
+comethod ZerosAndOnes_Theorem1()
+  ensures Append(zeros(), ones()) == zeros();
+{
+}
diff --git a/Test/dafny3/runtest.bat b/Test/dafny3/runtest.bat
index 2ebba74a..83d2bba9 100644
--- a/Test/dafny3/runtest.bat
+++ b/Test/dafny3/runtest.bat
@@ -4,7 +4,10 @@ setlocal
 set BINARIES=..\..\Binaries
 set DAFNY_EXE=%BINARIES%\Dafny.exe
 
-for %%f in (Iter.dfy Streams.dfy Dijkstra.dfy CachedContainer.dfy) do (
+for %%f in (
+  Iter.dfy Streams.dfy Dijkstra.dfy CachedContainer.dfy
+  SimpleCoinduction.dfy CalcExample.dfy
+) do (
   echo.
   echo -------------------- %%f --------------------
   %DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp %* %%f
-- 
cgit v1.2.3