Commit 2109c25d authored by Asma Tafat-Bouzid's avatar Asma Tafat-Bouzid
Browse files

preuves en cours

parent 93150b7a
......@@ -17,8 +17,7 @@ type value = Vvoid | Vint int | Vbool bool
type operator = Oplus | Ominus | Omult | Ole
(* TODO: introduce two distinct
types mident and ident *)
(** ident for imutable variable*)
type ident
constant result : ident
......@@ -87,13 +86,13 @@ predicate eval_fmla (sigma:env) (pi:stack) (f:fmla) =
| Fand f1 f2 -> eval_fmla sigma pi f1 /\ eval_fmla sigma pi f2
| Fnot f -> not (eval_fmla sigma pi f)
| Fimplies f1 f2 -> eval_fmla sigma pi f1 -> eval_fmla sigma pi f2
| Flet x t f ->
| Flet x t f ->
eval_fmla sigma (Cons (x,eval_term sigma pi t) pi) f
| Fforall x TYint f ->
| Fforall x TYint f ->
forall n:int. eval_fmla sigma (Cons (x,Vint n) pi) f
| Fforall x TYbool f ->
forall b:bool. eval_fmla sigma (Cons (x,Vbool b) pi) f
| Fforall x TYunit f -> eval_fmla sigma (Cons (x,Vvoid) pi) f
| Fforall x TYunit f -> eval_fmla sigma (Cons (x,Vvoid) pi) f
end
(** substitution of a reference [r] by a logic variable [v]
......@@ -102,7 +101,7 @@ predicate eval_fmla (sigma:env) (pi:stack) (f:fmla) =
function subst_term (e:term) (r:ident) (v:ident) : term =
match e with
| Tvalue _ | Tvar _ -> e
| Tderef x -> if r=x then Tvar v else e
| Tderef x -> if r = x then Tvar v else e
| Tbin e1 op e2 -> Tbin (subst_term e1 r v) op (subst_term e2 r v)
end
......@@ -290,7 +289,7 @@ inductive one_step env stack expr env stack expr =
| one_step_while:
forall sigma:env, pi:stack, cond:expr, inv:fmla, body:expr.
(* blocking semantics *)
eval_fmla sigma pi inv ->
eval_fmla sigma pi inv ->
one_step sigma pi (Ewhile cond inv body) sigma pi
(Eif cond (Eseq body (Ewhile cond inv body)) void)
......@@ -501,7 +500,7 @@ lemma assigns_union_right:
forall sigma sigma':env, s1 s2:Set.set ident.
assigns sigma s2 sigma' -> assigns sigma (Set.union s1 s2) sigma'
(** [expr_writes e W] is true when the only references modified by [e] are in [W] *)
(** [expr_writes e W] is true when the only references modified by [e] are in [W] *)
predicate expr_writes (e:expr) (w:Set.set ident) =
match e with
| Evalue _ | Evar _ | Ederef _ | Eassert _ -> true
......@@ -595,7 +594,7 @@ predicate expr_writes (e:expr) (w:Set.set ident) =
| _ -> true
end
lemma decide_value:
lemma decide_value:
forall e:expr. not_a_value e \/ exists v:value. e = Evalue v
lemma progress:
......@@ -604,6 +603,7 @@ predicate expr_writes (e:expr) (w:Set.set ident) =
exists sigma':env, pi':stack, e':expr.
one_step sigma pi e sigma' pi' e'
(*
let rec compute_writes (s:expr) : Set.set ident =
{ }
......@@ -701,7 +701,7 @@ lemma assigns_union_right:
forall sigma sigma':env, s1 s2:Set.set ident.
assigns sigma s2 sigma' -> assigns sigma (Set.union s1 s2) sigma'
(** [expr_writes e W] is true when the only references modified by [e] are in [W] *)
(** [expr_writes e W] is true when the only references modified by [e] are in [W] *)
predicate expr_writes (e:expr) (w:Set.set ident) =
match e with
| Evalue _ | Evar _ | Ederef _ | Eassert _ -> true
......@@ -810,7 +810,7 @@ predicate expr_writes (e:expr) (w:Set.set ident) =
| _ -> true
end
lemma decide_value:
lemma decide_value:
forall e:expr. not_a_value e \/ exists v:value. e = Evalue v
lemma progress:
......
......@@ -582,6 +582,7 @@ Theorem progress : forall (e:expr) (sigma:(map ident value)) (pi:(list
(not_a_value e)) -> exists sigmaqt:(map ident value), exists piqt:(list
(ident* value)%type), exists eqt:expr, (one_step sigma pi e sigmaqt piqt
eqt).
induction e.
simpl; tauto.
(* case 1: e = bin e1 op e2 *)
......@@ -624,7 +625,6 @@ exists pi.
exists (Evalue (eval_bin v o v2)).
apply one_step_bin_value.
(* case 2 : e = var *)
intros sigma pi q (h1 & _).
eexists.
......@@ -661,24 +661,74 @@ eapply one_step_assign_value.
(* case 5: e = e1; e2 *)
destruct (decide_value e1).
(* case 5.1: e1 not a value *)
admit. (* TODO by Asma *)
(* case 1.2: e1 is a value *)
admit. (* TODO by Asma *)
intros sigma pi q (h1 & _).
generalize (IHe1 _ _ _ (conj h1 H)).
intros (sigma' & pi' & e' & h).
exists sigma'.
exists pi'.
exists (Eseq e' e2).
eapply one_step_seq_ctxt; auto.
(* case 5.2: e1 is a value *)
elim H; clear H; intros v He_v.
subst e1.
intros sigma pi q (h2 & h3).
eexists.
exists pi.
eexists.
assert (h: v = Vvoid).
(* problem : typage pour savoir que v est void *)
admit.
subst v.
eapply one_step_seq_value.
(* case 6: e = let id = e1 in e2 *)
(* case 6: e = let i = e1 in e2 *)
destruct (decide_value e1).
(* case 6.1: e1 not a value *)
admit. (* TODO by Asma *)
intros sigma pi q (h1 & _).
generalize (IHe1 _ _ _(conj h1 H)).
intros (sigma' & pi' & e' & h).
exists sigma'.
exists pi'.
exists (Elet i e' e2).
eapply one_step_let_ctxt; auto.
(* case 6.2: e1 is a value *)
admit. (* TODO by Asma *)
elim H; clear H; intros v He_v.
subst e1.
intros sigma pi q (h2 & h3).
eexists.
eexists.
eexists.
eapply one_step_let_value.
(* case 7: e = if e1 then e2 else e3 *)
destruct (decide_value e1).
(* case 6.1: e1 not a value *)
admit. (* TODO by Asma *)
(* case 6.2: e1 is a value *)
(* case 7.1: e1 not a value *)
intros sigma pi q (h1 & _).
simpl in h1.
generalize (IHe1 _ _ _ (conj h1 H)).
intros (sigma' & pi' & e' & h).
exists sigma'.
exists pi'.
exists (Eif e' e2 e3).
eapply one_step_if_ctxt; auto.
(* case 7.2: e1 is a value *)
elim H; clear H; intros v He_v.
subst e1.
intros sigma pi q (h2 & h3).
eexists sigma.
exists pi.
assert (h: v = Vbool true \/ v = Vbool false).
(* problem : typage pour savoir que v est true ou false *)
admit.
destruct h.
eexists.
subst v.
apply one_step_if_true.
subst v.
eexists.
apply one_step_if_false.
(* case 8 : e = assert f *)
intros sigma pi q (h1 & _ ).
......@@ -690,13 +740,13 @@ eexists.
apply one_step_assert; auto.
(* case 9: e = while cond inv body *)
destruct (decide_value e1).
(* case 6.1: e1 not a value *)
admit. (* TODO by Asma *)
(* case 6.2: e1 is a value *)
(* problem : typage pour savoir que v est true ou false *)
admit.
intros sigma pi q (h1, h2).
simpl in h1.
destruct h1.
eexists.
eexists.
eexists.
eapply one_step_while; auto.
Qed.
......
......@@ -39,11 +39,11 @@
locfile="blocking_semantics/../blocking_semantics.mlw"
loclnum="6" loccnumb="7" loccnume="14"
verified="false"
expanded="true">
expanded="false">
<goal
name="get_stack_eq"
locfile="blocking_semantics/../blocking_semantics.mlw"
loclnum="52" loccnumb="6" loccnume="18"
loclnum="51" loccnumb="6" loccnume="18"
sum="ba23f979a9acc92cbd0aa927e6a492e7"
proved="true"
expanded="false"
......@@ -60,7 +60,7 @@
<goal
name="get_stack_neq"
locfile="blocking_semantics/../blocking_semantics.mlw"
loclnum="56" loccnumb="6" loccnume="19"
loclnum="55" loccnumb="6" loccnume="19"
sum="91809042d7f0e3672fb284ce69c7b63a"
proved="true"
expanded="false"
......@@ -77,7 +77,7 @@
<goal
name="eval_subst_term"
locfile="blocking_semantics/../blocking_semantics.mlw"
loclnum="118" loccnumb="6" loccnume="21"
loclnum="117" loccnumb="6" loccnume="21"
sum="2fcafe55c0868db14100e9bd0350077a"
proved="false"
expanded="false"
......@@ -94,7 +94,7 @@
<goal
name="eval_term_change_free"
locfile="blocking_semantics/../blocking_semantics.mlw"
loclnum="124" loccnumb="6" loccnume="27"
loclnum="123" loccnumb="6" loccnume="27"
sum="053c4358587b86d79bd6e10c760fc256"
proved="false"
expanded="false"
......@@ -111,7 +111,7 @@
<goal
name="subst_fresh"
locfile="blocking_semantics/../blocking_semantics.mlw"
loclnum="149" loccnumb="6" loccnume="17"
loclnum="148" loccnumb="6" loccnume="17"
sum="dc909c4eedc136bd149e268ed82f2800"
proved="false"
expanded="false"
......@@ -120,7 +120,7 @@
<goal
name="let_subst"
locfile="blocking_semantics/../blocking_semantics.mlw"
loclnum="153" loccnumb="6" loccnume="15"
loclnum="152" loccnumb="6" loccnume="15"
sum="75341198db12e1de873a8a62cb9ab945"
proved="true"
expanded="false"
......@@ -137,7 +137,7 @@
<goal
name="eval_subst"
locfile="blocking_semantics/../blocking_semantics.mlw"
loclnum="157" loccnumb="6" loccnume="16"
loclnum="156" loccnumb="6" loccnume="16"
sum="518fe956a4a5bed1d2cf79e78f2f3218"
proved="false"
expanded="false"
......@@ -154,7 +154,7 @@
<goal
name="eval_swap"
locfile="blocking_semantics/../blocking_semantics.mlw"
loclnum="163" loccnumb="6" loccnume="15"
loclnum="162" loccnumb="6" loccnume="15"
sum="0c6f04d96cf19c9559352c53aa2e442c"
proved="false"
expanded="false"
......@@ -171,7 +171,7 @@
<goal
name="eval_change_free"
locfile="blocking_semantics/../blocking_semantics.mlw"
loclnum="169" loccnumb="6" loccnume="22"
loclnum="168" loccnumb="6" loccnume="22"
sum="a66e7b11a74776933b206a164b0a40ea"
proved="false"
expanded="false"
......@@ -188,10 +188,10 @@
<goal
name="let_equiv"
locfile="blocking_semantics/../blocking_semantics.mlw"
loclnum="178" loccnumb="6" loccnume="15"
loclnum="177" loccnumb="6" loccnume="15"
sum="80318f792bd853c1b1a5e1e5e4dbf547"
proved="false"
expanded="true"
expanded="false"
shape="aeval_fmlaV4V5aFletV0V2V3Iaeval_fmlaV4V5aFletV1V2asubstV3V0V1FF">
<proof
prover="0"
......@@ -205,7 +205,7 @@
<goal
name="steps_non_neg"
locfile="blocking_semantics/../blocking_semantics.mlw"
loclnum="308" loccnumb="8" loccnume="21"
loclnum="307" loccnumb="8" loccnume="21"
sum="dc0a28ea13d0f5917cd6a59803232637"
proved="false"
expanded="false"
......@@ -222,7 +222,7 @@
<goal
name="many_steps_seq"
locfile="blocking_semantics/../blocking_semantics.mlw"
loclnum="312" loccnumb="8" loccnume="22"
loclnum="311" loccnumb="8" loccnume="22"
sum="1c3f781ce8d67850c418f9caa7dd6fc9"
proved="false"
expanded="false"
......@@ -239,7 +239,7 @@
<goal
name="many_steps_let"
locfile="blocking_semantics/../blocking_semantics.mlw"
loclnum="320" loccnumb="8" loccnume="22"
loclnum="319" loccnumb="8" loccnume="22"
sum="62edc3347ac0ffd5cb87dbca85565b20"
proved="false"
expanded="false"
......@@ -256,7 +256,7 @@
<goal
name="one_step_change_free"
locfile="blocking_semantics/../blocking_semantics.mlw"
loclnum="328" loccnumb="7" loccnume="27"
loclnum="327" loccnumb="7" loccnume="27"
sum="b803db2b4215fb56c3ef30091b108324"
proved="false"
expanded="false"
......@@ -266,13 +266,13 @@
<theory
name="TestSemantics"
locfile="blocking_semantics/../blocking_semantics.mlw"
loclnum="355" loccnumb="7" loccnume="20"
loclnum="354" loccnumb="7" loccnume="20"
verified="false"
expanded="false">
<goal
name="Test13"
locfile="blocking_semantics/../blocking_semantics.mlw"
loclnum="363" loccnumb="5" loccnume="11"
loclnum="362" loccnumb="5" loccnume="11"
sum="5470eecd18c482465080854e9b23b7b7"
proved="true"
expanded="false"
......@@ -289,7 +289,7 @@
<goal
name="Test13expr"
locfile="blocking_semantics/../blocking_semantics.mlw"
loclnum="366" loccnumb="5" loccnume="15"
loclnum="365" loccnumb="5" loccnume="15"
sum="ae7b49ba66863aa9e589cec426679317"
proved="true"
expanded="false"
......@@ -306,7 +306,7 @@
<goal
name="Test42"
locfile="blocking_semantics/../blocking_semantics.mlw"
loclnum="369" loccnumb="5" loccnume="11"
loclnum="368" loccnumb="5" loccnume="11"
sum="d68c7df88e341b31ac064b4b383bbb9b"
proved="true"
expanded="false"
......@@ -323,7 +323,7 @@
<goal
name="Test42expr"
locfile="blocking_semantics/../blocking_semantics.mlw"
loclnum="372" loccnumb="5" loccnume="15"
loclnum="371" loccnumb="5" loccnume="15"
sum="a9fc2cf4fc4cde61622c19948d63c9ba"
proved="false"
expanded="false"
......@@ -372,7 +372,7 @@
<goal
name="Test0"
locfile="blocking_semantics/../blocking_semantics.mlw"
loclnum="375" loccnumb="5" loccnume="10"
loclnum="374" loccnumb="5" loccnume="10"
sum="b5aaeaab59a26ee76c24020f3656525f"
proved="true"
expanded="false"
......@@ -389,7 +389,7 @@
<goal
name="Test0expr"
locfile="blocking_semantics/../blocking_semantics.mlw"
loclnum="378" loccnumb="5" loccnume="14"
loclnum="377" loccnumb="5" loccnume="14"
sum="11d3fc033b6a989ac73f6014c6e9e22c"
proved="false"
expanded="false"
......@@ -438,7 +438,7 @@
<goal
name="Test55"
locfile="blocking_semantics/../blocking_semantics.mlw"
loclnum="381" loccnumb="5" loccnume="11"
loclnum="380" loccnumb="5" loccnume="11"
sum="15475684f514243fe041e90468182f07"
proved="false"
expanded="false"
......@@ -487,7 +487,7 @@
<goal
name="Test55expr"
locfile="blocking_semantics/../blocking_semantics.mlw"
loclnum="384" loccnumb="5" loccnume="15"
loclnum="383" loccnumb="5" loccnume="15"
sum="99e91d2c91df5e92337b88237413b180"
proved="false"
expanded="false"
......@@ -536,7 +536,7 @@
<goal
name="Ass42"
locfile="blocking_semantics/../blocking_semantics.mlw"
loclnum="387" loccnumb="5" loccnume="10"
loclnum="386" loccnumb="5" loccnume="10"
sum="db1d25439495f9ccb031facb3e930a58"
proved="true"
expanded="false"
......@@ -553,7 +553,7 @@
<goal
name="If42"
locfile="blocking_semantics/../blocking_semantics.mlw"
loclnum="392" loccnumb="5" loccnume="9"
loclnum="391" loccnumb="5" loccnume="9"
sum="2d42fdcfd14985369a83947e4dda969b"
proved="false"
expanded="false"
......@@ -571,13 +571,13 @@
<theory
name="HoareLogic"
locfile="blocking_semantics/../blocking_semantics.mlw"
loclnum="406" loccnumb="7" loccnume="17"
loclnum="405" loccnumb="7" loccnume="17"
verified="false"
expanded="false">
<goal
name="consequence_rule"
locfile="blocking_semantics/../blocking_semantics.mlw"
loclnum="413" loccnumb="6" loccnume="22"
loclnum="412" loccnumb="6" loccnume="22"
sum="bc3818e5d5168b103a85bf7bab9e2808"
proved="false"
expanded="false"
......@@ -594,7 +594,7 @@
<goal
name="value_rule"
locfile="blocking_semantics/../blocking_semantics.mlw"
loclnum="420" loccnumb="6" loccnume="16"
loclnum="419" loccnumb="6" loccnume="16"
sum="482d9785580ad1fe01d446da39d85151"
proved="true"
expanded="false"
......@@ -611,7 +611,7 @@
<goal
name="assign_rule"
locfile="blocking_semantics/../blocking_semantics.mlw"
loclnum="424" loccnumb="6" loccnume="17"
loclnum="423" loccnumb="6" loccnume="17"
sum="65b35c83f9d3aa5384455ec7343da90f"
proved="false"
expanded="false"
......@@ -628,7 +628,7 @@
<goal
name="seq_rule"
locfile="blocking_semantics/../blocking_semantics.mlw"
loclnum="429" loccnumb="6" loccnume="14"
loclnum="428" loccnumb="6" loccnume="14"
sum="261184d5d8045756e5e74ceb458a5a0c"
proved="false"
expanded="false"
......@@ -645,7 +645,7 @@
<goal
name="let_rule"
locfile="blocking_semantics/../blocking_semantics.mlw"
loclnum="434" loccnumb="6" loccnume="14"
loclnum="433" loccnumb="6" loccnume="14"
sum="2a7044f47dcc32ba17422270e37490e5"
proved="false"
expanded="false"
......@@ -662,7 +662,7 @@
<goal
name="assert_rule"
locfile="blocking_semantics/../blocking_semantics.mlw"
loclnum="448" loccnumb="6" loccnume="17"
loclnum="447" loccnumb="6" loccnume="17"
sum="b590c17fe8762e6f9768bf398bf7c266"
proved="false"
expanded="false"
......@@ -679,7 +679,7 @@
<goal
name="assert_rule_ext"
locfile="blocking_semantics/../blocking_semantics.mlw"
loclnum="452" loccnumb="6" loccnume="21"
loclnum="451" loccnumb="6" loccnume="21"
sum="9b3011ef24753b7d67345b07f33a00e2"
proved="false"
expanded="false"
......@@ -697,13 +697,13 @@
<theory
name="WP"
locfile="blocking_semantics/../blocking_semantics.mlw"
loclnum="475" loccnumb="7" loccnume="9"
loclnum="474" loccnumb="7" loccnume="9"
verified="false"
expanded="true">
expanded="false">
<goal
name="assigns_refl"
locfile="blocking_semantics/../blocking_semantics.mlw"
loclnum="488" loccnumb="6" loccnume="18"
loclnum="487" loccnumb="6" loccnume="18"
sum="72b15dac60cdba92f8ef1583adb713ea"
proved="true"
expanded="false"
......@@ -720,7 +720,7 @@
<goal
name="assigns_trans"
locfile="blocking_semantics/../blocking_semantics.mlw"
loclnum="491" loccnumb="6" loccnume="19"
loclnum="490" loccnumb="6" loccnume="19"
sum="ed306518411caf9441faecfdee474b99"
proved="true"
expanded="false"
......@@ -737,7 +737,7 @@
<goal
name="assigns_union_left"
locfile="blocking_semantics/../blocking_semantics.mlw"
loclnum="496" loccnumb="6" loccnume="24"
loclnum="495" loccnumb="6" loccnume="24"
sum="2d54a7cc084759c7825a7a1a1e87eb36"
proved="true"
expanded="false"
......@@ -754,7 +754,7 @@
<goal
name="assigns_union_right"
locfile="blocking_semantics/../blocking_semantics.mlw"
loclnum="500" loccnumb="6" loccnume="25"
loclnum="499" loccnumb="6" loccnume="25"
sum="aa1889e101e9ccc1ad42aa2d02c00022"
proved="true"
expanded="false"
......@@ -771,7 +771,7 @@
<goal
name="wp_subst"
locfile="blocking_semantics/../blocking_semantics.mlw"
loclnum="564" loccnumb="8" loccnume="16"
loclnum="563" loccnumb="8" loccnume="16"
sum="332ac227a145197f6bd46f146aa96d2d"
proved="false"
expanded="false"
......@@ -780,7 +780,7 @@
<goal
name="wp_implies"
locfile="blocking_semantics/../blocking_semantics.mlw"
loclnum="569" loccnumb="8" loccnume="18"
loclnum="568" loccnumb="8" loccnume="18"
sum="bfcc2e44c5b5d93ca4e466a6f0282fb4"
proved="false"
expanded="false"
......@@ -789,10 +789,10 @@
<goal
name="wp_conj"
locfile="blocking_semantics/../blocking_semantics.mlw"
loclnum="578" loccnumb="8" loccnume="15"
loclnum="577" loccnumb="8" loccnume="15"
sum="4667ed4a9c6a9562519071e071c49658"
proved="false"
expanded="true"
expanded="false"
shape="aeval_fmlaV0V1awpV2V4Aaeval_fmlaV0V1awpV2V3qaeval_fmlaV0V1awpV2aFandV3V4F">
<proof
prover="4"
......@@ -807,10 +807,10 @@
<goal
name="wp_reduction"
locfile="blocking_semantics/../blocking_semantics.mlw"
loclnum="585" loccnumb="8" loccnume="20"
loclnum="584" loccnumb="8" loccnume="20"
sum="d6e1b0dcab971053679571b187e6fc79"
proved="false"
expanded="true"
expanded="false"
shape="aeval_fmlaV1V3awpV5V6Iaeval_fmlaV0V2awpV4V6FIaone_stepV0V2V4V1V3V5F">
<proof
prover="5"
......@@ -873,10 +873,10 @@
<goal
name="decide_value"
locfile="blocking_semantics/../blocking_semantics.mlw"
loclnum="598" loccnumb="8" loccnume="20"
loclnum="597" loccnumb="8" loccnume="20"
sum="3e267bc8fc7e9052d2c5a67aae0ed910"
proved="true"
expanded="true"
expanded="false"
shape="ainfix =V0aEvalueV1EOanot_a_valueV0F">
<proof
prover="0"
......@@ -890,19 +890,19 @@
<goal
name="progress"
locfile="blocking_semantics/../blocking_semantics.mlw"
loclnum="601" loccnumb="8" loccnume="16"
loclnum="600" loccnumb="8" loccnume="16"
sum="072d27a9e7a5198432dee86ea2dee213"
proved="true"
expanded="true"
expanded="false"
shape="aone_stepV1V2V0V4V5V6EIanot_a_valueV0Aaeval_fmlaV1V2awpV0V3F">
<proof
prover="4"
timelimit="5"
memlimit="1000"
timelimit="3"
memlimit="0"
edited="blocking_semantics_WP_progress_1.v"
obsolete="false"
archived="false">
<result status="valid" time="0.65"/>
<result status="valid" time="0.74"/>
</proof>
</goal>
</theory>
......
This diff is collapsed.