From 65de14b01e968fadbb011e28c25b7ea80c823639 Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@microsoft.com>
Date: Sun, 20 Jan 2013 15:36:14 -0800
Subject: More automatic co-induction for comethods

---
 Test/dafny3/Answer                |  2 +-
 Test/dafny3/SimpleCoinduction.dfy | 12 ++++++++++--
 2 files changed, 11 insertions(+), 3 deletions(-)

(limited to 'Test/dafny3')

diff --git a/Test/dafny3/Answer b/Test/dafny3/Answer
index c4e75986..418ca164 100644
--- a/Test/dafny3/Answer
+++ b/Test/dafny3/Answer
@@ -17,7 +17,7 @@ Dafny program verifier finished with 47 verified, 0 errors
 
 -------------------- SimpleCoinduction.dfy --------------------
 
-Dafny program verifier finished with 28 verified, 0 errors
+Dafny program verifier finished with 31 verified, 0 errors
 
 -------------------- CalcExample.dfy --------------------
 
diff --git a/Test/dafny3/SimpleCoinduction.dfy b/Test/dafny3/SimpleCoinduction.dfy
index 5a8ab288..cc92a6f1 100644
--- a/Test/dafny3/SimpleCoinduction.dfy
+++ b/Test/dafny3/SimpleCoinduction.dfy
@@ -64,7 +64,6 @@ copredicate True(s: Stream)
 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)
@@ -75,7 +74,16 @@ copredicate AlsoTrue(s: Stream)
 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
+}
+
+copredicate TT(y: int)
+{
+  TT(y+1)
+}
+
+comethod AlwaysTT(y: int)
+  ensures TT(y);
+{
 }
 
 // -----------------------------------------------------------------------
-- 
cgit v1.2.3