From d2d89cd3ce7fabaa597ada1a7749944353e46d0a Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@microsoft.com>
Date: Fri, 18 Jan 2013 22:45:50 -0800
Subject: Fixed the problem with the previous check-in.

---
 Test/dafny0/CoinductiveProofs.dfy | 30 +++++++++++++++---------------
 1 file changed, 15 insertions(+), 15 deletions(-)

(limited to 'Test/dafny0/CoinductiveProofs.dfy')

diff --git a/Test/dafny0/CoinductiveProofs.dfy b/Test/dafny0/CoinductiveProofs.dfy
index 47c5f262..b7dea89d 100644
--- a/Test/dafny0/CoinductiveProofs.dfy
+++ b/Test/dafny0/CoinductiveProofs.dfy
@@ -10,14 +10,14 @@ copredicate Pos(s: Stream<int>)
   0 < s.head && Pos(s.tail)
 }
 
-comethod PosLemma0(n: int)
+comethod {:induction false} PosLemma0(n: int)
   requires 1 <= n;
   ensures Pos(Upward(n));
 {
   PosLemma0(n + 1);  // this completes the proof
 }
 
-comethod PosLemma1(n: int)
+comethod {:induction false} PosLemma1(n: int)
   requires 1 <= n;
   ensures Pos(Upward(n));
 {
@@ -27,7 +27,7 @@ comethod PosLemma1(n: int)
   }
 }
 
-comethod Outside_CoMethod_Caller_PosLemma(n: int)
+comethod {:induction false} Outside_CoMethod_Caller_PosLemma(n: int)
   requires 1 <= n;
   ensures Pos(Upward(n));
 {
@@ -51,19 +51,19 @@ copredicate X(s: Stream)  // this is equivalent to always returning 'true'
   X(s)
 }
 
-comethod AlwaysLemma_X0(s: Stream)
+comethod {:induction false} AlwaysLemma_X0(s: Stream)
   ensures X(s);  // prove that X(s) really is always 'true'
 {  // error: this is not the right proof
   AlwaysLemma_X0(s.tail);
 }
 
-comethod AlwaysLemma_X1(s: Stream)
+comethod {:induction false} AlwaysLemma_X1(s: Stream)
   ensures X(s);  // prove that X(s) really is always 'true'
 {
   AlwaysLemma_X1(s);  // this is the right proof
 }
 
-comethod AlwaysLemma_X2(s: Stream)
+comethod {:induction false} AlwaysLemma_X2(s: Stream)
   ensures X(s);
 {
   AlwaysLemma_X2(s);
@@ -77,19 +77,19 @@ copredicate Y(s: Stream)  // this is equivalent to always returning 'true'
   Y(s.tail)
 }
 
-comethod AlwaysLemma_Y0(s: Stream)
+comethod {:induction false} AlwaysLemma_Y0(s: Stream)
   ensures Y(s);  // prove that Y(s) really is always 'true'
 {
   AlwaysLemma_Y0(s.tail);  // this is a correct proof
 }
 
-comethod AlwaysLemma_Y1(s: Stream)
+comethod {:induction false} AlwaysLemma_Y1(s: Stream)
   ensures Y(s);
 {  // error: this is not the right proof
   AlwaysLemma_Y1(s);
 }
 
-comethod AlwaysLemma_Y2(s: Stream)
+comethod {:induction false} AlwaysLemma_Y2(s: Stream)
   ensures Y(s);
 {
   AlwaysLemma_Y2(s.tail);
@@ -103,7 +103,7 @@ copredicate Z(s: Stream)
   false
 }
 
-comethod AlwaysLemma_Z(s: Stream)
+comethod {:induction false} AlwaysLemma_Z(s: Stream)
   ensures Z(s);  // says, perversely, that Z(s) is always 'true'
 {  // error: this had better not lead to a proof
   AlwaysLemma_Z(s);
@@ -119,7 +119,7 @@ copredicate Even(s: Stream<int>)
   s.head % 2 == 0 && Even(s.tail)
 }
 
-comethod Lemma0(n: int)
+comethod {:induction false} Lemma0(n: int)
   ensures Even(Doubles(n));
 {
   Lemma0(n+1);
@@ -130,25 +130,25 @@ function UpwardBy2(n: int): Stream<int>
   Cons(n, UpwardBy2(n + 2))
 }
 
-comethod Lemma1(n: int)
+comethod {:induction false} Lemma1(n: int)
   ensures Even(UpwardBy2(2*n));
 {
   Lemma1(n+1);
 }
 
-comethod ProveEquality(n: int)
+comethod {:induction false} ProveEquality(n: int)
   ensures Doubles(n) == UpwardBy2(2*n);
 {
   ProveEquality(n+1);
 }
 
-comethod BadEquality0(n: int)
+comethod {:induction false} BadEquality0(n: int)
   ensures Doubles(n) == UpwardBy2(n);
 {  // error: postcondition does not hold
   BadEquality0(n+1);
 }
 
-comethod BadEquality1(n: int)
+comethod {:induction false} BadEquality1(n: int)
   ensures Doubles(n) == UpwardBy2(n+1);
 {  // error: postcondition does not hold
   BadEquality1(n+1);
-- 
cgit v1.2.3