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, 8 insertions, 8 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;

diff --git a/Test/dafny1/MoreInduction.dfy b/Test/dafny1/MoreInduction.dfy
index 41adcf50..319bb8d0 100644
--- a/Test/dafny1/MoreInduction.dfy
+++ b/Test/dafny1/MoreInduction.dfy
@@ -42,13 +42,13 @@ function ToSeq<X>(list: List<X>): seq<X>
     case Nary(nn) => ToSeq(nn) + ToSeq(rest)

 }

 

-ghost method Theorem<X>(list: List<X>)

+lemma Theorem<X>(list: List<X>)

   ensures ToSeq(list) == ToSeq(FlattenMain(list));

 {

   Lemma(list, Nil);

 }

 

-ghost method Lemma<X>(list: List<X>, ext: List<X>)

+lemma Lemma<X>(list: List<X>, ext: List<X>)

   requires IsFlat(ext);

   ensures ToSeq(list) + ToSeq(ext) == ToSeq(Flatten(list, ext));

 {

@@ -73,27 +73,27 @@ function NegFac(n: int): int
   if -1 <= n then -1 else - NegFac(n+1) * n

 }

 

-ghost method LemmaAll()

+lemma LemmaAll()

   ensures forall n :: NegFac(n) <= -1;  // error: induction heuristic does not give a useful well-founded order, and thus this fails to verify

 {

 }

 

-ghost method LemmaOne(n: int)

+lemma LemmaOne(n: int)

   ensures NegFac(n) <= -1;  // error: induction heuristic does not give a useful well-founded order, and thus this fails to verify

 {

 }

 

-ghost method LemmaAll_Neg()

+lemma LemmaAll_Neg()

   ensures forall n :: NegFac(-n) <= -1;  // error: fails to verify because of the minus in the trigger

 {

 }

 

-ghost method LemmaOne_Neg(n: int)

+lemma LemmaOne_Neg(n: int)

   ensures NegFac(-n) <= -1;  // error: fails to verify because of the minus in the trigger

 {

 }

 

-ghost method LemmaOneWithDecreases(n: int)

+lemma LemmaOneWithDecreases(n: int)

   ensures NegFac(n) <= -1;  // here, the programmer gives a good well-founded order, so this verifies

   decreases -n;

 {