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.

10 files changed, 66 insertions, 80 deletions

diff --git a/Test/cloudmake/CloudMake-ConsistentBuilds.dfy b/Test/cloudmake/CloudMake-ConsistentBuilds.dfy
index 815352f6..6d86607b 100644
--- a/Test/cloudmake/CloudMake-ConsistentBuilds.dfy
+++ b/Test/cloudmake/CloudMake-ConsistentBuilds.dfy
@@ -23,7 +23,7 @@ function Union(st: State, st': State): State
       (p in DomSt(st) ==> GetSt(p, result) == GetSt(p, st)) &&

       (p in DomSt(st') ==> GetSt(p, result) == GetSt(p, st'));

 

-ghost method StateEqualityProperty(st: State, st': State)

+lemma StateEqualityProperty(st: State, st': State)

   requires DomSt(st) == DomSt(st');

   requires forall p :: p in DomSt(st) ==> GetSt(p, st) == GetSt(p, st');

   ensures st == st';

@@ -60,7 +60,7 @@ function UpdateC(cmd: Expression, deps: Expression, exts: Expression, stC: State
     UpdateC(cmd, deps, exts', S(stC.st, c'))

 }

 

-ghost method UpdateCLemma(cmd: Expression, deps: Expression, exts: Expression, stC: StateC)

+lemma UpdateCLemma(cmd: Expression, deps: Expression, exts: Expression, stC: StateC)

   requires

     cmd.exprLiteral? && cmd.lit.litString? &&

     deps.exprLiteral? && deps.lit.litArrOfPaths? &&

@@ -136,7 +136,7 @@ function CombineC(stsC: set<StateC>): StateC
     UnionC(stC, CombineC(stsC - {stC}))

 }

 

-ghost method CombineCLemma(stsC: set<StateC>)

+lemma CombineCLemma(stsC: set<StateC>)

   requires stsC != {};

   requires forall stC :: stC in stsC ==> ConsistentCache(stC);

   ensures

@@ -174,7 +174,7 @@ function SetEnv(id: Identifier, expr: Expression, env: Env): Env
 /******* Primitive function 'exec' *******/

 function exec(cmd: Expression, deps: Expression, exts: Expression, st: State): Tuple<Expression, State>

 

-ghost method ExecProperty(cmd: Expression, deps: Expression, exts: Expression, st: State)

+lemma ExecProperty(cmd: Expression, deps: Expression, exts: Expression, st: State)

   requires

     cmd.exprLiteral? && cmd.lit.litString? &&

     deps.exprLiteral? && deps.lit.litArrOfPaths? &&

@@ -244,7 +244,7 @@ function execC(cmd: Expression, deps: Expression, exts: Expression, stC: StateC)
     Pair(expr', stC')

 }

 

-ghost method ExecCProperty(cmd: Expression, deps: Expression, exts: Expression, stC: StateC)

+lemma ExecCProperty(cmd: Expression, deps: Expression, exts: Expression, stC: StateC)

   requires

     cmd.exprLiteral? && cmd.lit.litString? &&

     deps.exprLiteral? && deps.lit.litArrOfPaths? &&

@@ -305,7 +305,7 @@ predicate PostC(cmd: Expression, deps: Expression, exts: Expression, stC: StateC
 

 function Hash(p: Path): HashValue

 

-ghost method HashProperty(cmd: Expression, deps: Expression, ext: string, cmd': Expression, deps': Expression, ext': string)

+lemma HashProperty(cmd: Expression, deps: Expression, ext: string, cmd': Expression, deps': Expression, ext': string)

   requires Hash(Loc(cmd, deps, ext)) == Hash(Loc(cmd', deps', ext'));

   ensures cmd == cmd' && deps == deps' && ext == ext';

 

@@ -509,7 +509,7 @@ predicate ValidArgsC(prim: Primitive, args: seq<Expression>, stC: StateC)
 }

 

 /******* {consistent_cache} buildC {no_bad_cache_error /\ consistent_cache} *******/

-ghost method CachedBuildsTheorem(prog: Program, stC: StateC)

+lemma CachedBuildsTheorem(prog: Program, stC: StateC)

   requires Legal(prog.stmts);

   requires ConsistentCache(stC);

   ensures

@@ -521,7 +521,7 @@ ghost method CachedBuildsTheorem(prog: Program, stC: StateC)
   BuildCLemma(prog, stC);

 }

 

-ghost method BuildCLemma(prog: Program, stC: StateC)

+lemma BuildCLemma(prog: Program, stC: StateC)

   requires Legal(prog.stmts);

   requires ConsistentCache(stC);

   ensures

@@ -532,7 +532,7 @@ ghost method BuildCLemma(prog: Program, stC: StateC)
   DoCLemma(prog.stmts, stC, EmptyEnv());

 }

 

-ghost method DoCLemma(stmts: seq<Statement>, stC: StateC, env: Env)

+lemma DoCLemma(stmts: seq<Statement>, stC: StateC, env: Env)

   requires Legal(stmts);

   requires ConsistentCache(stC);

   ensures

@@ -558,7 +558,7 @@ ghost method DoCLemma(stmts: seq<Statement>, stC: StateC, env: Env)
   }

 }

 

-ghost method {:induction expr} EvalCLemma(expr: Expression, stC: StateC, env: Env)

+lemma {:induction expr} EvalCLemma(expr: Expression, stC: StateC, env: Env)

   requires ConsistentCache(stC);

   ensures

     var result := evalC(expr, stC, env);

@@ -627,7 +627,7 @@ ghost method {:induction expr} EvalCLemma(expr: Expression, stC: StateC, env: En
   } else { }

 }

 

-ghost method EvalArgsCLemma(expr: Expression, args: seq<Expression>, stC: StateC, env: Env)

+lemma EvalArgsCLemma(expr: Expression, args: seq<Expression>, stC: StateC, env: Env)

   requires ConsistentCache(stC);

   requires forall arg :: arg in args ==> arg < expr;

   ensures

@@ -640,7 +640,7 @@ ghost method EvalArgsCLemma(expr: Expression, args: seq<Expression>, stC: StateC
   EvalArgsC'Lemma(expr, args, stC, env, [], {});

 }

 

-ghost method EvalArgsC'Lemma(expr: Expression, args: seq<Expression>, stC: StateC, env: Env,

+lemma EvalArgsC'Lemma(expr: Expression, args: seq<Expression>, stC: StateC, env: Env,

                              args': seq<Expression>, stsC': set<StateC>)

   requires ConsistentCache(stC);

   requires forall stC' :: stC' in stsC' ==> ConsistentCache(stC');

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;

 {

diff --git a/Test/dafny2/Calculations.dfy b/Test/dafny2/Calculations.dfy
index 8af0afe9..3870490f 100644
--- a/Test/dafny2/Calculations.dfy
+++ b/Test/dafny2/Calculations.dfy
@@ -41,12 +41,12 @@ function qreverse(l: List): List
 

 // Here are two lemmas about the List functions.

 

-ghost method Lemma_ConcatNil(xs : List)

+lemma Lemma_ConcatNil(xs : List)

   ensures concat(xs, Nil) == xs;

 {

 }

 

-ghost method Lemma_RevCatCommute(xs : List)

+lemma Lemma_RevCatCommute(xs : List)

   ensures forall ys, zs :: revacc(xs, concat(ys, zs)) == concat(revacc(xs, ys), zs);

 {

 }

@@ -55,7 +55,7 @@ ghost method Lemma_RevCatCommute(xs : List)
 // is given in a calculational style.  The proof is not minimal--some lines can be omitted

 // and Dafny will still fill in the details.

 

-ghost method Theorem_QReverseIsCorrect_Calc(l: List)

+lemma Theorem_QReverseIsCorrect_Calc(l: List)

   ensures qreverse(l) == reverse(l);

 {

   calc {

@@ -69,7 +69,7 @@ ghost method Theorem_QReverseIsCorrect_Calc(l: List)
   }

 }

 

-ghost method Lemma_Revacc_calc(xs: List, ys: List)

+lemma Lemma_Revacc_calc(xs: List, ys: List)

   ensures revacc(xs, ys) == concat(reverse(xs), ys);

 {

   match (xs) {

@@ -93,7 +93,7 @@ ghost method Lemma_Revacc_calc(xs: List, ys: List)
 

 // Here is a version of the same proof, as it was constructed before Dafny's "calc" construct.

 

-ghost method Theorem_QReverseIsCorrect(l: List)

+lemma Theorem_QReverseIsCorrect(l: List)

   ensures qreverse(l) == reverse(l);

 {

   assert qreverse(l)

@@ -105,7 +105,7 @@ ghost method Theorem_QReverseIsCorrect(l: List)
   Lemma_ConcatNil(reverse(l));

 }

 

-ghost method Lemma_Revacc(xs: List, ys: List)

+lemma Lemma_Revacc(xs: List, ys: List)

   ensures revacc(xs, ys) == concat(reverse(xs), ys);

 {

   match (xs) {

@@ -140,7 +140,7 @@ function Fib(n: nat): nat
   if n < 2 then n else Fib(n - 2) + Fib(n - 1)

 }

 

-ghost method Lemma_Fib()

+lemma Lemma_Fib()

   ensures Fib(5) < 6;

 {

   calc {

@@ -160,11 +160,11 @@ ghost method Lemma_Fib()
 /* List length */

 // Here are some proofs that show the use of nested calculations.

 

-ghost method Lemma_Concat_Length(xs: List, ys: List)

+lemma Lemma_Concat_Length(xs: List, ys: List)

   ensures length(concat(xs, ys)) == length(xs) + length(ys);

 {}

 

-ghost method Lemma_Reverse_Length(xs: List)

+lemma Lemma_Reverse_Length(xs: List)

   ensures length(xs) == length(reverse(xs));

 {

   match (xs) {

@@ -193,7 +193,7 @@ ghost method Lemma_Reverse_Length(xs: List)
   }

 }

 

-ghost method Window(xs: List, ys: List)

+lemma Window(xs: List, ys: List)

   ensures length(xs) == length(ys) ==> length(reverse(xs)) == length(reverse(ys));

 {

   calc {

@@ -221,11 +221,11 @@ function ith<a>(xs: List, i: nat): a
   case Cons(x, xrest) => if i == 0 then x else ith(xrest, i - 1)

 }

 

-ghost method lemma_zero_length(xs: List)

+lemma lemma_zero_length(xs: List)

   ensures length(xs) == 0 <==> xs.Nil?;

 {}

 

-ghost method lemma_extensionality(xs: List, ys: List)

+lemma lemma_extensionality(xs: List, ys: List)

   requires length(xs) == length(ys); // (0)

   requires forall i: nat | i < length(xs) :: ith(xs, i) == ith(ys, i); // (1)

   ensures xs == ys;

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;

 {

diff --git a/Test/dafny3/CalcExample.dfy b/Test/dafny3/CalcExample.dfy
index 2782d049..b9d3260b 100644
--- a/Test/dafny3/CalcExample.dfy
+++ b/Test/dafny3/CalcExample.dfy
@@ -3,14 +3,14 @@
 

 function f(x: int, y: int): int

 

-ghost method Associativity(x: int, y: int, z: int)

+lemma Associativity(x: int, y: int, z: int)

   ensures f(x, f(y, z)) == f(f(x, y), z);

 

-ghost method Monotonicity(y: int, z: int)

+lemma Monotonicity(y: int, z: int)

   requires y <= z;

   ensures forall x :: f(x, y) <= f(x, z);

 

-ghost method DiagonalIdentity(x: int)

+lemma DiagonalIdentity(x: int)

   ensures f(x, x) == x;

 

 method M(a: int, b: int, c: int, x: int)

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));

 {

 }

diff --git a/Test/dafny4/NipkowKlein-chapter3.dfy b/Test/dafny4/NipkowKlein-chapter3.dfy
index 725d68f6..3de6a5fc 100644
--- a/Test/dafny4/NipkowKlein-chapter3.dfy
+++ b/Test/dafny4/NipkowKlein-chapter3.dfy
@@ -195,9 +195,12 @@ lemma BsimpCorrect(b: bexp, s: state)
   ensures bval(bsimp(b), s) == bval(b, s)

 {

 /*  Here is one proof, which uses the induction hypothesis any anything smaller than b and also invokes

-    the lemma AsimpCorrect on anything smaller than b.

+    the lemma AsimpCorrect on every arithmetic expression.

   forall b' | b' < b { BsimpCorrect(b', s); } 

-  forall a' | a' < b { AsimpCorrect(a', s); }

+  forall a { AsimpCorrect(a, s); }

+    Yet another possibility is to mark the lemma with {:induction b} and to use the following line in

+    the body:

+  forall a { AsimpCorrect(a, s); }

 */

   // Here is another proof, which makes explicit the uses of the induction hypothesis and the other lemma.

   match b

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?;

 }