Commit 8eb4bb3e authored by MARCHE Claude's avatar MARCHE Claude

example prover: proofs in progress

parent 7c176be8
......@@ -36,28 +36,28 @@ module Impl
use import set.Set as S
use import BacktrackArray.Impl as BA
val ghost sdata_inv_hack (u:unit) : pred sdata
val ghost sdata_inv_hack (u:unit) : sdata -> bool
ensures { result = sdata_inv }
let main (base:nlimpl_fo_formula_list) (gnum:int) : int
let main (base:nlimpl_fo_formula_list) (gnum:int) (ghost st:'st): int
requires { nlimpl_fo_formula_list_ok base }
diverges
ensures { forall m:model int 'st,rho:func int 'st.
ensures { forall m:model int 'st,rho:int -> 'st.
not(formula_list_conj_semantic base.model_fo_formula_list_field m rho) }
raises { Sat -> forall m:model int 'st,rho:func int 'st.
raises { Sat -> forall m:model int 'st,rho:int -> 'st.
formula_list_conj_semantic base.model_fo_formula_list_field m rho }
=
let root = construct_tableau NLC_Root in
try let phip = preprocessing base gnum in
try let phip = preprocessing base gnum st in
let phip0 = (phip:preprocessing_return 'st).preprocessed in
let phip0m = phip0.model_fo_formula_list_field in
assert { root.model_tableau_field = Root } ;
let gnum = phip.final_goals_number in
let gnum = if gnum <= 0 then (-1) else gnum in
let rec aux (n:int) : (int, prover_return)
let rec aux (n:int) (ghost st:'st) : (int, prover_return)
diverges
returns { (_,{ contradictory_assignment = s }) ->
forall m:model int 'st,rho:func int 'st.
forall m:model int 'st,rho:int -> 'st.
let rhos = semantic_subst s m rho in
not(formula_list_conj_semantic phip0.model_fo_formula_list_field m rhos) }
=
......@@ -71,15 +71,15 @@ module Impl
(subst_id_fo_term) &&
(smodel (BA.current_timestamp unifb)) = subst_id_fo_term } ;
assert { forall x:int. unassigned (BA.current_timestamp unifb) x } ;
try (n,extend_branch phip0 root unifb unif 0 n gnum)
with Failure -> aux (n+1)
try (n,extend_branch phip0 root unifb unif 0 n gnum st)
with Failure -> aux (n+1) st
end
in
let n,r = aux 0 in
let n,r = aux 0 st in
let s = r.contradictory_assignment in
let basem = base.model_fo_formula_list_field in
let tr = phip.model_transf in
assert { forall m:model int 'st,rho:func int 'st.
assert { forall m:model int 'st,rho:int -> 'st.
let m' = { interp_fun = (tr m).interp_fun ;
interp_pred = (tr m).interp_pred } in
let rhos = semantic_subst s m' rho in
......
......@@ -2,102 +2,104 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="Z3" version="4.3.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="4" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../ProverMain.mlw">
<theory name="Types">
</theory>
<theory name="Impl">
<goal name="WP_parameter main" expl="VC for main">
<transf name="split_goal_right">
<goal name="WP_parameter main.1" expl="precondition">
<proof prover="2"><result status="valid" time="0.12" steps="13"/></proof>
</goal>
<goal name="WP_parameter main.2" expl="assertion">
<proof prover="2"><result status="valid" time="0.25" steps="18"/></proof>
</goal>
<goal name="WP_parameter main.3" expl="assertion">
<transf name="split_goal_right">
<goal name="WP_parameter main.3.1" expl="VC for main">
<proof prover="1"><result status="valid" time="0.45"/></proof>
<prover id="5" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../ProverMain.mlw" proved="true">
<theory name="Impl" proved="true">
<goal name="VC main" expl="VC for main" proved="true">
<transf name="split_goal_right" proved="true" >
<goal name="VC main.0" expl="precondition" proved="true">
<proof prover="5"><result status="valid" time="0.34"/></proof>
</goal>
<goal name="VC main.1" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.11" steps="13"/></proof>
</goal>
<goal name="VC main.2" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.12" steps="18"/></proof>
</goal>
<goal name="VC main.3" expl="assertion" proved="true">
<transf name="split_goal_right" proved="true" >
<goal name="VC main.3.0" expl="VC for main" proved="true">
<proof prover="1"><result status="valid" time="0.62"/></proof>
</goal>
<goal name="WP_parameter main.3.2" expl="VC for main">
<proof prover="2"><result status="valid" time="0.15" steps="63"/></proof>
<goal name="VC main.3.1" expl="VC for main" proved="true">
<proof prover="0"><result status="valid" time="0.15" steps="53"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter main.4" expl="assertion">
<proof prover="2"><result status="valid" time="0.22" steps="90"/></proof>
<goal name="VC main.4" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.22" steps="123"/></proof>
</goal>
<goal name="WP_parameter main.5" expl="precondition">
<proof prover="2"><result status="valid" time="0.26" steps="24"/></proof>
<goal name="VC main.5" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.13" steps="23"/></proof>
</goal>
<goal name="WP_parameter main.6" expl="precondition">
<proof prover="2"><result status="valid" time="0.25" steps="24"/></proof>
<goal name="VC main.6" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.12" steps="24"/></proof>
</goal>
<goal name="WP_parameter main.7" expl="precondition">
<proof prover="2"><result status="valid" time="0.14" steps="42"/></proof>
<goal name="VC main.7" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.15" steps="41"/></proof>
</goal>
<goal name="WP_parameter main.8" expl="precondition">
<proof prover="2"><result status="valid" time="0.24" steps="24"/></proof>
<goal name="VC main.8" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.24" steps="24"/></proof>
</goal>
<goal name="WP_parameter main.9" expl="precondition">
<proof prover="2"><result status="valid" time="0.15" steps="46"/></proof>
<goal name="VC main.9" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.14" steps="56"/></proof>
</goal>
<goal name="WP_parameter main.10" expl="precondition">
<proof prover="2"><result status="valid" time="0.17" steps="93"/></proof>
<goal name="VC main.10" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.17" steps="132"/></proof>
</goal>
<goal name="WP_parameter main.11" expl="precondition">
<proof prover="2"><result status="valid" time="0.24" steps="41"/></proof>
<goal name="VC main.11" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.24" steps="64"/></proof>
</goal>
<goal name="WP_parameter main.12" expl="precondition">
<proof prover="2"><result status="valid" time="0.12" steps="24"/></proof>
<goal name="VC main.12" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.12" steps="26"/></proof>
</goal>
<goal name="WP_parameter main.13" expl="precondition">
<proof prover="2"><result status="valid" time="0.12" steps="24"/></proof>
<goal name="VC main.13" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.12" steps="26"/></proof>
</goal>
<goal name="WP_parameter main.14" expl="precondition">
<proof prover="2"><result status="valid" time="0.26" steps="24"/></proof>
<goal name="VC main.14" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.26" steps="26"/></proof>
</goal>
<goal name="WP_parameter main.15" expl="precondition">
<proof prover="2"><result status="valid" time="0.27" steps="42"/></proof>
<goal name="VC main.15" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.27" steps="69"/></proof>
</goal>
<goal name="WP_parameter main.16" expl="postcondition">
<proof prover="2"><result status="valid" time="0.14" steps="53"/></proof>
<goal name="VC main.16" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.26" steps="43"/></proof>
</goal>
<goal name="WP_parameter main.17" expl="postcondition">
<proof prover="2"><result status="valid" time="0.26" steps="53"/></proof>
<goal name="VC main.17" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.14" steps="43"/></proof>
</goal>
<goal name="WP_parameter main.18" expl="assertion">
<transf name="split_goal_right">
<goal name="WP_parameter main.18.1" expl="assertion">
<proof prover="2"><result status="valid" time="0.13" steps="18"/></proof>
<goal name="VC main.18" expl="assertion" proved="true">
<transf name="split_goal_right" proved="true" >
<goal name="VC main.18.0" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.13" steps="18"/></proof>
</goal>
<goal name="WP_parameter main.18.2" expl="assertion">
<proof prover="2"><result status="valid" time="0.14" steps="33"/></proof>
<goal name="VC main.18.1" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.17" steps="32"/></proof>
</goal>
<goal name="WP_parameter main.18.3" expl="assertion">
<proof prover="2"><result status="valid" time="0.17" steps="36"/></proof>
<goal name="VC main.18.2" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.17" steps="34"/></proof>
</goal>
<goal name="WP_parameter main.18.4" expl="assertion">
<proof prover="2"><result status="valid" time="0.15" steps="40"/></proof>
<goal name="VC main.18.3" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.14" steps="81"/></proof>
</goal>
<goal name="WP_parameter main.18.5" expl="assertion">
<proof prover="2"><result status="valid" time="0.17" steps="35"/></proof>
<goal name="VC main.18.4" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.15" steps="51"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter main.19" expl="postcondition">
<proof prover="3"><result status="valid" time="0.80"/></proof>
<proof prover="4"><result status="valid" time="1.21"/></proof>
<goal name="VC main.19" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.14" steps="31"/></proof>
</goal>
<goal name="WP_parameter main.20" expl="postcondition">
<proof prover="2"><result status="valid" time="0.14" steps="23"/></proof>
<goal name="VC main.20" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.30"/></proof>
<proof prover="4"><result status="valid" time="0.46"/></proof>
</goal>
<goal name="WP_parameter main.21" expl="exceptional postcondition">
<proof prover="2"><result status="valid" time="0.14" steps="23"/></proof>
<goal name="VC main.21" expl="exceptional postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.14" steps="23"/></proof>
</goal>
</transf>
</goal>
......
......@@ -324,7 +324,7 @@ module Impl
use import FormulaTransformations.Impl as F
let test () : unit
let test (ghost st:'st) : unit
diverges
raises { F.Sat -> true }
=
......@@ -350,7 +350,7 @@ module Impl
let nphi1 = construct_fo_formula (NLC_Not phi1) in
let fl1 = construct_fo_formula_list (NLC_FOFCons nphi1 fonil) in
let fl2 = construct_fo_formula_list (NLC_FOFCons phi0 fl1) in*)
let _ = main (zenon10 2) 1 in
let _ = main (zenon10 2) 1 st in
()
end
......@@ -2,58 +2,51 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../ProverTest.mlw">
<theory name="Types">
</theory>
<theory name="Impl">
<goal name="WP_parameter imply" expl="VC for imply">
<proof prover="0"><result status="valid" time="0.15" steps="48"/></proof>
<prover id="3" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../ProverTest.mlw" proved="true">
<theory name="Impl" proved="true">
<goal name="VC imply" expl="VC for imply" proved="true">
<proof prover="3"><result status="valid" time="0.40" steps="1195"/></proof>
</goal>
<goal name="WP_parameter equiv" expl="VC for equiv">
<proof prover="0"><result status="valid" time="0.17" steps="59"/></proof>
<goal name="VC equiv" expl="VC for equiv" proved="true">
<proof prover="3"><result status="valid" time="0.60" steps="2387"/></proof>
</goal>
<goal name="WP_parameter drinker" expl="VC for drinker">
<proof prover="0"><result status="valid" time="1.01" steps="54"/></proof>
<goal name="VC drinker" expl="VC for drinker" proved="true">
<proof prover="3"><result status="valid" time="1.91" steps="6811"/></proof>
</goal>
<goal name="WP_parameter group" expl="VC for group">
<proof prover="1"><result status="valid" time="0.36"/></proof>
<goal name="VC group" expl="VC for group" proved="true">
<proof prover="1"><result status="valid" time="0.63"/></proof>
</goal>
<goal name="WP_parameter bidon1" expl="VC for bidon1">
<proof prover="0"><result status="valid" time="0.22" steps="38"/></proof>
<goal name="VC bidon1" expl="VC for bidon1" proved="true">
<proof prover="3"><result status="valid" time="0.56" steps="1609"/></proof>
</goal>
<goal name="WP_parameter bidon2" expl="VC for bidon2">
<proof prover="0"><result status="valid" time="0.30" steps="52"/></proof>
<goal name="VC bidon2" expl="VC for bidon2" proved="true">
<proof prover="3"><result status="valid" time="2.35" steps="6730"/></proof>
</goal>
<goal name="WP_parameter bidon3" expl="VC for bidon3">
<proof prover="1"><result status="valid" time="0.30"/></proof>
<proof prover="2"><result status="valid" time="0.18"/></proof>
<goal name="VC bidon3" expl="VC for bidon3" proved="true">
<proof prover="1"><result status="valid" time="0.66"/></proof>
</goal>
<goal name="WP_parameter bidon4" expl="VC for bidon4">
<proof prover="1"><result status="valid" time="0.30"/></proof>
<proof prover="2"><result status="valid" time="0.10"/></proof>
<goal name="VC bidon4" expl="VC for bidon4" proved="true">
<proof prover="1"><result status="valid" time="0.48"/></proof>
</goal>
<goal name="WP_parameter pierce" expl="VC for pierce">
<proof prover="0"><result status="valid" time="0.30" steps="50"/></proof>
<goal name="VC pierce" expl="VC for pierce" proved="true">
<proof prover="3"><result status="valid" time="1.09" steps="3645"/></proof>
</goal>
<goal name="WP_parameter generate" expl="VC for generate">
<proof prover="0"><result status="valid" time="0.25" steps="51"/></proof>
<goal name="VC generate" expl="VC for generate" proved="true">
<proof prover="3"><result status="valid" time="0.45" steps="911"/></proof>
</goal>
<goal name="WP_parameter zenon5" expl="VC for zenon5">
<goal name="VC zenon5" expl="VC for zenon5" proved="true">
<proof prover="1"><result status="valid" time="0.31"/></proof>
<proof prover="2"><result status="valid" time="0.16"/></proof>
</goal>
<goal name="WP_parameter zenon6" expl="VC for zenon6">
<proof prover="1"><result status="valid" time="0.32"/></proof>
<proof prover="2"><result status="valid" time="0.17"/></proof>
<goal name="VC zenon6" expl="VC for zenon6" proved="true">
<proof prover="1"><result status="valid" time="0.46"/></proof>
</goal>
<goal name="WP_parameter zenon10" expl="VC for zenon10">
<proof prover="1"><result status="valid" time="0.30"/></proof>
<goal name="VC zenon10" expl="VC for zenon10" proved="true">
<proof prover="1"><result status="valid" time="0.44"/></proof>
</goal>
<goal name="WP_parameter test" expl="VC for test">
<proof prover="0"><result status="valid" time="0.13" steps="10"/></proof>
<goal name="VC test" expl="VC for test" proved="true">
<proof prover="3"><result status="valid" time="0.13" steps="10"/></proof>
</goal>
</theory>
</file>
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment