Commit aa89bbde authored by Martin Clochard's avatar Martin Clochard
Browse files

example double-wp: use strong invariant instead of correctness predicates

parent 31ab7518
......@@ -24,8 +24,8 @@ module Compile_aexpr
meta rewrite_def function aexpr_post
let rec compile_aexpr (a:aexpr) : hl 'a
ensures { result <% (trivial_pre,aexpr_post a result.code.length) }
ensures { hl_correctness result }
ensures { result.pre --> trivial_pre }
ensures { result.post --> aexpr_post a result.code.length }
variant { a }
= let c = match a with
| Anum n -> $ iconstf n
......@@ -74,9 +74,9 @@ module Compile_bexpr
meta rewrite_def function exec_cond
let rec compile_bexpr (b:bexpr) (cond:bool) (ofs:ofs) : hl 'a
ensures { let len = result.code.length in
result <% (trivial_pre,bexpr_post b cond (len + ofs) len) }
ensures { hl_correctness result }
ensures { result.pre --> trivial_pre }
ensures { result.post --> let len = result.code.length in
bexpr_post b cond (len + ofs) len }
variant { b }
= let c = match b with
| Btrue -> $ if cond then ibranchf ofs else inil ()
......@@ -164,9 +164,8 @@ module Compile_com
(forall pk sk mk. var (VMS pk sk mk) (VMS pi si mi) -> mk = mj)
let rec compile_com (cmd: com) : hl 'a
ensures { hl_correctness result }
ensures { let len = result.code.length in
result <% (com_pre cmd,com_post cmd len) }
ensures { result.pre --> com_pre cmd }
ensures { result.post --> let len = result.code.length in com_post cmd len }
variant { cmd }
= let res = match cmd with
| Cskip -> $ inil ()
......
This diff is collapsed.
......@@ -4,62 +4,62 @@
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../imp.why">
<theory name="Imp" sum="2d3400b438aea0519cb1313c5cfda33e">
<theory name="Imp" sum="4a862357dfae5a0041230517e577addf">
<goal name="ceval_deterministic_aux">
<transf name="induction_pr">
<goal name="ceval_deterministic_aux.1" expl="1.">
<transf name="simplify_trivial_quantification_in_goal">
<goal name="ceval_deterministic_aux.1.1" expl="1.">
<proof prover="0"><result status="valid" time="0.02" steps="41"/></proof>
<proof prover="0"><result status="valid" time="0.02" steps="39"/></proof>
</goal>
</transf>
</goal>
<goal name="ceval_deterministic_aux.2" expl="2.">
<transf name="simplify_trivial_quantification_in_goal">
<goal name="ceval_deterministic_aux.2.1" expl="1.">
<proof prover="0"><result status="valid" time="0.33" steps="473"/></proof>
<proof prover="0"><result status="valid" time="0.13" steps="224"/></proof>
</goal>
</transf>
</goal>
<goal name="ceval_deterministic_aux.3" expl="3.">
<transf name="simplify_trivial_quantification_in_goal">
<goal name="ceval_deterministic_aux.3.1" expl="1.">
<proof prover="0"><result status="valid" time="0.23" steps="391"/></proof>
<proof prover="0"><result status="valid" time="0.23" steps="384"/></proof>
</goal>
</transf>
</goal>
<goal name="ceval_deterministic_aux.4" expl="4.">
<transf name="simplify_trivial_quantification_in_goal">
<goal name="ceval_deterministic_aux.4.1" expl="1.">
<proof prover="0"><result status="valid" time="0.06" steps="157"/></proof>
<proof prover="0"><result status="valid" time="0.06" steps="146"/></proof>
</goal>
</transf>
</goal>
<goal name="ceval_deterministic_aux.5" expl="5.">
<transf name="simplify_trivial_quantification_in_goal">
<goal name="ceval_deterministic_aux.5.1" expl="1.">
<proof prover="0"><result status="valid" time="0.06" steps="153"/></proof>
<proof prover="0"><result status="valid" time="0.06" steps="147"/></proof>
</goal>
</transf>
</goal>
<goal name="ceval_deterministic_aux.6" expl="6.">
<transf name="simplify_trivial_quantification_in_goal">
<goal name="ceval_deterministic_aux.6.1" expl="1.">
<proof prover="0"><result status="valid" time="0.03" steps="50"/></proof>
<proof prover="0"><result status="valid" time="0.03" steps="44"/></proof>
</goal>
</transf>
</goal>
<goal name="ceval_deterministic_aux.7" expl="7.">
<transf name="simplify_trivial_quantification_in_goal">
<goal name="ceval_deterministic_aux.7.1" expl="1.">
<proof prover="0"><result status="valid" time="0.28" steps="444"/></proof>
<proof prover="0"><result status="valid" time="0.28" steps="405"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="ceval_deterministic">
<proof prover="0"><result status="valid" time="0.01" steps="27"/></proof>
<proof prover="0"><result status="valid" time="0.01" steps="25"/></proof>
</goal>
</theory>
</file>
......
......@@ -32,19 +32,15 @@ module Compiler_logic
type pre 'a = 'a -> pos -> pred
type post 'a = 'a -> pos -> rel
(* Machine transition valid whatever the global code is. *)
predicate contextual_irrelevance (c:code) (p:pos) (ms1 ms2:machine_state) =
forall c_glob. codeseq_at c_glob p c -> transition_star c_glob ms1 ms2
(* Hoare triples with explicit pre & post *)
type hl 'a = { code: code; ghost pre : pre {'a}; ghost post: post {'a} }
(* (<%): pack the pre/post rewriting.
lock is an artifact to prevent unrolling of
h's definition recursively. *)
let function lock () : (int,int) =
ensures { result = (0,0) }
while false do variant { 0 } () done; (0,0)
predicate (<%) (h:hl 'a) (x:(pre 'a,post 'a)) =
let (pr,ps) = x in
h --> { code = let (_,_) = lock () in h.code; pre = pr; post = ps }
meta rewrite_def predicate (<%)
(* (Total) correctness for hoare triple. *)
invariant { forall x:'a,p ms. pre x p ms ->
exists ms'. post x p ms ms' /\ contextual_irrelevance code p ms ms' }
(* Predicate transformer type. Same auxiliary variables as for
Hoare triples. *)
......@@ -52,20 +48,9 @@ module Compiler_logic
(* Code with backward predicate transformer. *)
type wp 'a = { wcode : code; ghost wp : wp_trans {'a} }
(* Machine transition valid whatever the global code is. *)
predicate contextual_irrelevance (c:code) (p:pos) (ms1 ms2:machine_state) =
forall c_glob. codeseq_at c_glob p c -> transition_star c_glob ms1 ms2
(* (Total) correctness for hoare triple. *)
predicate hl_correctness (cs:hl 'a) =
forall x:'a,p ms. cs.pre x p ms ->
exists ms'. cs.post x p ms ms' /\ contextual_irrelevance cs.code p ms ms'
(* Similar definition for backward predicate transformers *)
predicate wp_correctness (code:wp 'a) =
forall x:'a,p post ms. (code.wp x p post) ms ->
exists ms'. post ms' /\ contextual_irrelevance code.wcode p ms ms'
(* Similar invariant for backward predicate transformers *)
invariant { forall x:'a,p post ms. wp x p post ms ->
exists ms'. post ms' /\ contextual_irrelevance wcode p ms ms' }
(* WP combinator for sequence. Similar to the standard WP calculus
for sequence. The initial machine state is memorized in auxiliary
......@@ -81,10 +66,8 @@ module Compiler_logic
(* Code combinator for sequence, with wp. *)
let (--) (s1 : wp 'a) (s2 : wp ('a, machine_state)) : wp 'a
requires { wp_correctness s1 /\ wp_correctness s2 }
ensures { result.wcode.length = s1.wcode.length + s2.wcode.length }
ensures { result.wcode.length --> s1.wcode.length + s2.wcode.length }
ensures { result.wp --> seq_wp s1.wcode.length s1.wp s2.wp }
ensures { wp_correctness result }
= let code = s1.wcode ++ s2.wcode in
let res = { wcode = code; wp = seq_wp s1.wcode.length s1.wp s2.wp } in
assert { forall x: 'a, p post ms. res.wp x p post ms ->
......@@ -106,9 +89,8 @@ module Compiler_logic
Similar to WP calculus for (if cond then s). *)
let (%) (s:wp 'a) (ghost cond:pre {'a}) : wp 'a
requires { wp_correctness s }
ensures { result.wp --> fork_wp s.wp cond }
ensures { result.wcode.length = s.wcode.length /\ wp_correctness result }
ensures { result.wcode.length --> s.wcode.length }
= { wcode = s.wcode; wp = fork_wp s.wp cond }
(* WP transformer for hoare triples. *)
......@@ -118,26 +100,23 @@ module Compiler_logic
lemma towp_wp_lemma:
forall pr ps, x:'a, p q ms. towp_wp pr ps x p q ms =
(pr x p ms && (forall ms'. ps x p ms ms' -> q ms'))
meta rewrite lemma towp_wp_lemma
(* Unwrap code with hoare triple into code with wp.
Analogous to procedure call/abstract block. *)
let ($_) (c:hl 'a) : wp 'a
requires { hl_correctness c }
ensures { result.wcode.length = c.code.length }
ensures { result.wcode.length --> c.code.length }
ensures { result.wp --> towp_wp c.pre c.post }
ensures { wp_correctness result }
= { wcode = c.code; wp = towp_wp c.pre c.post }
(* Equip code with pre/post-condition. That is here that proof happen.
(P -> wp (c,Q)). Anologous to checking function/abstract block
specification. *)
let hoare (ghost pre:pre {'a}) (c:wp 'a) (ghost post:post {'a}) : hl 'a
requires { wp_correctness c }
requires { forall x p ms. pre x p ms -> (c.wp x p (post x p ms)) ms }
ensures { result <% (pre,post) }
ensures { result.code.length = c.wcode.length /\ hl_correctness result}
ensures { result.pre --> pre }
ensures { result.post --> post }
ensures { result.code.length --> c.wcode.length }
= { code = c.wcode ; pre = pre; post = post }
function trivial_pre : pre 'a = fun _ p ms -> let VMS p' _ _ = ms in p = p'
......@@ -175,15 +154,13 @@ module Compiler_logic
(* Code combinator for looping construct. *)
let make_loop (c:wp 'a) (ghost inv cont:pre {'a})
(ghost var:post {'a}) : wp 'a
requires { wp_correctness c }
ensures { result.wp --> loop_wp c.wp inv cont var }
ensures { wp_correctness result }
ensures { result.wcode.length = c.wcode.length }
= let res = { wcode = c.wcode; wp = loop_wp c.wp inv cont var } in
assert { forall x p q ms0. res.wp x p q ms0 ->
ensures { result.wcode.length --> c.wcode.length }
= let wpt = loop_wp c.wp inv cont var in
assert { forall x p q ms0. wpt x p q ms0 ->
forall ms. inv x p ms -> acc (var x p) ms ->
exists ms'. contextual_irrelevance res.wcode p ms ms' /\ q ms'
exists ms'. contextual_irrelevance c.wcode p ms ms' /\ q ms'
};
res
{ wcode = c.wcode; wp = wpt }
end
......@@ -4,27 +4,25 @@
<why3session shape_version="4">
<prover id="0" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="1.30" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="2" name="Z3" version="4.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../logic.mlw">
<theory name="Compiler_logic" sum="bbb4f6b95cf0f6f786305cc906cdbf54">
<goal name="VC lock" expl="VC for lock">
<proof prover="1"><result status="valid" time="0.01" steps="5"/></proof>
</goal>
<theory name="Compiler_logic" sum="ae5a0bf29b55ad0f369f0131f351d52a">
<goal name="seq_wp_lemma">
<proof prover="1"><result status="valid" time="0.02" steps="5"/></proof>
</goal>
<goal name="VC infix --" expl="VC for infix --">
<transf name="split_goal_wp">
<goal name="VC infix --.1" expl="1. assertion">
<proof prover="1"><result status="valid" time="0.05" steps="71"/></proof>
<goal name="VC infix --.1" expl="1. precondition">
<proof prover="1"><result status="valid" time="0.02" steps="69"/></proof>
</goal>
<goal name="VC infix --.2" expl="2. postcondition">
<proof prover="1"><result status="valid" time="0.03" steps="8"/></proof>
<goal name="VC infix --.2" expl="2. assertion">
<proof prover="1"><result status="valid" time="0.05" steps="15"/></proof>
</goal>
<goal name="VC infix --.3" expl="3. postcondition">
<proof prover="1"><result status="valid" time="0.02" steps="5"/></proof>
<proof prover="1"><result status="valid" time="0.02" steps="14"/></proof>
</goal>
<goal name="VC infix --.4" expl="4. postcondition">
<proof prover="1"><result status="valid" time="0.02" steps="20"/></proof>
<proof prover="1"><result status="valid" time="0.03" steps="8"/></proof>
</goal>
</transf>
</goal>
......@@ -38,7 +36,7 @@
<proof prover="1"><result status="valid" time="0.04" steps="13"/></proof>
</goal>
<goal name="VC prefix $" expl="VC for prefix $">
<proof prover="1"><result status="valid" time="0.05" steps="11"/></proof>
<proof prover="1"><result status="valid" time="0.05" steps="17"/></proof>
</goal>
<goal name="VC hoare" expl="VC for hoare">
<proof prover="0"><result status="valid" time="0.07"/></proof>
......@@ -58,7 +56,7 @@
<goal name="VC make_loop.1.1.1" expl="1. assertion">
<transf name="simplify_trivial_quantification_in_goal">
<goal name="VC make_loop.1.1.1.1" expl="1. VC for make_loop">
<proof prover="0"><result status="valid" time="0.25"/></proof>
<proof prover="2"><result status="valid" time="0.03"/></proof>
</goal>
</transf>
</goal>
......@@ -66,14 +64,14 @@
</goal>
</transf>
</goal>
<goal name="VC make_loop.2" expl="2. postcondition">
<proof prover="1"><result status="valid" time="0.02" steps="5"/></proof>
<goal name="VC make_loop.2" expl="2. precondition">
<proof prover="1"><result status="valid" time="0.02" steps="10"/></proof>
</goal>
<goal name="VC make_loop.3" expl="3. postcondition">
<proof prover="1"><result status="valid" time="0.05" steps="12"/></proof>
<proof prover="1"><result status="valid" time="0.05" steps="7"/></proof>
</goal>
<goal name="VC make_loop.4" expl="4. postcondition">
<proof prover="1"><result status="valid" time="0.02" steps="5"/></proof>
<proof prover="1"><result status="valid" time="0.02" steps="7"/></proof>
</goal>
</transf>
</goal>
......
......@@ -20,8 +20,9 @@ module VM_instr_spec
(ghost f:machine_state -> machine_state) : hl 'a
requires { forall c p. codeseq_at c p code_f ->
forall x ms. pre x p ms -> transition c ms (f ms) }
ensures { result <% (pre,ifun_post f) }
ensures { result.code = code_f /\ hl_correctness result }
ensures { result.pre --> pre }
ensures { result.post --> ifun_post f }
ensures { result.code --> code_f }
= let res = { pre = pre; code = code_f; post = ifun_post f } in
assert { forall x p ms. res.pre x p ms ->
not (exists ms' : machine_state. res.post x p ms ms' /\
......@@ -39,8 +40,9 @@ module VM_instr_spec
meta rewrite_def function iconst_fun
let iconstf (n: int) : hl 'a
ensures { result <% (trivial_pre,iconst_post n) }
ensures { result.code.length = 1 /\ hl_correctness result }
ensures { result.pre --> trivial_pre }
ensures { result.post --> iconst_post n }
ensures { result.code.length --> 1 }
= hoare trivial_pre ($ ifunf trivial_pre n.iconst n.iconst_fun) n.iconst_post
(* Ivar spec *)
......@@ -53,8 +55,9 @@ module VM_instr_spec
meta rewrite_def function ivar_fun
let ivarf (x: id) : hl 'a
ensures { result <% (trivial_pre,ivar_post x) }
ensures { result.code.length = 1 /\ hl_correctness result }
ensures { result.pre --> trivial_pre }
ensures { result.post --> ivar_post x }
ensures { result.code.length --> 1 }
= hoare trivial_pre ($ ifunf trivial_pre x.ivar x.ivar_fun) x.ivar_post
(* Binary arithmetic operators specification (Iadd, Isub, Imul)
......@@ -81,8 +84,9 @@ module VM_instr_spec
requires { forall c p. codeseq_at c p code_b ->
forall n1 n2 s m. transition c (VMS p (push n2 (push n1 s)) m)
(VMS (p+1) (push (op n1 n2) s) m) }
ensures { result <% (ibinop_pre,ibinop_post op) }
ensures { result.code.length = code_b.length /\ hl_correctness result }
ensures { result.pre --> ibinop_pre }
ensures { result.post --> ibinop_post op }
ensures { result.code.length --> code_b.length }
= hoare ibinop_pre ($ ifunf ibinop_pre code_b op.ibinop_fun) op.ibinop_post
constant plus : binop = fun x y -> x + y
......@@ -95,18 +99,21 @@ module VM_instr_spec
meta rewrite_def function mul
let iaddf () : hl 'a
ensures { result <% (ibinop_pre,ibinop_post plus) }
ensures { result.code.length = 1 /\ hl_correctness result }
ensures { result.pre --> ibinop_pre }
ensures { result.post --> ibinop_post plus }
ensures { result.code.length --> 1 }
= create_binop iadd plus
let isubf () : hl 'a
ensures { result <% (ibinop_pre,ibinop_post sub) }
ensures { result.code.length = 1 /\ hl_correctness result }
ensures { result.pre --> ibinop_pre }
ensures { result.post --> ibinop_post sub }
ensures { result.code.length --> 1 }
= create_binop isub sub
let imulf () : hl 'a
ensures { result <% (ibinop_pre,ibinop_post mul) }
ensures { result.code.length = 1 /\ hl_correctness result }
ensures { result.pre --> ibinop_pre }
ensures { result.post --> ibinop_post mul }
ensures { result.code.length --> 1 }
= create_binop imul mul
(* Inil spec *)
......@@ -115,8 +122,9 @@ module VM_instr_spec
meta rewrite_def function inil_post
let inil () : hl 'a
ensures { result <% (trivial_pre,inil_post) }
ensures { result.code.length = 0 /\ hl_correctness result }
ensures { result.pre --> trivial_pre }
ensures { result.post --> inil_post }
ensures { result.code.length --> 0 }
= { pre = trivial_pre; code = Nil; post = inil_post }
(* Ibranch specification *)
......@@ -129,8 +137,9 @@ module VM_instr_spec
meta rewrite_def function ibranch_fun
let ibranchf (ofs:ofs) : hl 'a
ensures { result <% (trivial_pre,ibranch_post ofs) }
ensures { result.code.length = 1 /\ hl_correctness result }
ensures { result.pre --> trivial_pre }
ensures { result.post --> ibranch_post ofs }
ensures { result.code.length --> 1 }
= let cf = $ ifunf trivial_pre (ibranch ofs) (ibranch_fun ofs) in
hoare trivial_pre cf (ibranch_post ofs)
......@@ -155,8 +164,9 @@ module VM_instr_spec
requires { forall c p1 n1 n2 s m. codeseq_at c p1 code_cd ->
let p2 = (if cond n1 n2 then p1 + ofs + 1 else p1 + 1) in
transition c (VMS p1 (push n2 (push n1 s)) m) (VMS p2 s m) }
ensures { result <% (ibinop_pre,icjump_post cond ofs) }
ensures { result.code.length = code_cd.length /\ hl_correctness result }
ensures { result.pre --> ibinop_pre }
ensures { result.post --> icjump_post cond ofs }
ensures { result.code.length --> code_cd.length }
= let c = $ ifunf ibinop_pre code_cd (icjump_fun cond ofs) in
hoare ibinop_pre c (icjump_post cond ofs)
......@@ -174,23 +184,27 @@ module VM_instr_spec
meta rewrite_def function bgt
let ibeqf (ofs:ofs) : hl 'a
ensures { result <% (ibinop_pre,icjump_post beq ofs) }
ensures { result.code.length = 1 /\ hl_correctness result }
ensures { result.pre --> ibinop_pre }
ensures { result.post --> icjump_post beq ofs }
ensures { result.code.length --> 1 }
= create_cjump (ibeq ofs) beq ofs
let ibnef (ofs:ofs) : hl 'a
ensures { result <% (ibinop_pre,icjump_post bne ofs) }
ensures { result.code.length = 1 /\ hl_correctness result }
ensures { result.pre --> ibinop_pre }
ensures { result.post --> icjump_post bne ofs }
ensures { result.code.length --> 1 }
= create_cjump (ibne ofs) bne ofs
let iblef (ofs:ofs) : hl 'a
ensures { result <% (ibinop_pre,icjump_post ble ofs) }
ensures { result.code.length = 1 /\ hl_correctness result }
ensures { result.pre --> ibinop_pre }
ensures { result.post --> icjump_post ble ofs }
ensures { result.code.length --> 1 }
= create_cjump (ible ofs) ble ofs
let ibgtf (ofs:ofs) : hl 'a
ensures { result <% (ibinop_pre,icjump_post bgt ofs) }
ensures { result.code.length = 1 /\ hl_correctness result }
ensures { result.pre --> ibinop_pre }
ensures { result.post --> icjump_post bgt ofs }
ensures { result.code.length --> 1 }
= create_cjump (ibgt ofs) bgt ofs
(* Isetvar specification *)
......@@ -211,8 +225,9 @@ module VM_instr_spec
meta rewrite_def function isetvar_fun
let isetvarf (x: id) : hl 'a
ensures { result <% (isetvar_pre,isetvar_post x) }
ensures { result.code.length = 1 /\ hl_correctness result }
ensures { result.pre --> isetvar_pre }
ensures { result.post --> isetvar_post x }
ensures { result.code.length --> 1 }
= let c = $ ifunf isetvar_pre (isetvar x) (isetvar_fun x) in
hoare isetvar_pre c (isetvar_post x)
......
......@@ -5,68 +5,68 @@
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="1" name="Eprover" version="1.8-001" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../specs.mlw">
<theory name="VM_instr_spec" sum="e1714e6c495913e6af15b7ca2491573b">
<theory name="VM_instr_spec" sum="17c08329fc66ca05a14a3a537fb64283">
<goal name="VC ifunf" expl="VC for ifunf">
<transf name="split_goal_wp">
<goal name="VC ifunf.1" expl="1. assertion">
<goal name="VC ifunf.1" expl="1. precondition">
<proof prover="1"><result status="valid" time="0.25"/></proof>
</goal>
<goal name="VC ifunf.2" expl="2. assertion">
<transf name="split_goal_wp">
<goal name="VC ifunf.1.1" expl="1. assertion">
<proof prover="0"><result status="valid" time="0.03" steps="17"/></proof>
<goal name="VC ifunf.2.1" expl="1. assertion">
<proof prover="0"><result status="valid" time="0.03" steps="20"/></proof>
</goal>
<goal name="VC ifunf.1.2" expl="2. assertion">
<proof prover="0"><result status="valid" time="0.02" steps="8"/></proof>
<goal name="VC ifunf.2.2" expl="2. assertion">
<proof prover="0"><result status="valid" time="0.02" steps="11"/></proof>
</goal>
</transf>
</goal>
<goal name="VC ifunf.2" expl="2. postcondition">
<proof prover="0"><result status="valid" time="0.05" steps="6"/></proof>
</goal>
<goal name="VC ifunf.3" expl="3. postcondition">
<proof prover="0"><result status="valid" time="0.04" steps="9"/></proof>
<proof prover="0"><result status="valid" time="0.05" steps="8"/></proof>
</goal>
<goal name="VC ifunf.4" expl="4. postcondition">
<proof prover="0"><result status="valid" time="0.04" steps="8"/></proof>
</goal>
<goal name="VC ifunf.5" expl="5. postcondition">
<proof prover="0"><result status="valid" time="0.04" steps="8"/></proof>
</goal>
</transf>
</goal>
<goal name="VC iconstf" expl="VC for iconstf">
<transf name="split_goal_wp">
<goal name="VC iconstf.1" expl="1. precondition">
<proof prover="1"><result status="valid" time="1.00"/></proof>
<proof prover="1"><result status="valid" time="0.52"/></proof>
</goal>
<goal name="VC iconstf.2" expl="2. precondition">
<proof prover="0"><result status="valid" time="0.05" steps="8"/></proof>
<proof prover="0"><result status="valid" time="0.08" steps="30"/></proof>
</goal>
<goal name="VC iconstf.3" expl="3. precondition">
<proof prover="0"><result status="valid" time="0.05" steps="11"/></proof>
<goal name="VC iconstf.3" expl="3. postcondition">
<proof prover="0"><result status="valid" time="0.05" steps="13"/></proof>
</goal>
<goal name="VC iconstf.4" expl="4. precondition">
<proof prover="0"><result status="valid" time="0.08" steps="57"/></proof>
<goal name="VC iconstf.4" expl="4. postcondition">
<proof prover="0"><result status="valid" time="0.05" steps="13"/></proof>
</goal>
<goal name="VC iconstf.5" expl="5. postcondition">
<proof prover="0"><result status="valid" time="0.05" steps="14"/></proof>
</goal>
<goal name="VC iconstf.6" expl="6. postcondition">
<proof prover="0"><result status="valid" time="0.04" steps="26"/></proof>
<proof prover="0"><result status="valid" time="0.04" steps="22"/></proof>
</goal>
</transf>
</goal>
<goal name="VC ivarf" expl="VC for ivarf">
<transf name="split_goal_wp">
<goal name="VC ivarf.1" expl="1. precondition">
<proof prover="1"><result status="valid" time="0.85"/></proof>
<proof prover="1"><result status="valid" time="1.24"/></proof>
</goal>
<goal name="VC ivarf.2" expl="2. precondition">
<proof prover="0"><result status="valid" time="0.05" steps="8"/></proof>
<proof prover="0"><result status="valid" time="0.07" steps="30"/></proof>
</goal>
<goal name="VC ivarf.3" expl="3. precondition">
<proof prover="0"><result status="valid" time="0.06" steps="11"/></proof>
<goal name="VC ivarf.3" expl="3. postcondition">
<proof prover="0"><result status="valid" time="0.05" steps="13"/></proof>
</goal>
<goal name="VC ivarf.4" expl="4. precondition">
<proof prover="0"><result status="valid" time="0.07" steps="58"/></proof>
<goal name="VC ivarf.4" expl="4. postcondition">
<proof prover="0"><result status="valid" time="0.05" steps="13"/></proof>
</goal>
<goal name="VC ivarf.5" expl="5. postcondition">
<proof prover="0"><result status="valid" time="0.05" steps="14"/></proof>
</goal>
<goal name="VC ivarf.6" expl="6. postcondition">
<proof prover="0"><result status="valid" time="0.04" steps="26"/></proof>
<proof prover="0"><result status="valid" time="0.04" steps="22"/></proof>
</goal>
</transf>
</goal>
......@@ -84,19 +84,13 @@
</transf>
</goal>
<goal name="VC create_binop.2" expl="2. precondition">
<proof prover="0"><result status="valid" time="0.05" steps="8"/></proof>
</goal>
<goal name="VC create_binop.3" expl="3. precondition">
<proof prover="0"><result status="valid" time="0.05" steps="11"/></proof>
</goal>
<goal name="VC create_binop.4" expl="4. precondition">
<transf name="compute_specified">
<goal name="VC create_binop.4.1" expl="1. precondition">
<goal name="VC create_binop.2.1" expl="1. precondition">
<transf name="introduce_premises">
<goal name="VC create_binop.4.1.1" expl="1. precondition">
<goal name="VC create_binop.2.1.1" expl="1. precondition">
<transf name="compute_specified">
<goal name="VC create_binop.4.1.1.1" expl="1. precondition">
<proof prover="0"><result status="valid" time="0.05" steps="143"/></proof>
<goal name="VC create_binop.2.1.1.1" expl="1. precondition">
<proof prover="0"><result status="valid" time="0.05" steps="140"/></proof>
</goal>
</transf>
</goal>
......@@ -104,11 +98,14 @@
</goal>
</transf>
</goal>
<goal name="VC create_binop.5" expl="5. postcondition">
<proof prover="0"><result status="valid" time="0.06" steps="14"/></proof>
<goal name="VC create_binop.3" expl="3. postcondition">
<proof prover="0"><result status="valid" time="0.06" steps="13"/></proof>
</goal>
<goal name="VC create_binop.4" expl="4. postcondition">
<proof prover="0"><result status="valid" time="0.05" steps="13"/></proof>
</goal>
<goal name="VC create_binop.6" expl="6. postcondition">
<proof prover="0"><result status="valid" time="0.05" steps="14"/></proof>
<goal name="VC create_binop.5" expl="5. postcondition">
<proof prover="0"><result status="valid" time="0.05" steps="13"/></proof>
</goal>
</transf>
</goal>
......@@ -123,24 +120,19 @@
</goal>
<goal name="VC inil" expl="VC for inil">
<transf name="split_goal_wp">
<goal name="VC inil.1" expl="1. postcondition">
<proof prover="0"><result status="valid" time="0.03" steps="6"/></proof>
<goal name="VC inil.1" expl="1. precondition">
<proof prover="1"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="VC inil.2" expl="2. postcondition">
<proof prover="0"><result status="valid" time="0.03" steps="8"/></proof>
</goal>
<goal name="VC inil.3" expl="3. postcondition">
<proof prover="0"><result status="valid" time="0.02" steps="8"/></proof>