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

Repair sessions

parent 784887ff
......@@ -7,11 +7,37 @@
<prover id="2" name="Z3" version="4.3.1" timelimit="5" memlimit="1000"/>
<prover id="3" name="Alt-Ergo" version="0.95.2" timelimit="5" memlimit="1000"/>
<file name="../priority_queue.mlw" expanded="true">
<theory name="PQueue" sum="43d94f2f459569d40d93b24723828ae5" expanded="true">
<theory name="PQueue" sum="bf9be8441d5314e5761b34e3d7d132e0" expanded="true">
<goal name="S.O.Trans">
<proof prover="3" timelimit="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="M.WP_parameter assoc_m" expl="VC for assoc_m" expanded="true">
<goal name="M.WP_parameter assoc_m" expl="VC for assoc_m">
<transf name="split_goal_wp">
<goal name="WP_parameter assoc_m.1" expl="1. postcondition">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter assoc_m.2" expl="2. postcondition">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter assoc_m.3" expl="3. postcondition">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter assoc_m.4" expl="4. postcondition">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter assoc_m.5" expl="5. postcondition">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter assoc_m.6" expl="6. postcondition">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter assoc_m.7" expl="7. postcondition">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter assoc_m.8" expl="8. postcondition">
<proof prover="1"><result status="valid" time="0.03"/></proof>
</goal>
</transf>
</goal>
<goal name="M.WP_parameter neutral_m" expl="VC for neutral_m">
<proof prover="1" timelimit="3"><result status="valid" time="0.05"/></proof>
......@@ -655,13 +681,13 @@
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter selected_is_min.1.2" expl="2. postcondition">
<proof prover="3"><result status="valid" time="1.42"/></proof>
<proof prover="3"><result status="valid" time="1.67"/></proof>
</goal>
<goal name="WP_parameter selected_is_min.1.3" expl="3. postcondition">
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="WP_parameter selected_is_min.1.4" expl="4. postcondition">
<proof prover="1"><result status="valid" time="0.45"/></proof>
<proof prover="1"><result status="valid" time="0.63"/></proof>
</goal>
</transf>
</goal>
......@@ -670,24 +696,30 @@
<goal name="WP_parameter selected_part" expl="VC for selected_part">
<transf name="split_goal_wp">
<goal name="WP_parameter selected_part.1" expl="1. postcondition">
<proof prover="3"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="WP_parameter selected_part.2" expl="2. postcondition">
<transf name="split_goal_wp">
<goal name="WP_parameter selected_part.1.1" expl="1. postcondition">
<proof prover="3"><result status="valid" time="0.04"/></proof>
<goal name="WP_parameter selected_part.2.1" expl="1. postcondition">
<proof prover="3"><result status="valid" time="0.36"/></proof>
</goal>
<goal name="WP_parameter selected_part.2.2" expl="2. postcondition">
<proof prover="3"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="WP_parameter selected_part.1.2" expl="2. postcondition">
<goal name="WP_parameter selected_part.2.3" expl="3. postcondition">
<transf name="introduce_premises">
<goal name="WP_parameter selected_part.1.2.1" expl="1.">
<goal name="WP_parameter selected_part.2.3.1" expl="1.">
<transf name="inline_goal">
<goal name="WP_parameter selected_part.1.2.1.1" expl="1.">
<goal name="WP_parameter selected_part.2.3.1.1" expl="1.">
<transf name="split_goal_wp">
<goal name="WP_parameter selected_part.1.2.1.1.1" expl="1.">
<proof prover="3"><result status="valid" time="0.05"/></proof>
<goal name="WP_parameter selected_part.2.3.1.1.1" expl="1.">
<proof prover="3"><result status="valid" time="0.07"/></proof>
</goal>
<goal name="WP_parameter selected_part.1.2.1.1.2" expl="2.">
<proof prover="1" timelimit="30"><result status="valid" time="0.90"/></proof>
<goal name="WP_parameter selected_part.2.3.1.1.2" expl="2.">
<proof prover="1"><result status="valid" time="0.17"/></proof>
</goal>
<goal name="WP_parameter selected_part.1.2.1.1.3" expl="3.">
<proof prover="3"><result status="valid" time="0.05"/></proof>
<goal name="WP_parameter selected_part.2.3.1.1.3" expl="3.">
<proof prover="3"><result status="valid" time="0.06"/></proof>
</goal>
</transf>
</goal>
......@@ -695,30 +727,30 @@
</goal>
</transf>
</goal>
<goal name="WP_parameter selected_part.1.3" expl="3. postcondition">
<proof prover="3"><result status="valid" time="1.06"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter selected_part.2" expl="2. postcondition">
<goal name="WP_parameter selected_part.3" expl="3. postcondition">
<transf name="split_goal_wp">
<goal name="WP_parameter selected_part.2.1" expl="1. postcondition">
<proof prover="3"><result status="valid" time="0.03"/></proof>
<goal name="WP_parameter selected_part.3.1" expl="1. postcondition">
<proof prover="3"><result status="valid" time="0.07"/></proof>
</goal>
<goal name="WP_parameter selected_part.2.2" expl="2. postcondition">
<goal name="WP_parameter selected_part.3.2" expl="2. postcondition">
<proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="WP_parameter selected_part.3.3" expl="3. postcondition">
<transf name="introduce_premises">
<goal name="WP_parameter selected_part.2.2.1" expl="1.">
<goal name="WP_parameter selected_part.3.3.1" expl="1.">
<transf name="inline_goal">
<goal name="WP_parameter selected_part.2.2.1.1" expl="1.">
<goal name="WP_parameter selected_part.3.3.1.1" expl="1.">
<transf name="split_goal_wp">
<goal name="WP_parameter selected_part.2.2.1.1.1" expl="1.">
<proof prover="3"><result status="valid" time="0.05"/></proof>
<goal name="WP_parameter selected_part.3.3.1.1.1" expl="1.">
<proof prover="3"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="WP_parameter selected_part.2.2.1.1.2" expl="2.">
<proof prover="1" timelimit="20"><result status="valid" time="0.89"/></proof>
<goal name="WP_parameter selected_part.3.3.1.1.2" expl="2.">
<proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="WP_parameter selected_part.2.2.1.1.3" expl="3.">
<proof prover="3"><result status="valid" time="0.07"/></proof>
<goal name="WP_parameter selected_part.3.3.1.1.3" expl="3.">
<proof prover="1"><result status="valid" time="1.57"/></proof>
</goal>
</transf>
</goal>
......@@ -726,23 +758,27 @@
</goal>
</transf>
</goal>
<goal name="WP_parameter selected_part.2.3" expl="3. postcondition">
<proof prover="3"><result status="valid" time="0.05"/></proof>
</transf>
</goal>
<goal name="WP_parameter selected_part.4" expl="4. postcondition">
<transf name="split_goal_wp">
<goal name="WP_parameter selected_part.4.1" expl="1. postcondition">
<proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="WP_parameter selected_part.2.4" expl="4. postcondition">
<goal name="WP_parameter selected_part.4.2" expl="2. postcondition">
<transf name="introduce_premises">
<goal name="WP_parameter selected_part.2.4.1" expl="1.">
<goal name="WP_parameter selected_part.4.2.1" expl="1.">
<transf name="inline_goal">
<goal name="WP_parameter selected_part.2.4.1.1" expl="1.">
<goal name="WP_parameter selected_part.4.2.1.1" expl="1.">
<transf name="split_goal_wp">
<goal name="WP_parameter selected_part.2.4.1.1.1" expl="1.">
<proof prover="3"><result status="valid" time="0.06"/></proof>
<goal name="WP_parameter selected_part.4.2.1.1.1" expl="1.">
<proof prover="3"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="WP_parameter selected_part.2.4.1.1.2" expl="2.">
<proof prover="3"><result status="valid" time="0.07"/></proof>
<goal name="WP_parameter selected_part.4.2.1.1.2" expl="2.">
<proof prover="1" timelimit="30"><result status="valid" time="1.19"/></proof>
</goal>
<goal name="WP_parameter selected_part.2.4.1.1.3" expl="3.">
<proof prover="1" timelimit="20"><result status="valid" time="2.16"/></proof>
<goal name="WP_parameter selected_part.4.2.1.1.3" expl="3.">
<proof prover="3"><result status="valid" time="0.05"/></proof>
</goal>
</transf>
</goal>
......@@ -750,30 +786,30 @@
</goal>
</transf>
</goal>
<goal name="WP_parameter selected_part.4.3" expl="3. postcondition">
<proof prover="3"><result status="valid" time="1.34"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter selected_part.3" expl="3. postcondition">
<goal name="WP_parameter selected_part.5" expl="5. postcondition">
<transf name="split_goal_wp">
<goal name="WP_parameter selected_part.3.1" expl="1. postcondition">
<proof prover="3"><result status="valid" time="0.07"/></proof>
</goal>
<goal name="WP_parameter selected_part.3.2" expl="2. postcondition">
<proof prover="3"><result status="valid" time="0.04"/></proof>
<goal name="WP_parameter selected_part.5.1" expl="1. postcondition">
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="WP_parameter selected_part.3.3" expl="3. postcondition">
<goal name="WP_parameter selected_part.5.2" expl="2. postcondition">
<transf name="introduce_premises">
<goal name="WP_parameter selected_part.3.3.1" expl="1.">
<goal name="WP_parameter selected_part.5.2.1" expl="1.">
<transf name="inline_goal">
<goal name="WP_parameter selected_part.3.3.1.1" expl="1.">
<goal name="WP_parameter selected_part.5.2.1.1" expl="1.">
<transf name="split_goal_wp">
<goal name="WP_parameter selected_part.3.3.1.1.1" expl="1.">
<proof prover="3"><result status="valid" time="0.06"/></proof>
<goal name="WP_parameter selected_part.5.2.1.1.1" expl="1.">
<proof prover="3"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="WP_parameter selected_part.3.3.1.1.2" expl="2.">
<proof prover="3"><result status="valid" time="0.04"/></proof>
<goal name="WP_parameter selected_part.5.2.1.1.2" expl="2.">
<proof prover="1" timelimit="20"><result status="valid" time="1.22"/></proof>
</goal>
<goal name="WP_parameter selected_part.3.3.1.1.3" expl="3.">
<proof prover="1"><result status="valid" time="1.01"/></proof>
<goal name="WP_parameter selected_part.5.2.1.1.3" expl="3.">
<proof prover="3"><result status="valid" time="0.07"/></proof>
</goal>
</transf>
</goal>
......@@ -781,30 +817,23 @@
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="WP_parameter selected_part.4" expl="4. postcondition">
<transf name="split_goal_wp">
<goal name="WP_parameter selected_part.4.1" expl="1. postcondition">
<proof prover="3"><result status="valid" time="0.17"/></proof>
</goal>
<goal name="WP_parameter selected_part.4.2" expl="2. postcondition">
<goal name="WP_parameter selected_part.5.3" expl="3. postcondition">
<proof prover="3"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="WP_parameter selected_part.4.3" expl="3. postcondition">
<goal name="WP_parameter selected_part.5.4" expl="4. postcondition">
<transf name="introduce_premises">
<goal name="WP_parameter selected_part.4.3.1" expl="1.">
<goal name="WP_parameter selected_part.5.4.1" expl="1.">
<transf name="inline_goal">
<goal name="WP_parameter selected_part.4.3.1.1" expl="1.">
<goal name="WP_parameter selected_part.5.4.1.1" expl="1.">
<transf name="split_goal_wp">
<goal name="WP_parameter selected_part.4.3.1.1.1" expl="1.">
<proof prover="3"><result status="valid" time="0.07"/></proof>
<goal name="WP_parameter selected_part.5.4.1.1.1" expl="1.">
<proof prover="3"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="WP_parameter selected_part.4.3.1.1.2" expl="2.">
<proof prover="1"><result status="valid" time="0.17"/></proof>
<goal name="WP_parameter selected_part.5.4.1.1.2" expl="2.">
<proof prover="3"><result status="valid" time="0.07"/></proof>
</goal>
<goal name="WP_parameter selected_part.4.3.1.1.3" expl="3.">
<proof prover="3"><result status="valid" time="0.06"/></proof>
<goal name="WP_parameter selected_part.5.4.1.1.3" expl="3.">
<proof prover="1" timelimit="20"><result status="valid" time="2.67"/></proof>
</goal>
</transf>
</goal>
......@@ -814,9 +843,6 @@
</goal>
</transf>
</goal>
<goal name="WP_parameter selected_part.5" expl="5. postcondition">
<proof prover="3"><result status="valid" time="0.05"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter first_minimum_caracterisation" expl="VC for first_minimum_caracterisation">
......@@ -859,7 +885,7 @@
</transf>
</goal>
<goal name="WP_parameter first_minimum_caracterisation.5" expl="5. postcondition">
<proof prover="1"><result status="valid" time="2.39"/></proof>
<proof prover="1"><result status="valid" time="3.53"/></proof>
</goal>
<goal name="WP_parameter first_minimum_caracterisation.6" expl="6. variant decrease">
<proof prover="3"><result status="valid" time="0.04"/></proof>
......@@ -913,7 +939,7 @@
<goal name="WP_parameter first_minimum_caracterisation.14" expl="14. postcondition">
<transf name="split_goal_wp">
<goal name="WP_parameter first_minimum_caracterisation.14.1" expl="1.">
<proof prover="2"><result status="valid" time="0.29"/></proof>
<proof prover="2"><result status="valid" time="0.56"/></proof>
</goal>
<goal name="WP_parameter first_minimum_caracterisation.14.2" expl="2.">
<proof prover="3"><result status="valid" time="0.02"/></proof>
......
......@@ -5,7 +5,7 @@
<prover id="0" name="CVC3" version="2.4.1" timelimit="1" memlimit="1000"/>
<prover id="1" name="CVC4" version="1.4" timelimit="1" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="0.95.2" timelimit="1" memlimit="1000"/>
<file name="../tables.mlw" expanded="true">
<file name="../tables.mlw">
<theory name="MapBase" sum="7cd93351ec4f61724437c746a929f65e">
<goal name="D.WP_parameter measure" expl="VC for measure">
<proof prover="2" timelimit="3"><result status="valid" time="0.02"/></proof>
......@@ -79,7 +79,7 @@
<goal name="WP_parameter selected_sem.10.1.1" expl="1. postcondition">
<transf name="split_goal_wp">
<goal name="WP_parameter selected_sem.10.1.1.1" expl="1. postcondition">
<proof prover="1"><result status="timeout" time="0.98"/></proof>
<proof prover="0" timelimit="5"><result status="valid" time="0.14"/></proof>
</goal>
<goal name="WP_parameter selected_sem.10.1.1.2" expl="2. postcondition">
<proof prover="0"><result status="valid" time="0.56"/></proof>
......@@ -146,7 +146,7 @@
<proof prover="2"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="WP_parameter selected_part.2.1.1.2" expl="2. postcondition">
<proof prover="2"><result status="timeout" time="1.99"/></proof>
<proof prover="0" timelimit="5"><result status="valid" time="0.95"/></proof>
</goal>
<goal name="WP_parameter selected_part.2.1.1.3" expl="3. postcondition">
<proof prover="2"><result status="valid" time="0.03"/></proof>
......@@ -164,7 +164,7 @@
<proof prover="2" timelimit="5"><result status="valid" time="1.66"/></proof>
</goal>
<goal name="WP_parameter selected_part.2.1.1.8" expl="8. postcondition">
<proof prover="2"><result status="timeout" time="1.99"/></proof>
<proof prover="0" timelimit="5"><result status="valid" time="0.34"/></proof>
</goal>
<goal name="WP_parameter selected_part.2.1.1.9" expl="9. postcondition">
<proof prover="0"><result status="valid" time="0.29"/></proof>
......
......@@ -2,30 +2,36 @@
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require bool.Bool.
Require int.Int.
Require map.Map.
Require list.List.
Require list.Length.
Require list.Mem.
Require list.Append.
(* Why3 assumption *)
Inductive datatype :=
| TYunit : datatype
| TYint : datatype
| TYbool : datatype .
Inductive datatype :=
| TYunit : datatype
| TYint : datatype
| TYbool : datatype.
Axiom datatype_WhyType : WhyType datatype.
Existing Instance datatype_WhyType.
(* Why3 assumption *)
Inductive value :=
| Vvoid : value
| Vint : Z -> value
| Vbool : bool -> value .
Inductive value :=
| Vvoid : value
| Vint : Z -> value
| Vbool : bool -> value.
Axiom value_WhyType : WhyType value.
Existing Instance value_WhyType.
(* Why3 assumption *)
Inductive operator :=
| Oplus : operator
| Ominus : operator
| Omult : operator
| Ole : operator .
Inductive operator :=
| Oplus : operator
| Ominus : operator
| Omult : operator
| Ole : operator.
Axiom operator_WhyType : WhyType operator.
Existing Instance operator_WhyType.
......@@ -43,93 +49,59 @@ Existing Instance ident_WhyType.
Axiom ident_decide : forall (m1:ident) (m2:ident), (m1 = m2) \/ ~ (m1 = m2).
(* Why3 assumption *)
Inductive term :=
| Tvalue : value -> term
| Tvar : ident -> term
| Tderef : mident -> term
| Tbin : term -> operator -> term -> term .
Inductive term :=
| Tvalue : value -> term
| Tvar : ident -> term
| Tderef : mident -> term
| Tbin : term -> operator -> term -> term.
Axiom term_WhyType : WhyType term.
Existing Instance term_WhyType.
(* Why3 assumption *)
Inductive fmla :=
| Fterm : term -> fmla
| Fand : fmla -> fmla -> fmla
| Fnot : fmla -> fmla
| Fimplies : fmla -> fmla -> fmla
| Flet : ident -> term -> fmla -> fmla
| Fforall : ident -> datatype -> fmla -> fmla .
Inductive fmla :=
| Fterm : term -> fmla
| Fand : fmla -> fmla -> fmla
| Fnot : fmla -> fmla
| Fimplies : fmla -> fmla -> fmla
| Flet : ident -> term -> fmla -> fmla
| Fforall : ident -> datatype -> fmla -> fmla.
Axiom fmla_WhyType : WhyType fmla.
Existing Instance fmla_WhyType.
(* Why3 assumption *)
Inductive stmt :=
| Sskip : stmt
| Sassign : mident -> term -> stmt
| Sseq : stmt -> stmt -> stmt
| Sif : term -> stmt -> stmt -> stmt
| Sassert : fmla -> stmt
| Swhile : term -> fmla -> stmt -> stmt .
Inductive stmt :=
| Sskip : stmt
| Sassign : mident -> term -> stmt
| Sseq : stmt -> stmt -> stmt
| Sif : term -> stmt -> stmt -> stmt
| Sassert : fmla -> stmt
| Swhile : term -> fmla -> stmt -> stmt.
Axiom stmt_WhyType : WhyType stmt.
Existing Instance stmt_WhyType.
Axiom decide_is_skip : forall (s:stmt), (s = Sskip) \/ ~ (s = Sskip).
Axiom map : forall (a:Type) {a_WT:WhyType a} (b:Type) {b_WT:WhyType b}, Type.
Parameter map_WhyType : forall (a:Type) {a_WT:WhyType a}
(b:Type) {b_WT:WhyType b}, WhyType (map a b).
Existing Instance map_WhyType.
Parameter get: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
(map a b) -> a -> b.
Parameter set: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
(map a b) -> a -> b -> (map a b).
Axiom Select_eq : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
forall (m:(map a b)), forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) ->
((get (set m a1 b1) a2) = b1).
Axiom Select_neq : forall {a:Type} {a_WT:WhyType a}
{b:Type} {b_WT:WhyType b}, forall (m:(map a b)), forall (a1:a) (a2:a),
forall (b1:b), (~ (a1 = a2)) -> ((get (set m a1 b1) a2) = (get m a2)).
Parameter const: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
b -> (map a b).
Axiom Const : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
forall (b1:b) (a1:a), ((get (const b1:(map a b)) a1) = b1).
(* Why3 assumption *)
Inductive list (a:Type) {a_WT:WhyType a} :=
| Nil : list a
| Cons : a -> (list a) -> list a.
Axiom list_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (list a).
Existing Instance list_WhyType.
Implicit Arguments Nil [[a] [a_WT]].
Implicit Arguments Cons [[a] [a_WT]].
Definition env := (map.Map.map mident value).
(* Why3 assumption *)
Definition env := (map mident value).
(* Why3 assumption *)
Definition stack := (list (ident* value)%type).
Definition stack := (list (ident* value)%type).
Parameter get_stack: ident -> (list (ident* value)%type) -> value.
Axiom get_stack_def : forall (i:ident) (pi:(list (ident* value)%type)),
match pi with
| Nil => ((get_stack i pi) = Vvoid)
| (Cons (x, v) r) => ((x = i) -> ((get_stack i pi) = v)) /\ ((~ (x = i)) ->
((get_stack i pi) = (get_stack i r)))
| Init.Datatypes.nil => ((get_stack i pi) = Vvoid)
| (Init.Datatypes.cons (x, v) r) => ((x = i) -> ((get_stack i pi) = v)) /\
((~ (x = i)) -> ((get_stack i pi) = (get_stack i r)))
end.
Axiom get_stack_eq : forall (x:ident) (v:value) (r:(list (ident*
value)%type)), ((get_stack x (Cons (x, v) r)) = v).
value)%type)), ((get_stack x (Init.Datatypes.cons (x, v) r)) = v).
Axiom get_stack_neq : forall (x:ident) (i:ident) (v:value) (r:(list (ident*
value)%type)), (~ (x = i)) -> ((get_stack i (Cons (x, v) r)) = (get_stack i
r)).
value)%type)), (~ (x = i)) -> ((get_stack i (Init.Datatypes.cons (x,
v) r)) = (get_stack i r)).
Parameter eval_bin: value -> operator -> value -> value.
......@@ -147,140 +119,108 @@ Axiom eval_bin_def : forall (x:value) (op:operator) (y:value), match (x,
end.
(* Why3 assumption *)
Fixpoint eval_term(sigma:(map mident value)) (pi:(list (ident* value)%type))
(t:term) {struct t}: value :=
Fixpoint eval_term (sigma:(map.Map.map mident value)) (pi:(list (ident*
value)%type)) (t:term) {struct t}: value :=
match t with
| (Tvalue v) => v
| (Tvar id) => (get_stack id pi)
| (Tderef id) => (get sigma id)
| (Tderef id) => (map.Map.get sigma id)
| (Tbin t1 op t2) => (eval_bin (eval_term sigma pi t1) op (eval_term sigma
pi t2))
end.
(* Why3 assumption *)
Fixpoint eval_fmla(sigma:(map mident value)) (pi:(list (ident* value)%type))
(f:fmla) {struct f}: Prop :=
Fixpoint eval_fmla (sigma:(map.Map.map mident value)) (pi:(list (ident*
value)%type)) (f:fmla) {struct f}: Prop :=
match f with
| (Fterm t) => ((eval_term sigma pi t) = (Vbool true))
| (Fand f1 f2) => (eval_fmla sigma pi f1) /\ (eval_fmla sigma pi f2)
| (Fnot f1) => ~ (eval_fmla sigma pi f1)
| (Fimplies f1 f2) => (eval_fmla sigma pi f1) -> (eval_fmla sigma pi f2)
| (Flet x t f1) => (eval_fmla sigma (Cons (x, (eval_term sigma pi t)) pi)
f1)
| (Fforall x TYint f1) => forall (n:Z), (eval_fmla sigma (Cons (x,
(Vint n)) pi) f1)
| (Fforall x TYbool f1) => forall (b:bool), (eval_fmla sigma (Cons (x,
(Vbool b)) pi) f1)
| (Fforall x TYunit f1) => (eval_fmla sigma (Cons (x, Vvoid) pi) f1)
| (Flet x t f1) => (eval_fmla sigma (Init.Datatypes.cons (x,
(eval_term sigma pi t)) pi) f1)
| (Fforall x TYint f1) => forall (n:Z), (eval_fmla sigma
(Init.Datatypes.cons (x, (Vint n)) pi) f1)
| (Fforall x TYbool f1) => forall (b:bool), (eval_fmla sigma
(Init.Datatypes.cons (x, (Vbool b)) pi) f1)
| (Fforall x TYunit f1) => (eval_fmla sigma (Init.Datatypes.cons (x,
Vvoid) pi) f1)
end.
(* Why3 assumption *)
Definition valid_fmla(p:fmla): Prop := forall (sigma:(map mident value))
(pi:(list (ident* value)%type)), (eval_fmla sigma pi p).
Definition valid_fmla (p:fmla): Prop := forall (sigma:(map.Map.map mident
value)) (pi:(list (ident* value)%type)), (eval_fmla sigma pi p).
(* Why3 assumption *)
Inductive one_step : (map mident value) -> (list (ident* value)%type) -> stmt
-> (map mident value) -> (list (ident* value)%type) -> stmt -> Prop :=