Commit 3db7ba50 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

blocking_semantics3 continued

parent 06860f87
......@@ -460,7 +460,7 @@ inductive one_step env stack stmt env stack stmt =
one_step sigma pi (Swhile cond inv body) sigma pi
(Sseq body (Swhile cond inv body))
| one_step_while_falsee:
| one_step_while_false:
forall sigma:env, pi:stack, cond:term, inv:fmla, body:stmt.
(* blocking semantics *)
eval_fmla sigma pi inv ->
......@@ -668,6 +668,11 @@ predicate stmt_writes (s:stmt) (w:Set.set mident) =
function abstract_effects (s:stmt) (f:fmla) : fmla
axiom abstract_effects_generalize :
forall sigma:env, pi:stack, s:stmt, f:fmla.
eval_fmla sigma pi (abstract_effects s f) ->
eval_fmla sigma pi f
function wp (s:stmt) (q:fmla) : fmla =
match s with
| Sskip -> q
......@@ -691,6 +696,12 @@ predicate stmt_writes (s:stmt) (w:Set.set mident) =
end
axiom abstract_effects_writes :
forall sigma:env, pi:stack, s:stmt, q:fmla.
eval_fmla sigma pi (abstract_effects s q) ->
eval_fmla sigma pi (wp s (abstract_effects s q))
(* lemma wp_subst: *)
(* forall e:expr, q:fmla, id :mident, id':ident. *)
(* fresh_in_stmt id e -> *)
......
......@@ -314,6 +314,11 @@ Fixpoint eval_term(sigma:(map mident value)) (pi:(list (ident* value)%type))
(eval_term sigma pi t2))
end.
Axiom eval_bool_term : forall (sigma:(map mident value)) (pi:(list (ident*
value)%type)) (sigmat:(map mident datatype)) (pit:(list (ident*
datatype)%type)) (t:term), (type_term sigmat pit t TYbool) ->
exists b:bool, ((eval_term sigma pi t) = (Vbool b)).
(* Why3 assumption *)
Fixpoint eval_fmla(sigma:(map mident value)) (pi:(list (ident* value)%type))
(f:fmla) {struct f}: Prop :=
......@@ -717,7 +722,12 @@ Theorem progress : forall (s:stmt),
destruct s; auto.
intros.
inversion H1; subst; clear H1.
elim (eval_bool_term sigma pi _ _ _ H9).
destruct x; intros Hval.
do 3 eexists.
apply one_step_if_true; auto.
do 3 eexists.
apply one_step_if_false; auto.
Qed.
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require int.MinMax.
(* Why3 assumption *)
Inductive list (a:Type) :=
Inductive list (a:Type) {a_WT:WhyType a} :=
| Nil : list a
| Cons : a -> (list a) -> list a.
Implicit Arguments Nil [[a]].
Implicit Arguments Cons [[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]].
Parameter map : forall (a:Type) (b:Type), Type.
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} {b:Type}, (map a b) -> a -> b.
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} {b:Type}, (map a b) -> a -> b -> (map 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} {b:Type}, forall (m:(map a b)),
forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) -> ((get (set m a1 b1)
a2) = b1).
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} {b:Type}, forall (m:(map a b)),
forall (a1:a) (a2:a), forall (b1:b), (~ (a1 = a2)) -> ((get (set m a1 b1)
a2) = (get m a2)).
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} {b:Type}, b -> (map a b).
Parameter const: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
b -> (map a b).
Axiom Const : forall {a:Type} {b:Type}, forall (b1:b) (a1:a),
((get (const b1:(map a b)) a1) = b1).
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 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 .
Axiom value_WhyType : WhyType value.
Existing Instance value_WhyType.
(* Why3 assumption *)
Inductive operator :=
......@@ -49,12 +61,18 @@ Inductive operator :=
| Ominus : operator
| Omult : operator
| Ole : operator .
Axiom operator_WhyType : WhyType operator.
Existing Instance operator_WhyType.
Parameter mident : Type.
Axiom mident : Type.
Parameter mident_WhyType : WhyType mident.
Existing Instance mident_WhyType.
(* Why3 assumption *)
Inductive ident :=
| mk_ident : Z -> ident .
Axiom ident_WhyType : WhyType ident.
Existing Instance ident_WhyType.
(* Why3 assumption *)
Definition ident_index(v:ident): Z := match v with
......@@ -66,11 +84,14 @@ Inductive term_node :=
| Tvalue : value -> term_node
| Tvar : ident -> term_node
| Tderef : mident -> term_node
| Tbin : term -> operator -> term -> term_node .
(* Why3 assumption *)
Inductive term :=
| Tbin : term -> operator -> term -> term_node
with term :=
| mk_term : term_node -> Z -> term .
Axiom term_WhyType : WhyType term.
Existing Instance term_WhyType.
Axiom term_node_WhyType : WhyType term_node.
Existing Instance term_node_WhyType.
(* Why3 assumption *)
Definition term_maxvar(v:term): Z := match v with
......@@ -127,6 +148,8 @@ Inductive 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 :=
......@@ -136,12 +159,16 @@ Inductive 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).
(* Why3 assumption *)
Definition type_value(v:value): datatype :=
match v with
| Vvoid => TYunit
| (Vint int1) => TYint
| (Vint int) => TYint
| (Vbool bool1) => TYbool
end.
......@@ -287,6 +314,11 @@ Fixpoint eval_term(sigma:(map mident value)) (pi:(list (ident* value)%type))
(eval_term sigma pi t2))
end.
Axiom eval_bool_term : forall (sigma:(map mident value)) (pi:(list (ident*
value)%type)) (sigmat:(map mident datatype)) (pit:(list (ident*
datatype)%type)) (t:term), (type_term sigmat pit t TYbool) ->
exists b:bool, ((eval_term sigma pi t) = (Vbool b)).
(* Why3 assumption *)
Fixpoint eval_fmla(sigma:(map mident value)) (pi:(list (ident* value)%type))
(f:fmla) {struct f}: Prop :=
......@@ -467,7 +499,7 @@ Inductive one_step : (map mident value) -> (list (ident* value)%type) -> stmt
value)%type)) (cond:term) (inv:fmla) (body:stmt), (eval_fmla sigma pi
inv) -> (((eval_term sigma pi cond) = (Vbool true)) -> (one_step sigma
pi (Swhile cond inv body) sigma pi (Sseq body (Swhile cond inv body))))
| one_step_while_falsee : forall (sigma:(map mident value)) (pi:(list
| one_step_while_false : forall (sigma:(map mident value)) (pi:(list
(ident* value)%type)) (cond:term) (inv:fmla) (body:stmt),
(eval_fmla sigma pi inv) -> (((eval_term sigma pi
cond) = (Vbool false)) -> (one_step sigma pi (Swhile cond inv body)
......@@ -518,70 +550,80 @@ Definition total_valid_triple(p:fmla) (s:stmt) (q:fmla): Prop :=
exists pi':(list (ident* value)%type), exists n:Z, (many_steps sigma pi s
sigma' pi' Sskip n) /\ (eval_fmla sigma' pi' q).
Parameter set1 : forall (a:Type), Type.
Axiom set1 : forall (a:Type) {a_WT:WhyType a}, Type.
Parameter set1_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (set1 a).
Existing Instance set1_WhyType.
Parameter mem: forall {a:Type}, a -> (set1 a) -> Prop.
Parameter mem: forall {a:Type} {a_WT:WhyType a}, a -> (set1 a) -> Prop.
(* Why3 assumption *)
Definition infix_eqeq {a:Type}(s1:(set1 a)) (s2:(set1 a)): Prop :=
forall (x:a), (mem x s1) <-> (mem x s2).
Definition infix_eqeq {a:Type} {a_WT:WhyType a}(s1:(set1 a)) (s2:(set1
a)): Prop := forall (x:a), (mem x s1) <-> (mem x s2).
Axiom extensionality : forall {a:Type}, forall (s1:(set1 a)) (s2:(set1 a)),
(infix_eqeq s1 s2) -> (s1 = s2).
Axiom extensionality : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set1 a))
(s2:(set1 a)), (infix_eqeq s1 s2) -> (s1 = s2).
(* Why3 assumption *)
Definition subset {a:Type}(s1:(set1 a)) (s2:(set1 a)): Prop := forall (x:a),
(mem x s1) -> (mem x s2).
Definition subset {a:Type} {a_WT:WhyType a}(s1:(set1 a)) (s2:(set1
a)): Prop := forall (x:a), (mem x s1) -> (mem x s2).
Axiom subset_trans : forall {a:Type}, forall (s1:(set1 a)) (s2:(set1 a))
(s3:(set1 a)), (subset s1 s2) -> ((subset s2 s3) -> (subset s1 s3)).
Axiom subset_trans : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set1 a))
(s2:(set1 a)) (s3:(set1 a)), (subset s1 s2) -> ((subset s2 s3) ->
(subset s1 s3)).
Parameter empty: forall {a:Type}, (set1 a).
Parameter empty: forall {a:Type} {a_WT:WhyType a}, (set1 a).
(* Why3 assumption *)
Definition is_empty {a:Type}(s:(set1 a)): Prop := forall (x:a), ~ (mem x s).
Definition is_empty {a:Type} {a_WT:WhyType a}(s:(set1 a)): Prop :=
forall (x:a), ~ (mem x s).
Axiom empty_def1 : forall {a:Type}, (is_empty (empty :(set1 a))).
Axiom empty_def1 : forall {a:Type} {a_WT:WhyType a}, (is_empty (empty :(set1
a))).
Parameter add: forall {a:Type}, a -> (set1 a) -> (set1 a).
Parameter add: forall {a:Type} {a_WT:WhyType a}, a -> (set1 a) -> (set1 a).
Axiom add_def1 : forall {a:Type}, forall (x:a) (y:a), forall (s:(set1 a)),
(mem x (add y s)) <-> ((x = y) \/ (mem x s)).
Axiom add_def1 : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (y:a),
forall (s:(set1 a)), (mem x (add y s)) <-> ((x = y) \/ (mem x s)).
Parameter remove: forall {a:Type}, a -> (set1 a) -> (set1 a).
Parameter remove: forall {a:Type} {a_WT:WhyType a}, a -> (set1 a) -> (set1
a).
Axiom remove_def1 : forall {a:Type}, forall (x:a) (y:a) (s:(set1 a)), (mem x
(remove y s)) <-> ((~ (x = y)) /\ (mem x s)).
Axiom remove_def1 : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (y:a)
(s:(set1 a)), (mem x (remove y s)) <-> ((~ (x = y)) /\ (mem x s)).
Axiom subset_remove : forall {a:Type}, forall (x:a) (s:(set1 a)),
(subset (remove x s) s).
Axiom subset_remove : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (s:(set1
a)), (subset (remove x s) s).
Parameter union: forall {a:Type}, (set1 a) -> (set1 a) -> (set1 a).
Parameter union: forall {a:Type} {a_WT:WhyType a}, (set1 a) -> (set1 a) ->
(set1 a).
Axiom union_def1 : forall {a:Type}, forall (s1:(set1 a)) (s2:(set1 a)) (x:a),
(mem x (union s1 s2)) <-> ((mem x s1) \/ (mem x s2)).
Axiom union_def1 : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set1 a))
(s2:(set1 a)) (x:a), (mem x (union s1 s2)) <-> ((mem x s1) \/ (mem x s2)).
Parameter inter: forall {a:Type}, (set1 a) -> (set1 a) -> (set1 a).
Parameter inter: forall {a:Type} {a_WT:WhyType a}, (set1 a) -> (set1 a) ->
(set1 a).
Axiom inter_def1 : forall {a:Type}, forall (s1:(set1 a)) (s2:(set1 a)) (x:a),
(mem x (inter s1 s2)) <-> ((mem x s1) /\ (mem x s2)).
Axiom inter_def1 : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set1 a))
(s2:(set1 a)) (x:a), (mem x (inter s1 s2)) <-> ((mem x s1) /\ (mem x s2)).
Parameter diff: forall {a:Type}, (set1 a) -> (set1 a) -> (set1 a).
Parameter diff: forall {a:Type} {a_WT:WhyType a}, (set1 a) -> (set1 a) ->
(set1 a).
Axiom diff_def1 : forall {a:Type}, forall (s1:(set1 a)) (s2:(set1 a)) (x:a),
(mem x (diff s1 s2)) <-> ((mem x s1) /\ ~ (mem x s2)).
Axiom diff_def1 : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set1 a))
(s2:(set1 a)) (x:a), (mem x (diff s1 s2)) <-> ((mem x s1) /\ ~ (mem x s2)).
Axiom subset_diff : forall {a:Type}, forall (s1:(set1 a)) (s2:(set1 a)),
(subset (diff s1 s2) s1).
Axiom subset_diff : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set1 a))
(s2:(set1 a)), (subset (diff s1 s2) s1).
Parameter choose: forall {a:Type}, (set1 a) -> a.
Parameter choose: forall {a:Type} {a_WT:WhyType a}, (set1 a) -> a.
Axiom choose_def : forall {a:Type}, forall (s:(set1 a)), (~ (is_empty s)) ->
(mem (choose s) s).
Axiom choose_def : forall {a:Type} {a_WT:WhyType a}, forall (s:(set1 a)),
(~ (is_empty s)) -> (mem (choose s) s).
Parameter all: forall {a:Type}, (set1 a).
Parameter all: forall {a:Type} {a_WT:WhyType a}, (set1 a).
Axiom all_def : forall {a:Type}, forall (x:a), (mem x (all :(set1 a))).
Axiom all_def : forall {a:Type} {a_WT:WhyType a}, forall (x:a), (mem x
(all :(set1 a))).
(* Why3 assumption *)
Definition assigns(sigma:(map mident value)) (a:(set1 mident)) (sigma':(map
......@@ -623,6 +665,10 @@ Axiom fresh_from_stmt : forall (s:stmt) (f:fmla),
Parameter abstract_effects: stmt -> fmla -> fmla.
Axiom abstract_effects_generalize : forall (sigma:(map mident value))
(pi:(list (ident* value)%type)) (s:stmt) (f:fmla), (eval_fmla sigma pi
(abstract_effects s f)) -> (eval_fmla sigma pi f).
(* Why3 assumption *)
Fixpoint wp(s:stmt) (q:fmla) {struct s}: fmla :=
match s with
......@@ -638,6 +684,11 @@ Fixpoint wp(s:stmt) (q:fmla) {struct s}: fmla :=
(Fimplies (Fand (Fnot (Fterm cond)) inv) q))))
end.
Axiom abstract_effects_writes : forall (sigma:(map mident value)) (pi:(list
(ident* value)%type)) (s:stmt) (q:fmla), (eval_fmla sigma pi
(abstract_effects s q)) -> (eval_fmla sigma pi (wp s (abstract_effects s
q))).
Axiom distrib_conj : forall (sigma:(map mident value)) (pi:(list (ident*
value)%type)) (s:stmt) (p:fmla) (q:fmla), (eval_fmla sigma pi (wp s (Fand p
q))) <-> ((eval_fmla sigma pi (wp s p)) /\ (eval_fmla sigma pi (wp s q))).
......@@ -650,7 +701,59 @@ Theorem wp_reduction : forall (sigma:(map mident value)) (sigma':(map mident
value)) (pi:(list (ident* value)%type)) (pi':(list (ident* value)%type))
(s:stmt) (s':stmt), (one_step sigma pi s sigma' pi' s') -> forall (q:fmla),
(eval_fmla sigma pi (wp s q)) -> (eval_fmla sigma' pi' (wp s' q)).
intros sigma sigma' pi pi' s s' h1 q h2.
induction 1; intros q Hq.
(* case Sassign *)
simpl.
simpl in Hq.
rewrite eval_msubst in Hq.
(* TODO *)
(* case Sseq *)
simpl.
apply IHone_step.
apply Hq.
(* case Skip ; s2 *)
simpl in Hq; auto.
(* case if true *)
simpl in Hq.
intuition.
(* case if false *)
simpl in Hq.
destruct Hq as (_ & h2).
apply h2.
rewrite H; discriminate.
(* case assert *)
simpl.
simpl in Hq.
intuition.
(* case While true *)
simpl.
simpl in Hq.
destruct Hq as (h1 & h2).
rewrite distrib_conj; split.
generalize (abstract_effects_generalize _ _ _ _ h2).
intros h3.
simpl in h3.
intuition.
apply abstract_effects_writes; auto.
(* case While False *)
simpl.
simpl in Hq.
destruct Hq as (h1 & h2).
generalize (abstract_effects_generalize _ _ _ _ h2).
intros h3.
simpl in h3.
destruct h3 as (_ & h4).
apply h4.
split; auto.
rewrite H0; discriminate.
Qed.
......
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