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, 1 insertions, 1 deletions

diff --git a/Test/dafny1/FindZero.dfy b/Test/dafny1/FindZero.dfy
index f0eb6a60..0940d9e7 100644
--- a/Test/dafny1/FindZero.dfy
+++ b/Test/dafny1/FindZero.dfy
@@ -18,7 +18,7 @@ method FindZero(a: array<int>) returns (r: int)
   r := -1;

 }

 

-ghost method Lemma(a: array<int>, k: int, m: int)

+lemma Lemma(a: array<int>, k: int, m: int)

   requires a != null && forall i :: 0 <= i < a.Length ==> 0 <= a[i];

   requires forall i :: 0 <= i && i+1 < a.Length ==> a[i]-1 <= a[i+1];

   requires 0 <= k;