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, 17 insertions, 34 deletions

diff --git a/Test/vstte2012/Combinators.dfy b/Test/vstte2012/Combinators.dfy
index be7bc25f..ba4a4141 100644
--- a/Test/vstte2012/Combinators.dfy
+++ b/Test/vstte2012/Combinators.dfy
@@ -170,7 +170,7 @@ function IsTerminal(t: Term): bool
 

 // The following theorem states the correctness of the FindAndStep function:

 

-ghost method Theorem_FindAndStep(t: Term)

+lemma Theorem_FindAndStep(t: Term)

   // If FindAndStep returns the term it started from, then there is no

   // way to take a step.  More precisely, there is no C[u] == t for which the

   // Step applies to "u".

@@ -194,7 +194,7 @@ ghost method Theorem_FindAndStep(t: Term)
 // computes the value of FindAndStep(t) as it goes along and it returns

 // that value.

 

-ghost method Lemma_FindAndStep(t: Term) returns (r: Term, C: Context, u: Term)

+lemma Lemma_FindAndStep(t: Term) returns (r: Term, C: Context, u: Term)

   ensures r == FindAndStep(t);

   ensures r == t ==> IsTerminal(t);

   ensures r != t ==>

@@ -255,7 +255,7 @@ ghost method Lemma_FindAndStep(t: Term) returns (r: Term, C: Context, u: Term)
 // The proof of the lemma above used one more lemma, namely one that enumerates

 // lays out the options for how to represent a term as a C[u] pair.

 

-ghost method Lemma_ContextPossibilities(t: Term)

+lemma Lemma_ContextPossibilities(t: Term)

   ensures forall C,u :: IsContext(C) && t == EvalExpr(C, u) ==>

     (C == Hole && t == u) ||

     (t.Apply? && exists D :: C == C_term(D, t.cdr) && t.car == EvalExpr(D, u)) ||

@@ -442,7 +442,7 @@ function method ks(n: nat): Term
 // VerificationTask2) it computes the same thing as method VerificationTask2

 // does.

 

-ghost method VerificationTask3()

+lemma VerificationTask3()

   ensures forall n: nat ::

     TerminatingReduction(ks(n)) == if n % 2 == 0 then K else Apply(K, K);

 {

@@ -451,13 +451,13 @@ ghost method VerificationTask3()
   }

 }

 

-ghost method VT3(n: nat)

+lemma VT3(n: nat)

   ensures TerminatingReduction(ks(n)) == if n % 2 == 0 then K else Apply(K, K);

 {

   // Dafny's (way cool) induction tactic kicks in and proves the following

   // assertion automatically:

   assert forall p :: 2 <= p ==> FindAndStep(ks(p)) == ks(p-2);

-  // And then Dafny's (cool beyond words) induction tactic for ghost methods kicks

+  // And then Dafny's (cool beyond words) induction tactic for lemmas kicks

   // in to prove the postcondition.  (If this got you curious, scope out Leino's

   // VMCAI 2012 paper "Automating Induction with an SMT Solver".)

 }

diff --git a/Test/vstte2012/Tree.dfy b/Test/vstte2012/Tree.dfy
index 4a45d011..a346aac5 100644
--- a/Test/vstte2012/Tree.dfy
+++ b/Test/vstte2012/Tree.dfy
@@ -75,7 +75,7 @@ function method build(s: seq<int>): Result
 }

 

 

-// This ghost methods encodes the main lemma for the

+// This is the main lemma for the

 // completeness theorem. If a sequence s starts with a

 // valid encoding of a tree t then build_rec yields a

 // result (i.e., does not fail) and the rest of the sequence.

@@ -83,8 +83,8 @@ function method build(s: seq<int>): Result
 // induction on t. Dafny proves termination (using the

 // height of the term t as termination measure), which

 // ensures that the induction hypothesis is applied

-// correctly (encoded by calls to this ghost method).

-ghost method lemma0(t: Tree, d: int, s: seq<int>)

+// correctly (encoded by calls to this lemma).

+lemma lemma0(t: Tree, d: int, s: seq<int>)

   ensures build_rec(d, toList(d, t) + s).Res? &&

           build_rec(d, toList(d, t) + s).sOut == s;

 {

@@ -100,13 +100,13 @@ ghost method lemma0(t: Tree, d: int, s: seq<int>)
 }

 

 

-// This ghost method encodes a lemma that states the

+// This lemma states the

 // completeness property. It is proved by applying the

 // main lemma (lemma0). In this lemma, the bound variables

 // of the completeness theorem are passed as arguments;

-// the following two ghost methods replace these arguments

+// the following two lemmas replace these arguments

 // by quantified variables.

-ghost method lemma1(t: Tree, s:seq<int>)

+lemma lemma1(t: Tree, s:seq<int>)

   requires s == toList(0, t) + [];

   ensures  build(s).Res?;

 {

@@ -114,9 +114,9 @@ ghost method lemma1(t: Tree, s:seq<int>)
 }

 

 

-// This ghost method encodes a lemma that introduces the

-// existential quantifier in the completeness property.

-ghost method lemma2(s: seq<int>)

+// This lemma introduces the existential quantifier in the completeness

+// property.

+lemma lemma2(s: seq<int>)

   ensures (exists t: Tree :: toList(0,t) == s) ==> build(s).Res?;

 {

   forall t | toList(0,t) == s {

@@ -125,12 +125,12 @@ ghost method lemma2(s: seq<int>)
 }

 

 

-// This ghost method encodes the completeness theorem.

+// This lemma encodes the completeness theorem.

 // For each sequence for which there is a corresponding

 // tree, function build yields a result different from Fail.

 // The body of the method converts the argument of lemma2

 // into a universally quantified variable.

-ghost method completeness()

+lemma completeness()

   ensures forall s: seq<int> :: ((exists t: Tree :: toList(0,t) == s) ==> build(s).Res?);

 {

   forall s {

@@ -147,19 +147,6 @@ method harness0()
   ensures build([1,3,3,2]).Res? &&

           build([1,3,3,2]).t == Node(Leaf, Node(Node(Leaf, Leaf), Leaf));

 {

-  assert build_rec(2, [2]) ==

-         Res(Leaf, []);

-  assert build_rec(2, [3,3,2]) ==

-         Res(Node(Leaf, Leaf), [2]);

-  assert build_rec(1, [3,3,2]) ==

-         Res(Node(Node(Leaf, Leaf), Leaf), []);

-  assert build_rec(1, [1,3,3,2]) ==

-         Res(Leaf, [3,3,2]);

-  assert build_rec(0, [1,3,3,2]) ==

-         Res(

-           Node(build_rec(1, [1,3,3,2]).t,

-                build_rec(1, [3,3,2]).t),

-           []);

 }

 

 

@@ -170,8 +157,4 @@ method harness0()
 method harness1()

   ensures build([1,3,2,2]).Fail?;

 {

-  assert build_rec(1,[1,3,2,2]) == Res(Leaf, [3,2,2]);

-  assert build_rec(3,[2,2]).Fail?;

-  assert build_rec(2,[3,2,2]).Fail?;

-  assert build_rec(1,[3,2,2]).Fail?;

 }