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

diff --git a/Test/dafny2/MajorityVote.dfy b/Test/dafny2/MajorityVote.dfy
index 51e5b968..f1c3b485 100644
--- a/Test/dafny2/MajorityVote.dfy
+++ b/Test/dafny2/MajorityVote.dfy
@@ -165,7 +165,7 @@ method SearchForWinner<Candidate(==)>(a: seq<Candidate>, ghost hasWinner: bool,
 

 // Here are two lemmas about Count that are used in the methods above.

 

-ghost method Lemma_Split<T>(a: seq<T>, s: int, t: int, u: int, x: T)

+lemma Lemma_Split<T>(a: seq<T>, s: int, t: int, u: int, x: T)

   requires 0 <= s <= t <= u <= |a|;

   ensures Count(a, s, t, x) + Count(a, t, u, x) == Count(a, s, u, x);

 {

@@ -178,7 +178,7 @@ ghost method Lemma_Split<T>(a: seq<T>, s: int, t: int, u: int, x: T)
   */

 }

 

-ghost method Lemma_Unique<T>(a: seq<T>, s: int, t: int, x: T, y: T)

+lemma Lemma_Unique<T>(a: seq<T>, s: int, t: int, x: T, y: T)

   requires 0 <= s <= t <= |a|;

   ensures x != y ==> Count(a, s, t, x) + Count(a, s, t, y) <= t - s;

 {