Commit 314ec01e authored by Martin Clochard's avatar Martin Clochard
Browse files

(wip) formalization of Why3 API.

parent 5459a06b
This diff is collapsed.
......@@ -2,10 +2,103 @@
<!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" memlimit="1000"/>
<prover id="1" name="CVC3" version="2.4.1" timelimit="5" memlimit="1000"/>
<file name="../term.mlw" expanded="true">
<theory name="Vs" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
<theory name="Vs" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="Ls" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
<theory name="Ls" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="Term" sum="ddbc28b7f2fe9a580e03e892dc4bc3fb">
<goal name="WP_parameter fused_alt" expl="VC for fused_alt">
<transf name="split_goal_wp">
<goal name="WP_parameter fused_alt.1" expl="1. assertion">
<proof prover="0"><result status="valid" time="0.06" steps="13"/></proof>
</goal>
<goal name="WP_parameter fused_alt.2" expl="2. assertion">
<transf name="split_goal_wp">
<goal name="WP_parameter fused_alt.2.1" expl="1. assertion">
<proof prover="0"><result status="valid" time="0.08" steps="36"/></proof>
</goal>
<goal name="WP_parameter fused_alt.2.2" expl="2. assertion">
<proof prover="0"><result status="valid" time="0.09" steps="58"/></proof>
</goal>
<goal name="WP_parameter fused_alt.2.3" expl="3. assertion">
<proof prover="0"><result status="valid" time="0.23" steps="34"/></proof>
</goal>
<goal name="WP_parameter fused_alt.2.4" expl="4. assertion">
<proof prover="0"><result status="valid" time="0.08" steps="45"/></proof>
</goal>
<goal name="WP_parameter fused_alt.2.5" expl="5. assertion">
<proof prover="0"><result status="valid" time="0.08" steps="103"/></proof>
</goal>
<goal name="WP_parameter fused_alt.2.6" expl="6. assertion">
<proof prover="0"><result status="valid" time="0.09" steps="34"/></proof>
</goal>
<goal name="WP_parameter fused_alt.2.7" expl="7. assertion">
<proof prover="0"><result status="valid" time="0.07" steps="45"/></proof>
</goal>
<goal name="WP_parameter fused_alt.2.8" expl="8. assertion">
<proof prover="0"><result status="valid" time="0.20" steps="103"/></proof>
</goal>
<goal name="WP_parameter fused_alt.2.9" expl="9. assertion">
<proof prover="0"><result status="valid" time="0.19" steps="24"/></proof>
</goal>
<goal name="WP_parameter fused_alt.2.10" expl="10. assertion">
<proof prover="0"><result status="valid" time="0.22" steps="33"/></proof>
</goal>
<goal name="WP_parameter fused_alt.2.11" expl="11. assertion">
<proof prover="0"><result status="valid" time="0.09" steps="61"/></proof>
</goal>
<goal name="WP_parameter fused_alt.2.12" expl="12. assertion">
<proof prover="0"><result status="valid" time="0.08" steps="32"/></proof>
</goal>
<goal name="WP_parameter fused_alt.2.13" expl="13. assertion">
<proof prover="0"><result status="valid" time="0.24" steps="97"/></proof>
</goal>
<goal name="WP_parameter fused_alt.2.14" expl="14. assertion">
<proof prover="0"><result status="valid" time="0.08" steps="33"/></proof>
</goal>
<goal name="WP_parameter fused_alt.2.15" expl="15. assertion">
<proof prover="0"><result status="valid" time="0.19" steps="61"/></proof>
</goal>
<goal name="WP_parameter fused_alt.2.16" expl="16. assertion">
<proof prover="0"><result status="valid" time="0.18" steps="32"/></proof>
</goal>
<goal name="WP_parameter fused_alt.2.17" expl="17. assertion">
<proof prover="0"><result status="valid" time="0.08" steps="97"/></proof>
</goal>
<goal name="WP_parameter fused_alt.2.18" expl="18. assertion">
<proof prover="0"><result status="valid" time="0.08" steps="47"/></proof>
</goal>
<goal name="WP_parameter fused_alt.2.19" expl="19. assertion">
<proof prover="0"><result status="valid" time="0.06" steps="38"/></proof>
</goal>
<goal name="WP_parameter fused_alt.2.20" expl="20. assertion">
<proof prover="0"><result status="valid" time="0.07" steps="43"/></proof>
</goal>
<goal name="WP_parameter fused_alt.2.21" expl="21. assertion">
<proof prover="0"><result status="valid" time="0.08" steps="47"/></proof>
</goal>
<goal name="WP_parameter fused_alt.2.22" expl="22. assertion">
<proof prover="0"><result status="valid" time="0.07" steps="38"/></proof>
</goal>
<goal name="WP_parameter fused_alt.2.23" expl="23. assertion">
<proof prover="0"><result status="valid" time="0.06" steps="43"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter fused_alt.3" expl="3. postcondition">
<proof prover="1"><result status="valid" time="0.55"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter fused_inj" expl="VC for fused_inj">
<proof prover="0"><result status="valid" time="0.31" steps="141"/></proof>
</goal>
<goal name="WP_parameter trigger_irrelevant" expl="VC for trigger_irrelevant">
<proof prover="0"><result status="valid" time="0.18" steps="82"/></proof>
</goal>
</theory>
</file>
</why3session>
......@@ -267,8 +267,7 @@ module Ty
val ty_inst (ghost cty0 cty1:ty_ctx) (m:Mtv.t ty) (ty:ty) : ty
requires { cty0.cty_d ty }
requires { forall x. cty0.cty_tv.c_pdom x /\ m.Mtv.domain x ->
cty1.cty_d (m.Mtv.bindings x) }
requires { forall x. m.Mtv.domain x -> cty1.cty_d (m.Mtv.bindings x) }
ensures { cty1.cty_d result /\
cty1.cty_m result = ty_subst (make_ty_subst cty1 m) id (cty0.cty_m ty) }
......@@ -280,8 +279,7 @@ module Ty
raises otherwise. *)
val ty_match (ghost cty0 cty1:ty_ctx) (s:Mtv.t ty) (pat ty:ty) : Mtv.t ty
requires { cty0.cty_d pat /\ cty1.cty_d ty }
requires { forall x. cty0.cty_tv.c_pdom x /\ s.Mtv.domain x ->
cty1.cty_d (s.Mtv.bindings x) }
requires { forall x. s.Mtv.domain x -> cty1.cty_d (s.Mtv.bindings x) }
(* Correct instantiation. *)
ensures {
ty_subst (make_ty_subst cty1 result) id (cty0.cty_m pat) = cty1.cty_m ty }
......@@ -295,11 +293,12 @@ module Ty
ty_tyv_free_var (cty0.cty_m pat) (cty0.cty_tv.c_ptl x))) }
(* Increase. *)
ensures { equalizer s.Mtv.domain s.Mtv.bindings result.Mtv.bindings }
ensures { forall x. cty0.cty_tv.c_pdom x /\ result.Mtv.domain x ->
cty1.cty_d (result.Mtv.bindings x) }
(* Invariant. *)
ensures { forall x. result.Mtv.domain x ->
ty1.cty_d (result.Mtv.bindings x) }
(* Failure. *)
raises { TypeMismatch _ -> forall f.
(forall x. cty0.cty_tv.c_pdom x /\ s.Mtv.domain x ->
(forall x. s.Mtv.domain x ->
f (cty0.cty_tv.c_ptl x) = cty1.cty_m (s.Mtv.bindings x)) ->
ty_subst f id (cty0.cty_m pat) <> cty1.cty_m ty }
......@@ -307,7 +306,7 @@ module Ty
let ty_match_sure (ghost cty0 cty1:ty_ctx) (ghost f:int -> D.ty)
(s:Mtv.t ty) (pat ty:ty) : Mtv.t ty
requires { cty0.cty_d pat /\ cty1.cty_d ty }
requires { forall x. cty0.cty_tv.c_pdom x /\ s.Mtv.domain x ->
requires { forall x. s.Mtv.domain x ->
cty1.cty_d (s.Mtv.bindings x) /\
f (cty0.cty_tv.c_ptl x) = cty1.cty_m (s.Mtv.bindings x) }
requires { ty_subst f id (cty0.cty_m pat) = cty1.cty_m ty }
......@@ -320,13 +319,13 @@ module Ty
(s.Mtv.domain x \/ (cty0.cty_tv.c_pdom x /\
ty_tyv_free_var (cty0.cty_m pat) (cty0.cty_tv.c_ptl x))) }
ensures { equalizer s.Mtv.domain s.Mtv.bindings result.Mtv.bindings }
ensures { forall x. cty0.cty_tv.c_pdom x /\ result.Mtv.domain x ->
ensures { forall x. result.Mtv.domain x ->
cty1.cty_d (result.Mtv.bindings x) }
= try ty_match cty0 cty1 s pat ty
with TypeMismatch _ -> absurd
end
val ty_free_vars (ghost cty:ty_ctx) (s:Mtv.s) (ty:ty) : Mtv.s
val ty_freevars (ghost cty:ty_ctx) (s:Mtv.s) (ty:ty) : Mtv.s
requires { cty.cty_d ty }
ensures { let ctv = cty.cty_tv in
forall x. result.Mtv.domain x <->
......
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