Commit 66c45c70 authored by Martin Clochard's avatar Martin Clochard

mini-compiler: cleanup

parent f7f8465e
theory Imp
use import state.State
use import bool.Bool
use import int.Int
......@@ -29,84 +30,57 @@ theory Imp
(* ************************ SEMANTICS ************************ *)
function aeval (st: state) (e: aexpr) : int =
function aeval (st:state) (e:aexpr) : int =
match e with
| Anum n -> n
| Avar x -> st[x]
| Aadd e1 e2 -> aeval st e1 + aeval st e2
| Asub e1 e2 -> aeval st e1 - aeval st e2
| Amul e1 e2 -> aeval st e1 * aeval st e2
end
function beval (st:state) (b:bexpr) : bool =
match b with
| Btrue -> true
| Bfalse -> false
| Bnot b' -> notb (beval st b')
| Band b1 b2 -> andb (beval st b1) (beval st b2)
| Beq a1 a2 -> aeval st a1 = aeval st a2
| Ble a1 a2 -> aeval st a1 <= aeval st a2
end
function beval (st : state) (b: bexpr) : bool =
match b with
| Btrue -> True
| Bfalse -> False
| Bnot b' -> notb (beval st b')
| Band b1 b2 -> andb (beval st b1) (beval st b2)
| Beq a1 a2 ->
if (aeval st a1) = (aeval st a2) then True else False
| Ble a1 a2 ->
if (aeval st a1) <= (aeval st a2) then True else False
end
(* lemma inversion_beval_t :
forall a1 a2: aexpr, m: state.
beval m (Beq a1 a2) = True -> aeval m a1 = aeval m a2
lemma inversion_beval_f :
forall a1 a2: aexpr, m: state.
beval m (Beq a1 a2) = False -> aeval m a1 <> aeval m a2 *)
inductive ceval state com state =
(* skip *)
| E_Skip :
forall m: state. ceval m Cskip m
(* assignement *)
| E_Ass :
forall m: state, a: aexpr, n: int, x: id.
aeval m a = n ->
ceval m (Cassign x a) m[x <- n]
(* sequence *)
| E_Seq :
forall cmd1 cmd2: com, m0 m1 m2: state.
ceval m0 cmd1 m1 ->
ceval m1 cmd2 m2 ->
ceval m0 (Cseq cmd1 cmd2) m2
(* if then else *)
| E_IfTrue :
forall m0 m1: state, cond: bexpr, cmd1 cmd2: com.
beval m0 cond = True ->
ceval m0 cmd1 m1 ->
ceval m0 (Cif cond cmd1 cmd2) m1
| E_IfFalse :
forall m0 m1: state, cond: bexpr, cmd1 cmd2: com.
beval m0 cond = False ->
ceval m0 cmd2 m1 ->
ceval m0 (Cif cond cmd1 cmd2) m1
(* while *)
| E_WhileEnd :
forall cond: bexpr, m: state, body: com.
beval m cond = False ->
ceval m (Cwhile cond body) m
| E_WhileLoop :
forall mi mj mf: state, cond: bexpr, body: com.
beval mi cond = True ->
ceval mi body mj ->
ceval mj (Cwhile cond body) mf ->
ceval mi (Cwhile cond body) mf
lemma ceval_deterministic_aux :
forall c mi mf1. ceval mi c mf1 -> forall mf2. ("inversion" ceval mi c mf2) -> mf1 = mf2
lemma ceval_deterministic :
forall c mi mf1 mf2. ceval mi c mf1 -> ceval mi c mf2 -> mf1 = mf2
end
\ No newline at end of file
inductive ceval state com state =
(* skip *)
| E_Skip : forall m. ceval m Cskip m
(* assignement *)
| E_Ass : forall m a x. ceval m (Cassign x a) m[x <- aeval m a]
(* sequence *)
| E_Seq : forall cmd1 cmd2 m0 m1 m2.
ceval m0 cmd1 m1 -> ceval m1 cmd2 m2 -> ceval m0 (Cseq cmd1 cmd2) m2
(* if then else *)
| E_IfTrue : forall m0 m1 cond cmd1 cmd2. beval m0 cond ->
ceval m0 cmd1 m1 -> ceval m0 (Cif cond cmd1 cmd2) m1
| E_IfFalse : forall m0 m1 cond cmd1 cmd2. not beval m0 cond ->
ceval m0 cmd2 m1 -> ceval m0 (Cif cond cmd1 cmd2) m1
(* while *)
| E_WhileEnd : forall cond m body. not beval m cond ->
ceval m (Cwhile cond body) m
| E_WhileLoop : forall mi mj mf cond body. beval mi cond ->
ceval mi body mj -> ceval mj (Cwhile cond body) mf ->
ceval mi (Cwhile cond body) mf
lemma ceval_deterministic_aux : forall c mi mf1. ceval mi c mf1 ->
forall mf2. ("inversion" ceval mi c mf2) -> mf1 = mf2
lemma ceval_deterministic : forall c mi mf1 mf2.
ceval mi c mf1 -> ceval mi c mf2 -> mf1 = mf2
end
......@@ -5,9 +5,9 @@
<prover id="0" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="0.95.2" timelimit="5" memlimit="1000"/>
<file name="../imp.why" expanded="true">
<theory name="Imp" sum="8d9b512f0a2a1961484e5a0fa9ff9b68" expanded="true">
<goal name="ceval_deterministic_aux" expanded="true">
<transf name="induction_pr" expanded="true">
<theory name="Imp" sum="d47e4ca50e2ba0ffa18970b5b9819d30">
<goal name="ceval_deterministic_aux">
<transf name="induction_pr">
<goal name="ceval_deterministic_aux.1" expl="1.">
<transf name="inversion_pr">
<goal name="ceval_deterministic_aux.1.1" expl="1.">
......@@ -42,13 +42,13 @@
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="ceval_deterministic_aux.2.3" expl="3.">
<proof prover="1"><result status="valid" time="0.03"/></proof>
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="ceval_deterministic_aux.2.4" expl="4.">
<proof prover="1"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="ceval_deterministic_aux.2.5" expl="5.">
<proof prover="1"><result status="valid" time="0.02"/></proof>
<proof prover="1"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="ceval_deterministic_aux.2.6" expl="6.">
<proof prover="1"><result status="valid" time="0.02"/></proof>
......@@ -185,8 +185,8 @@
</goal>
</transf>
</goal>
<goal name="ceval_deterministic" expanded="true">
<proof prover="1"><result status="valid" time="1.06"/></proof>
<goal name="ceval_deterministic">
<proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
</theory>
</file>
......
......@@ -6,8 +6,8 @@
<prover id="1" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="0.95.2" timelimit="5" memlimit="1000"/>
<prover id="3" name="CVC4" version="1.3" timelimit="5" memlimit="1000"/>
<file name="../logic.mlw" expanded="true">
<theory name="Compiler_logic" sum="01f7b599ba74d4eafec3be887b1930e1" expanded="true">
<file name="../logic.mlw">
<theory name="Compiler_logic" sum="6d58101ef25a960c2128d32f7613d9ec">
<goal name="seq_wp_lemma">
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
......@@ -23,7 +23,7 @@
<goal name="WP_parameter infix ~.1.2.1" expl="1.">
<transf name="compute_specified">
<goal name="WP_parameter infix ~.1.2.1.1" expl="1.">
<proof prover="2"><result status="valid" time="0.23"/></proof>
<proof prover="2"><result status="valid" time="0.05"/></proof>
</goal>
</transf>
</goal>
......@@ -63,9 +63,6 @@
</goal>
</transf>
</goal>
<goal name="trivial_pre_lemma">
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="WP_parameter make_loop_hl" expl="VC for make_loop_hl">
<transf name="split_goal_wp">
<goal name="WP_parameter make_loop_hl.1" expl="1. assertion">
......
theory State
clone export map.Map
type id = Id int
type state = map id int
(*...*)
end
This diff is collapsed.
......@@ -3,31 +3,29 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="CVC3" version="2.4.1" timelimit="5" memlimit="1000"/>
<prover id="1" name="Z3" version="4.3.1" timelimit="5" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="0.95.2" timelimit="5" memlimit="1000"/>
<prover id="3" name="Vampire" version="0.6" timelimit="5" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="0.95.2" timelimit="5" memlimit="1000"/>
<file name="../vm.mlw" expanded="true">
<theory name="ReflTransClosure" sum="41f42e2f3926adcb698b8698151507f0" expanded="true">
<goal name="transition_star_one" expanded="true">
<theory name="ReflTransClosure" sum="41f42e2f3926adcb698b8698151507f0">
<goal name="transition_star_one">
<proof prover="0"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="transition_star_transitive" expanded="true">
<transf name="induction_pr" expanded="true">
<goal name="transition_star_transitive">
<transf name="induction_pr">
<goal name="transition_star_transitive.1" expl="1.">
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="transition_star_transitive.2" expl="2." expanded="true">
<goal name="transition_star_transitive.2" expl="2.">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
</transf>
</goal>
</theory>
<theory name="Vm" sum="ff0e2f36dbba20610ead4bbdaf34a210" expanded="true">
<theory name="Vm" sum="a613e6c8c28ff260907256dd866405f6">
<goal name="codeseq_at_app_right">
<proof prover="3"><result status="valid" time="0.28"/></proof>
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="codeseq_at_app_left">
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="1"><result status="valid" time="0.07"/></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