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/dafny3/SimpleInduction.dfy | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

(limited to 'Test/dafny3/SimpleInduction.dfy')

diff --git a/Test/dafny3/SimpleInduction.dfy b/Test/dafny3/SimpleInduction.dfy
index 83ea6d14..8cf937e1 100644
--- a/Test/dafny3/SimpleInduction.dfy
+++ b/Test/dafny3/SimpleInduction.dfy
@@ -13,7 +13,7 @@ function Fib(n: nat): nat
   decreases n;
 { if n < 2 then n else Fib(n-2) + Fib(n-1) }
 
-ghost method FibLemma(n: nat)
+lemma FibLemma(n: nat)
   ensures Fib(n) % 2 == 0 <==> n % 3 == 0;
   decreases n;
 {
@@ -30,7 +30,7 @@ ghost method FibLemma(n: nat)
   satisfying 0 <= k < n, and in the second example, to all non-negative n. 
 */
 
-ghost method FibLemma_Alternative(n: nat)
+lemma FibLemma_Alternative(n: nat)
   ensures Fib(n) % 2 == 0 <==> n % 3 == 0;
 {
   forall k | 0 <= k < n {
@@ -38,7 +38,7 @@ ghost method FibLemma_Alternative(n: nat)
   }
 }
 
-ghost method FibLemma_All()
+lemma FibLemma_All()
   ensures forall n :: 0 <= n ==> (Fib(n) % 2 == 0 <==> n % 3 == 0);
 {
   forall n | 0 <= n {
@@ -48,8 +48,8 @@ ghost method FibLemma_All()
 
 /*
   A standard inductive definition of a generic List type and a function Append
-  that concatenates two lists.  The ghost method states the lemma that Append
-  is associative, and its recursive body gives the inductive proof. 
+  that concatenates two lists.  The lemma states that Append is associative,
+  and its recursive body gives the inductive proof.
   
   We omitted the explicit declaration and uses of the List type parameter in
   the signature of the method, since in simple cases like this, Dafny is able
@@ -68,7 +68,7 @@ function Append<T>(xs: List<T>, ys: List<T>): List<T>
 
 // The {:induction false} attribute disables automatic induction tactic,
 // so we can make the proof explicit.
-ghost method {:induction false} AppendIsAssociative(xs: List, ys: List, zs: List)
+lemma {:induction false} AppendIsAssociative(xs: List, ys: List, zs: List)
   ensures Append(Append(xs, ys), zs) == Append(xs, Append(ys, zs));
   decreases xs;
 {
@@ -81,7 +81,7 @@ ghost method {:induction false} AppendIsAssociative(xs: List, ys: List, zs: List
 
 // Here the proof is fully automatic - the body of the method is empty,
 // yet still verifies.
-ghost method AppendIsAssociative_Auto(xs: List, ys: List, zs: List)
+lemma AppendIsAssociative_Auto(xs: List, ys: List, zs: List)
   ensures Append(Append(xs, ys), zs) == Append(xs, Append(ys, zs));
 {
 }
-- 
cgit v1.2.3