Deprecated "comethod" keyword in favor of "colemma". (Also, "prefix method" -> "prefix lemma")

5 files changed, 54 insertions, 54 deletions

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index a41cd0cd..f56af482 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -60,7 +60,7 @@ lemma M(x: int)
 {

 }

 

-comethod M'(x': int)

+colemma M'(x': int)

   ensures true;

 {

 }

@@ -1392,11 +1392,11 @@ CoResolution.dfy(64,10): Error: a copredicate is not allowed to declare any read
 CoResolution.dfy(70,31): Error: a copredicate is not allowed to declare any ensures clause

 CoResolution.dfy(79,20): Error: a recursive call from a copredicate can go only to other copredicates

 CoResolution.dfy(83,20): Error: a recursive call from a copredicate can go only to other copredicates

-CoResolution.dfy(92,4): Error: a recursive call from a comethod can go only to other comethods and prefix methods

-CoResolution.dfy(106,13): Error: a recursive call from a comethod can go only to other comethods and prefix methods

-CoResolution.dfy(107,13): Error: a recursive call from a comethod can go only to other comethods and prefix methods

-CoResolution.dfy(126,13): Error: a recursive call from a comethod can go only to other comethods and prefix methods

-CoResolution.dfy(127,13): Error: a recursive call from a comethod can go only to other comethods and prefix methods

+CoResolution.dfy(92,4): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas

