From 3cfa0049262a9d547f061937d5c452afb2033401 Mon Sep 17 00:00:00 2001
From: Rustan Leino <unknown>
Date: Tue, 28 Jul 2015 14:27:29 -0700
Subject: 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.

---
 Test/dafny1/FindZero.dfy      |  2 +-
 Test/dafny1/MoreInduction.dfy | 14 +++++++-------
 2 files changed, 8 insertions(+), 8 deletions(-)

(limited to 'Test/dafny1')

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;
 {
-- 
cgit v1.2.3