Renamed "ghost method" to "lemma" whenever appropriate (which is most of the time) in the test suite.

Removed some assertions that have been rendered unnecessary because of the computations that Dafny instructs the SMT solver to do.

2 files changed, 10 insertions, 10 deletions

diff --git a/Test/dafny3/CalcExample.dfy b/Test/dafny3/CalcExample.dfy
index 2782d049..b9d3260b 100644
--- a/Test/dafny3/CalcExample.dfy
+++ b/Test/dafny3/CalcExample.dfy
@@ -3,14 +3,14 @@
 

 function f(x: int, y: int): int

 

-ghost method Associativity(x: int, y: int, z: int)

+lemma Associativity(x: int, y: int, z: int)

   ensures f(x, f(y, z)) == f(f(x, y), z);

 

-ghost method Monotonicity(y: int, z: int)

+lemma Monotonicity(y: int, z: int)

   requires y <= z;

   ensures forall x :: f(x, y) <= f(x, z);

 

-ghost method DiagonalIdentity(x: int)

+lemma DiagonalIdentity(x: int)

   ensures f(x, x) == x;

 

 method M(a: int, b: int, c: int, x: int)

diff --git a/Test/dafny3/SimpleInduction.dfy b/Test/dafny3/SimpleInduction.dfy
index 83ea6d14..8cf937e1 100644
--- a/Test/dafny3/SimpleInduction.dfy
+++ b/Test/dafny3/SimpleInduction.dfy
@@ -13,7 +13,7 @@ function Fib(n: nat): nat
   decreases n;

 { if n < 2 then n else Fib(n-2) + Fib(n-1) }

 

-ghost method FibLemma(n: nat)

+lemma FibLemma(n: nat)

   ensures Fib(n) % 2 == 0 <==> n % 3 == 0;

   decreases n;

 {

@@ -30,7 +30,7 @@ ghost method FibLemma(n: nat)
   satisfying 0 <= k < n, and in the second example, to all non-negative n. 

 */

 

-ghost method FibLemma_Alternative(n: nat)

+lemma FibLemma_Alternative(n: nat)

   ensures Fib(n) % 2 == 0 <==> n % 3 == 0;

 {

   forall k | 0 <= k < n {

@@ -38,7 +38,7 @@ ghost method FibLemma_Alternative(n: nat)
   }

 }

 

-ghost method FibLemma_All()

+lemma FibLemma_All()

   ensures forall n :: 0 <= n ==> (Fib(n) % 2 == 0 <==> n % 3 == 0);

 {

   forall n | 0 <= n {

@@ -48,8 +48,8 @@ ghost method FibLemma_All()
 

 /*

   A standard inductive definition of a generic List type and a function Append

-  that concatenates two lists.  The ghost method states the lemma that Append

-  is associative, and its recursive body gives the inductive proof. 

+  that concatenates two lists.  The lemma states that Append is associative,

+  and its recursive body gives the inductive proof.

   

   We omitted the explicit declaration and uses of the List type parameter in

   the signature of the method, since in simple cases like this, Dafny is able

@@ -68,7 +68,7 @@ function Append<T>(xs: List<T>, ys: List<T>): List<T>
 

 // The {:induction false} attribute disables automatic induction tactic,

 // so we can make the proof explicit.

-ghost method {:induction false} AppendIsAssociative(xs: List, ys: List, zs: List)

+lemma {:induction false} AppendIsAssociative(xs: List, ys: List, zs: List)

   ensures Append(Append(xs, ys), zs) == Append(xs, Append(ys, zs));

   decreases xs;

 {

@@ -81,7 +81,7 @@ ghost method {:induction false} AppendIsAssociative(xs: List, ys: List, zs: List
 

 // Here the proof is fully automatic - the body of the method is empty,

 // yet still verifies.

-ghost method AppendIsAssociative_Auto(xs: List, ys: List, zs: List)

+lemma AppendIsAssociative_Auto(xs: List, ys: List, zs: List)

   ensures Append(Append(xs, ys), zs) == Append(xs, Append(ys, zs));

 {

 }