Fixed the problem with the previous check-in.

1 files changed, 14 insertions, 8 deletions

diff --git a/Test/dafny0/CoPrefix.dfy b/Test/dafny0/CoPrefix.dfy
index 8cbe5394..991e160f 100644
--- a/Test/dafny0/CoPrefix.dfy
+++ b/Test/dafny0/CoPrefix.dfy
@@ -26,7 +26,7 @@ copredicate atmost(a: Stream, b: Stream)
   case Cons(h,t) => b.Cons? && h <= b.head && atmost(t, b.tail)

 }

 

-comethod Theorem0()

+comethod {:induction false} Theorem0()

   ensures atmost(zeros(), ones());

 {

   // the following shows two equivalent ways to getting essentially the

@@ -48,7 +48,7 @@ ghost method Theorem0_Manual()
 

 datatype Natural = Zero | Succ(Natural);

 

-comethod Theorem0_TerminationFailure_ExplicitDecreases(y: Natural)

+comethod {:induction false} Theorem0_TerminationFailure_ExplicitDecreases(y: Natural)

   ensures atmost(zeros(), ones());

   decreases y;

 {

@@ -62,7 +62,7 @@ comethod Theorem0_TerminationFailure_ExplicitDecreases(y: Natural)
   Theorem0_TerminationFailure_ExplicitDecreases#[_k-1](y);

 }

 

-comethod Theorem0_TerminationFailure_DefaultDecreases(y: Natural)

+comethod {:induction false} Theorem0_TerminationFailure_DefaultDecreases(y: Natural)

   ensures atmost(zeros(), ones());

 {

   match (y) {

@@ -80,7 +80,7 @@ ghost method {:induction true} Theorem0_Lemma(k: nat)
 {

 }

 

-comethod Theorem1()

+comethod {:induction false} Theorem1()

   ensures append(zeros(), ones()) == zeros();

 {

   Theorem1();

@@ -98,17 +98,17 @@ copredicate Pos(s: IList)
   s.head > 0 && Pos(s.tail)

 }

 

-comethod Theorem2(n: int)

+comethod {:induction false} Theorem2(n: int)

   requires 1 <= n;

   ensures Pos(UpIList(n));

 {

   Theorem2(n+1);

 }

 

-comethod Theorem2_NotAProof(n: int)

+comethod {:induction false} Theorem2_NotAProof(n: int)

   requires 1 <= n;

   ensures Pos(UpIList(n));

-{  // error: this is not a proof

+{  // error: this is not a proof (without automatic induction)

 }

 

 codatatype TList<T> = TCons(head: T, tail: TList);

@@ -125,7 +125,7 @@ function GG<T>(h: T): TList<T>
   TCons(h, GG(Next(h)))

 }

 

-comethod Compare<T>(h: T)

+comethod {:induction false} Compare<T>(h: T)

   ensures FF(h) == GG(h);

 {

   assert FF(h).head == GG(h).head;

@@ -142,3 +142,9 @@ comethod Compare<T>(h: T)
     case true =>

   }

 }

+

+comethod {:induction false} BadTheorem(s: IList)

+  ensures false;

+{  // error: postcondition violation

+  BadTheorem(s.tail);

+}