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/cloudmake/CloudMake-ConsistentBuilds.dfy | 24 ++++++++++++------------
 1 file changed, 12 insertions(+), 12 deletions(-)

(limited to 'Test/cloudmake')

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