+CoResolution.dfy(106,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas

+CoResolution.dfy(107,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas

+CoResolution.dfy(126,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas

+CoResolution.dfy(127,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas

 CoResolution.dfy(146,4): Error: a recursive call from a copredicate can go only to other copredicates

 CoResolution.dfy(148,4): Error: a recursive call from a copredicate can go only to other copredicates

 16 resolution/type errors detected in CoResolution.dfy

diff --git a/Test/dafny0/CoPrefix.dfy b/Test/dafny0/CoPrefix.dfy
index 06692314..7c010a09 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 {:induction false} Theorem0()

+colemma {: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 {:induction false} Theorem0_TerminationFailure_ExplicitDecreases(y: Natural)

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

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

   decreases y;

 {

@@ -62,7 +62,7 @@ comethod {:induction false} Theorem0_TerminationFailure_ExplicitDecreases(y: Nat
   Theorem0_TerminationFailure_ExplicitDecreases#[_k-1](y);

 }

 

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

+colemma {: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 {:induction false} Theorem1()

+colemma {:induction false} Theorem1()

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

 {

   Theorem1();

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

 }

 

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

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

   requires 1 <= n;

   ensures Pos(UpIList(n));

 {

   Theorem2(n+1);

 }

 

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

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

   requires 1 <= n;

   ensures Pos(UpIList(n));

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

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

 }

 

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

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

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

 {

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

@@ -143,7 +143,7 @@ comethod {:induction false} Compare<T>(h: T)
   }

 }

 

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

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

   ensures false;

 {  // error: postcondition violation

   BadTheorem(s.tail);

@@ -153,36 +153,36 @@ comethod {:induction false} BadTheorem(s: IList)
 

 // Make sure recursive calls get checked for termination

 module Recursion {

-  comethod X() { Y(); }

-  comethod Y() { X(); }

+  colemma X() { Y(); }

+  colemma Y() { X(); }

 

-  comethod G(x: int)

+  colemma G(x: int)

     ensures x < 100;

   {  // error: postcondition violation (when _k == 0)

     H(x);

   }

-  comethod H(x: int)

+  colemma H(x: int)

     ensures x < 100;

   {  // error: postcondition violation (when _k == 0)

     G(x);

   }

   

-  comethod A(x: int) { B(x); }

-  comethod B(x: int)

+  colemma A(x: int) { B(x); }

+  colemma B(x: int)

   {

     A#[10](x);  // error: this is a recursive call, and the termination metric may not be going down

   }

   

-  comethod A'(x: int) { B'(x); }

-  comethod B'(x: int)

+  colemma A'(x: int) { B'(x); }

+  colemma B'(x: int)

   {

     if (10 < _k) {

       A'#[10](x);

     }

   }

   

-  comethod A''(x: int) { B''(x); }

-  comethod B''(x: int)

+  colemma A''(x: int) { B''(x); }

+  colemma B''(x: int)

   {

     if (0 < x) {

       A''#[_k](x-1);

diff --git a/Test/dafny0/CoResolution.dfy b/Test/dafny0/CoResolution.dfy
index 9ab52d53..a7111a09 100644
--- a/Test/dafny0/CoResolution.dfy
+++ b/Test/dafny0/CoResolution.dfy
@@ -18,7 +18,7 @@ module TestModule {
     S#[_k](d)  // error: _k is not an identifier in scope

   }

 

-  comethod CM(d: set<int>)

+  colemma CM(d: set<int>)

   {

     var b;

     b := this.S#[5](d);

@@ -82,26 +82,26 @@ module Mojul1 {
   copredicate X() { Y() }

   copredicate Y() { X#[10]() }  // error: X is not allowed to depend on X#

 

-  comethod M()

+  colemma M()

   {

     N();

   }

-  comethod N()

+  colemma N()

   {

     Z();

-    W();  // error: not allowed to make co-recursive call to non-comethod

+    W();  // error: not allowed to make co-recursive call to non-colemma

   }

   ghost method Z() { }

   ghost method W() { M(); }

 

-  comethod G() { H(); }

-  comethod H() { G#[10](); }  // fine for comethod/prefix-method

+  colemma G() { H(); }

+  colemma H() { G#[10](); }  // fine for colemma/prefix-lemma

 }

 

 module CallGraph {

-  // comethod -> copredicate -> comethod

-  // comethod -> copredicate -> prefix method

-  comethod CoLemma(n: nat)

+  // colemma -> copredicate -> colemma

+  // colemma -> copredicate -> prefix lemma

+  colemma CoLemma(n: nat)

   {

     var q := Q(n);  // error

     var r := R(n);  // error

@@ -119,9 +119,9 @@ module CallGraph {
     false

   }

 

-  // comethod -> prefix predicate -> comethod

-  // comethod -> prefix predicate -> prefix method

-  comethod CoLemma_D(n: nat)

+  // colemma -> prefix predicate -> colemma

+  // colemma -> prefix predicate -> prefix lemma

+  colemma CoLemma_D(n: nat)

   {

     var q := Q_D#[n](n);  // error

     var r := R_D#[n](n);  // error

diff --git a/Test/dafny0/Coinductive.dfy b/Test/dafny0/Coinductive.dfy
index b31dc5be..27b279c3 100644
--- a/Test/dafny0/Coinductive.dfy
+++ b/Test/dafny0/Coinductive.dfy
@@ -133,7 +133,7 @@ module CoPredicateResolutionErrors {
 

 // --------------------------------------------------

 

-module UnfruitfulCoMethodConclusions {

+module UnfruitfulCoLemmaConclusions {

   codatatype Stream<T> = Cons(head: T, tail: Stream);

 

   copredicate Positive(s: Stream<int>)

@@ -141,13 +141,13 @@ module UnfruitfulCoMethodConclusions {
     s.head > 0 && Positive(s.tail)

   }

 

-  comethod BadTheorem(s: Stream)

+  colemma BadTheorem(s: Stream)

     ensures false;

   {

     BadTheorem(s.tail);

   }

 

-  comethod CM(s: Stream<int>)

+  colemma CM(s: Stream<int>)

     ensures true && !false;

     ensures s.head == 8 ==> Positive(s);

     ensures s.tail == s;

diff --git a/Test/dafny0/CoinductiveProofs.dfy b/Test/dafny0/CoinductiveProofs.dfy
index b7dea89d..d3112233 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 {:induction false} PosLemma0(n: int)

+colemma {:induction false} PosLemma0(n: int)

   requires 1 <= n;

   ensures Pos(Upward(n));

 {

   PosLemma0(n + 1);  // this completes the proof

 }

 

-comethod {:induction false} PosLemma1(n: int)

+colemma {:induction false} PosLemma1(n: int)

   requires 1 <= n;

   ensures Pos(Upward(n));

 {

@@ -27,7 +27,7 @@ comethod {:induction false} PosLemma1(n: int)
   }

 }

 

-comethod {:induction false} Outside_CoMethod_Caller_PosLemma(n: int)

+colemma {:induction false} Outside_CoLemma_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 {:induction false} AlwaysLemma_X0(s: Stream)

+colemma {: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 {:induction false} AlwaysLemma_X1(s: Stream)

+colemma {: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 {:induction false} AlwaysLemma_X2(s: Stream)

+colemma {: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 {:induction false} AlwaysLemma_Y0(s: Stream)

+colemma {: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 {:induction false} AlwaysLemma_Y1(s: Stream)

+colemma {:induction false} AlwaysLemma_Y1(s: Stream)

   ensures Y(s);

 {  // error: this is not the right proof

   AlwaysLemma_Y1(s);

 }

 

-comethod {:induction false} AlwaysLemma_Y2(s: Stream)

+colemma {:induction false} AlwaysLemma_Y2(s: Stream)

   ensures Y(s);

 {

   AlwaysLemma_Y2(s.tail);

@@ -103,7 +103,7 @@ copredicate Z(s: Stream)
   false

 }

 

-comethod {:induction false} AlwaysLemma_Z(s: Stream)

+colemma {: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 {:induction false} Lemma0(n: int)

+colemma {: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 {:induction false} Lemma1(n: int)

+colemma {:induction false} Lemma1(n: int)

   ensures Even(UpwardBy2(2*n));

 {

   Lemma1(n+1);

 }

 

-comethod {:induction false} ProveEquality(n: int)

+colemma {:induction false} ProveEquality(n: int)

   ensures Doubles(n) == UpwardBy2(2*n);

 {

   ProveEquality(n+1);

 }

 

-comethod {:induction false} BadEquality0(n: int)

+colemma {:induction false} BadEquality0(n: int)

   ensures Doubles(n) == UpwardBy2(n);

 {  // error: postcondition does not hold

   BadEquality0(n+1);

 }

 

-comethod {:induction false} BadEquality1(n: int)

+colemma {:induction false} BadEquality1(n: int)

   ensures Doubles(n) == UpwardBy2(n+1);

 {  // error: postcondition does not hold

   BadEquality1(n+1);