Fixed the problem with the previous check-in.

1 files changed, 15 insertions, 15 deletions

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);