Commit 0a03ce52 by MARCHE Claude

### WP on expressions

parent af9d5d0b
 name="examples/hoare_logic/wp2/why3session.xml"> expanded="true"> expanded="true"> expanded="true"> expanded="false"> expanded="false">
 (** {1 A certified WP calculus} *) (** {2 A simple imperative language with expressions, syntax and semantics} *) theory ImpExpr use import int.Int use import bool.Bool (** types and values *) type datatype = TYunit | TYint | TYbool type value = Vvoid | Vint int | Vbool bool (** terms and formulas *) type operator = Oplus | Ominus | Omult | Ole type ident = int constant result : ident = (-1) type term = | Tvalue value | Tvar ident | Tderef ident | Tbin term operator term type fmla = | Fterm term | Fand fmla fmla | Fnot fmla | Fimplies fmla fmla | Flet ident term fmla | Fforall ident datatype fmla use map.Map as IdMap type env = IdMap.map ident value (** semantics of formulas *) function eval_bin (x:value) (op:operator) (y:value) : value = match x,y with | Vint x,Vint y -> match op with | Oplus -> Vint (x+y) | Ominus -> Vint (x-y) | Omult -> Vint (x*y) | Ole -> Vbool (if x <= y then True else False) end | _,_ -> Vbool False end function get_env (i:ident) (e:env) : value = IdMap.get e i function eval_term (sigma:env) (pi:env) (t:term) : value = match t with | Tvalue v -> v | Tvar id -> get_env id pi | Tderef id -> get_env id sigma | Tbin t1 op t2 -> eval_bin (eval_term sigma pi t1) op (eval_term sigma pi t2) end predicate eval_fmla (sigma:env) (pi:env) (f:fmla) = 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 f -> not (eval_fmla sigma pi f) | Fimplies f1 f2 -> eval_fmla sigma pi f1 -> eval_fmla sigma pi f2 | Flet x t f -> eval_fmla sigma (IdMap.set pi x (eval_term sigma pi t)) f | Fforall x TYint f -> forall n:int. eval_fmla sigma (IdMap.set pi x (Vint n)) f | Fforall x TYbool f -> forall b:bool. eval_fmla sigma (IdMap.set pi x (Vbool b)) f | Fforall x TYunit f -> eval_fmla sigma (IdMap.set pi x Vvoid) f end (** substitution of a reference [r] by a logic variable [v] warning: proper behavior only guaranted if [v] is fresh *) 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 | Tbin e1 op e2 -> Tbin (subst_term e1 r v) op (subst_term e2 r v) end predicate fresh_in_term (id:ident) (t:term) = match t with | Tvalue _ -> true | Tvar v -> id <> v | Tderef _ -> true | Tbin t1 _ t2 -> fresh_in_term id t1 /\ fresh_in_term id t2 end lemma eval_subst_term: forall sigma pi:env, e:term, x:ident, v:ident. fresh_in_term v e -> eval_term sigma pi (subst_term e x v) = eval_term (IdMap.set sigma x (IdMap.get pi v)) pi e lemma eval_term_change_free : forall t:term, sigma pi:env, id:ident, v:value. fresh_in_term id t -> eval_term sigma (IdMap.set pi id v) t = eval_term sigma pi t predicate fresh_in_fmla (id:ident) (f:fmla) = match f with | Fterm e -> fresh_in_term id e | Fand f1 f2 | Fimplies f1 f2 -> fresh_in_fmla id f1 /\ fresh_in_fmla id f2 | Fnot f -> fresh_in_fmla id f | Flet y t f -> id <> y /\ fresh_in_term id t /\ fresh_in_fmla id f | Fforall y ty f -> id <> y /\ fresh_in_fmla id f end function subst (f:fmla) (x:ident) (v:ident) : fmla = match f with | Fterm e -> Fterm (subst_term e x v) | Fand f1 f2 -> Fand (subst f1 x v) (subst f2 x v) | Fnot f -> Fnot (subst f x v) | Fimplies f1 f2 -> Fimplies (subst f1 x v) (subst f2 x v) | Flet y t f -> Flet y (subst_term t x v) (subst f x v) | Fforall y ty f -> Fforall y ty (subst f x v) end lemma eval_subst: forall f:fmla, sigma pi:env, x:ident, v:ident. fresh_in_fmla v f -> (eval_fmla sigma pi (subst f x v) <-> eval_fmla (IdMap.set sigma x (IdMap.get pi v)) pi f) lemma eval_swap: forall f:fmla, sigma pi:env, id1 id2:ident, v1 v2:value. id1 <> id2 -> (eval_fmla sigma (IdMap.set (IdMap.set pi id1 v1) id2 v2) f <-> eval_fmla sigma (IdMap.set (IdMap.set pi id2 v2) id1 v1) f) lemma eval_change_free : forall f:fmla, sigma pi:env, id:ident, v:value. fresh_in_fmla id f -> (eval_fmla sigma (IdMap.set pi id v) f <-> eval_fmla sigma pi f) (* expressions *) type expr = | Evalue value | Ebin expr operator expr | Evar ident | Ederef ident | Eassign ident expr | Eseq expr expr | Elet ident expr expr | Eif expr expr expr | Eassert fmla | Ewhile expr fmla expr constant void : expr = Evalue Vvoid (* lemma check_skip: forall s:stmt. s=Sskip \/s<>Sskip *) (** small-steps semantics for statements *) inductive one_step env env expr env env expr = | one_step_assign_ctxt: forall sigma pi sigma' pi':env, x:ident, e e':expr. one_step sigma pi e sigma' pi' e' -> one_step sigma pi (Eassign x e) sigma' pi' (Eassign x e') | one_step_assign_value: forall sigma pi:env, x:ident, v:value, e:term. one_step sigma pi (Eassign x (Evalue v)) (IdMap.set sigma x v) pi void | one_step_seq_ctxt: forall sigma pi sigma' pi':env, e1 e1' e2:expr. one_step sigma pi e1 sigma' pi' e1' -> one_step sigma pi (Eseq e1 e2) sigma' pi' (Eseq e1' e2) | one_step_seq_value: forall sigma pi:env, id:ident, e:expr. one_step sigma pi (Eseq void e) sigma pi e | one_step_let_ctxt: forall sigma pi sigma' pi':env, id:ident, e1 e1' e2:expr. one_step sigma pi e1 sigma' pi' e1' -> one_step sigma pi (Elet id e1 e2) sigma' pi' (Elet id e1' e2) | one_step_let_value: forall sigma pi:env, id:ident, v:value, e:expr. one_step sigma pi (Elet id (Evalue v) e) sigma (IdMap.set pi id v) e | one_step_if_ctxt: forall sigma pi sigma' pi':env, id:ident, e1 e1' e2 e3:expr. one_step sigma pi e1 sigma' pi' e1' -> one_step sigma pi (Eif e1 e2 e3) sigma' pi' (Eif e1' e2 e3) | one_step_if_true: forall sigma pi:env, e:term, e1 e2:expr. one_step sigma pi (Eif (Evalue (Vbool True)) e1 e2) sigma pi e1 | one_step_if_false: forall sigma pi:env, e:term, e1 e2:expr. one_step sigma pi (Eif (Evalue (Vbool False)) e1 e2) sigma pi e2 | one_step_assert: forall sigma pi:env, f:fmla. eval_fmla sigma pi f -> one_step sigma pi (Eassert f) sigma pi void | one_step_while: forall sigma pi:env, e:expr, inv:fmla, e':expr. one_step sigma pi (Ewhile e inv e') sigma pi (Eif e (Eseq e' (Ewhile e inv e')) void) (*** lemma progress: forall s:state, i:expr. i <> Sskip -> exists s':state, i':expr. one_step s i s' i' *) (** many steps of execution *) inductive many_steps env env expr env env expr int = | many_steps_refl: forall sigma pi:env, i:expr. many_steps sigma pi i sigma pi i 0