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.

1 files changed, 3 insertions, 3 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)