(** {1 A certified WP calculus} *) (** {2 A simple imperative language with expressions, syntax and semantics} *) theory ImpExpr use import int.Int use import int.MinMax use import bool.Bool use export list.List use export list.Append use map.Map as IdMap (** types and values *) type datatype = TYunit | TYint | TYbool type value = Vvoid | Vint int | Vbool bool (** terms and formulas *) type operator = Oplus | Ominus | Omult | Ole (** ident for mutable variables *) type mident axiom mident_decide : forall m1 m2: mident. m1 = m2 \/ m1 <> m2 (** ident for immutable variables *) type ident = {| ident_index : int |} constant result : ident axiom ident_decide : forall m1 m2: ident. m1 = m2 \/ m1 <> m2 (** Terms *) type term = | Tvalue value | Tvar ident | Tderef mident | Tbin term operator term predicate var_occurs_in_term (x:ident) (t:term) = match t with | Tvalue _ -> false | Tvar i -> x=i | Tderef _ -> false | Tbin t1 _ t2 -> var_occurs_in_term x t1 \/ var_occurs_in_term x t2 end (* predicate term_inv (t:term) = *) (* forall x:ident. var_occurs_in_term x t -> x.ident_index <= t.term_maxvar *) function mk_tvalue (v:value) : term = Tvalue v function mk_tvar (i:ident) : term = Tvar i function mk_tderef (r:mident) : term = Tderef r function mk_tbin (t1:term) (o:operator) (t2:term) : term = Tbin t1 o t2 (** Formulas *) type fmla = | Fterm term | Fand fmla fmla | Fnot fmla | Fimplies fmla fmla | Flet ident term fmla (* let id = term in fmla *) | Fforall ident datatype fmla (* forall id : ty, fmla *) (** Expressions *) type expr = | Evalue value | Ebin expr operator expr | Evar ident | Ederef mident | Eassign mident expr | Eseq expr expr | Elet ident expr expr | Eif expr expr expr | Eassert fmla | Ewhile expr fmla expr (* while cond invariant inv body *) function mk_evalue (v:value) : expr = Evalue v function mk_evar (i:ident) : expr = Evar i function mk_ederef (r:mident) : expr = Ederef r function mk_ebin (e1:expr) (o:operator) (e2:expr) : expr = Ebin e1 o e2 (* lemma decide_is_skip: *) (* forall s:stmt. s = Sskip \/ s <> Sskip *) (** Typing *) function type_value (v:value) : datatype = match v with | Vvoid -> TYunit | Vint int -> TYint | Vbool bool -> TYbool end inductive type_operator (op:operator) (ty1 ty2 ty: datatype) = | Type_plus : type_operator Oplus TYint TYint TYint | Type_minus : type_operator Ominus TYint TYint TYint | Type_mult : type_operator Omult TYint TYint TYint | Type_le : type_operator Ole TYint TYint TYbool type type_stack = list (ident, datatype) (* map local immutable variables to their type *) function get_vartype (i:ident) (pi:type_stack) : datatype = match pi with | Nil -> TYunit | Cons (x,ty) r -> if x=i then ty else get_vartype i r end type type_env = IdMap.map mident datatype (* map global mutable variables to their type *) function get_reftype (i:mident) (e:type_env) : datatype = IdMap.get e i inductive type_term type_env type_stack term datatype = | Type_value : forall sigma: type_env, pi:type_stack, v:value. type_term sigma pi (Tvalue v) (type_value v) | Type_var : forall sigma: type_env, pi:type_stack, v: ident, ty:datatype. (get_vartype v pi = ty) -> type_term sigma pi (Tvar v) ty | Type_deref : forall sigma: type_env, pi:type_stack, v: mident, ty:datatype. (get_reftype v sigma = ty) -> type_term sigma pi (Tderef v) ty | Type_bin : forall sigma: type_env, pi:type_stack, t1 t2 : term, op:operator, ty1 ty2 ty:datatype. type_term sigma pi t1 ty1 -> type_term sigma pi t2 ty2 -> type_operator op ty1 ty2 ty -> type_term sigma pi (Tbin t1 op t2) ty inductive type_fmla type_env type_stack fmla = | Type_term : forall sigma: type_env, pi:type_stack, t:term. type_term sigma pi t TYbool -> type_fmla sigma pi (Fterm t) | Type_conj : forall sigma: type_env, pi:type_stack, f1 f2:fmla. type_fmla sigma pi f1 -> type_fmla sigma pi f2 -> type_fmla sigma pi (Fand f1 f2) | Type_neg : forall sigma: type_env, pi:type_stack, f:fmla. type_fmla sigma pi f -> type_fmla sigma pi (Fnot f) | Type_implies : forall sigma: type_env, pi:type_stack, f1 f2:fmla. type_fmla sigma pi f1 -> type_fmla sigma pi f2 -> type_fmla sigma pi (Fimplies f1 f2) | Type_let : forall sigma: type_env, pi:type_stack, x:ident, t:term, f:fmla, ty:datatype. type_term sigma pi t ty -> type_fmla sigma (Cons (x,ty) pi) f -> type_fmla sigma pi (Flet x t f) | Type_forall1 : forall sigma: type_env, pi:type_stack, x:ident, f:fmla. type_fmla sigma (Cons (x,TYint) pi) f -> type_fmla sigma pi (Fforall x TYint f) | Type_forall2 : forall sigma: type_env, pi:type_stack, x:ident, f:fmla. type_fmla sigma (Cons (x,TYbool) pi) f -> type_fmla sigma pi (Fforall x TYbool f) | Type_forall3: forall sigma: type_env, pi:type_stack, x:ident, f:fmla. type_fmla sigma (Cons (x,TYunit) pi) f -> type_fmla sigma pi (Fforall x TYunit f) inductive type_expr type_env type_stack expr datatype = | Type_Evalue : forall sigma: type_env, pi:type_stack, v:value. type_expr sigma pi (Evalue v) (type_value v) | Type_Evar : forall sigma: type_env, pi:type_stack, v: ident, ty:datatype. (get_vartype v pi = ty) -> type_expr sigma pi (Evar v) ty | Type_Ederef : forall sigma: type_env, pi:type_stack, v: mident, ty:datatype. (get_reftype v sigma = ty) -> type_expr sigma pi (Ederef v) ty | Type_Ebinop : forall sigma: type_env, pi:type_stack, e1 e2 : expr, op:operator, ty1 ty2 ty:datatype. type_expr sigma pi e1 ty1 -> type_expr sigma pi e2 ty2 -> type_operator op ty1 ty2 ty -> type_expr sigma pi (Ebin e1 op e2) ty | Type_seq : forall sigma: type_env, pi:type_stack, e1 e2:expr, \$alt-ergo ty:datatype. type_expr sigma pi e1 TYunit -> type_expr sigma pi e2 ty -> type_expr sigma pi (Eseq e1 e2) ty | Type_assigns : forall sigma: type_env, pi:type_stack, x:mident, e:expr, ty:datatype. (get_reftype x sigma = ty) -> type_expr sigma pi e ty -> type_expr sigma pi (Eassign x e) TYunit | Type_if : forall sigma: type_env, pi:type_stack, t e1 e2:expr, ty:datatype. type_expr sigma pi t TYbool -> type_expr sigma pi e1 ty -> type_expr sigma pi e2 ty -> type_expr sigma pi (Eif t e1 e2) ty | Type_assert : forall sigma: type_env, pi:type_stack, p:fmla. type_fmla sigma pi p -> type_expr sigma pi (Eassert p) TYbool | Type_while : forall sigma: type_env, pi:type_stack, guard:expr, body:expr, inv:fmla, ty:datatype. type_fmla sigma pi inv -> type_expr sigma pi guard TYbool -> type_expr sigma pi body ty -> type_expr sigma pi (Ewhile guard inv body) ty | Type_Elet : forall sigma: type_env, pi:type_stack, x:ident, e1 e2:expr, ty1 ty2 :datatype. type_expr sigma pi e1 ty1 -> type_expr sigma (Cons (x,ty1) pi) e2 ty2 -> type_expr sigma pi (Elet x e1 e2) ty2 (** Operational semantic *) type env = IdMap.map mident value (* map global mutable variables to their value *) function get_env (i:mident) (e:env) : value = IdMap.get e i type stack = list (ident, value) (* map local immutable variables to their value *) function get_stack (i:ident) (pi:stack) : value = match pi with | Nil -> Vvoid | Cons (x,v) r -> if x=i then v else get_stack i r end lemma get_stack_eq: forall x:ident, v:value, r:stack. get_stack x (Cons (x,v) r) = v lemma get_stack_neq: forall x i:ident, v:value, r:stack. x <> i -> get_stack i (Cons (x,v) r) = get_stack i r (** 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 | _,_ -> Vvoid end function eval_term (sigma:env) (pi:stack) (t:term) : value = match t with | Tvalue v -> v | Tvar id -> get_stack 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 lemma eval_bool_term: forall sigma:env, pi:stack, sigmat:type_env, pit:type_stack, t:term. type_term sigmat pit t TYbool -> (* TODO: compatibility sigma, sigmat and pi,pit *) exists b:bool. eval_term sigma pi t = Vbool b predicate eval_fmla (sigma:env) (pi:stack) (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 (Cons (x,eval_term sigma pi t) pi) 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 end (** substitution of a reference [r] by a logic variable [v] warning: proper behavior only guaranted if [v] is "fresh", i.e index(v) > term_maxvar(t) *) function msubst_term (t:term) (r:mident) (v:ident) : term = match t with | Tvalue _ | Tvar _ -> t | Tderef x -> if r = x then mk_tvar v else t | Tbin t1 op t2 -> mk_tbin (msubst_term t1 r v) op (msubst_term t2 r v) end function subst_term (t:term) (r:ident) (v:ident) : term = match t with | Tvalue _ | Tderef _ -> t | Tvar x -> if r = x then mk_tvar v else t | Tbin t1 op t2 -> mk_tbin (subst_term t1 r v) op (subst_term t2 r v) end (** [fresh_in_term id t] is true when [id] does not occur in [t] *) predicate fresh_in_term (id:ident) (t:term) = not (var_occurs_in_term id t) lemma fresh_in_binop: forall t t':term, op:operator, v:ident. fresh_in_term v (mk_tbin t op t') -> fresh_in_term v t /\ fresh_in_term v t' (* lemma eval_subst_term: *) (* forall sigma:env, pi:stack, e:term, x:ident, v:ident. *) (* fresh_in_term v e -> *) (* eval_term sigma pi (subst_term e x v) = *) (* eval_term sigma (Cons (x, (get_stack v pi)) pi) e *) 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 function msubst (f:fmla) (x:mident) (v:ident) : fmla = match f with | Fterm e -> Fterm (msubst_term e x v) | Fand f1 f2 -> Fand (msubst f1 x v) (msubst f2 x v) | Fnot f -> Fnot (msubst f x v) | Fimplies f1 f2 -> Fimplies (msubst f1 x v) (msubst f2 x v) | Flet y t f -> Flet y (msubst_term t x v) (msubst f x v) | Fforall y ty f -> Fforall y ty (msubst f x v) end lemma subst_fresh_term : forall t:term, x:ident, v:ident. fresh_in_term x t -> subst_term t x v = t lemma subst_fresh : forall f:fmla, x:ident, v:ident. fresh_in_fmla x f -> subst f x v = f (* Not needed *) (* lemma let_subst: *) (* forall t:term, f:fmla, x id':ident, id :mident. *) (* msubst (Flet x t f) id id' = Flet x (msubst_term t id id') (msubst f id id') *) lemma eval_msubst_term: forall e:term, sigma:env, pi:stack, x:mident, v:ident. fresh_in_term v e -> eval_term sigma pi (msubst_term e x v) = eval_term (IdMap.set sigma x (get_stack v pi)) pi e (* Need it for monotonicity and wp_reduction *) lemma eval_msubst: forall f:fmla, sigma:env, pi:stack, x:mident, v:ident. fresh_in_fmla v f -> (eval_fmla sigma pi (msubst f x v) <-> eval_fmla (IdMap.set sigma x (get_stack v pi)) pi f) (* lemma eval_subst: *) (* forall f:fmla, sigma:env, pi:stack, x:ident, v:ident. *) (* fresh_in_fmla v f -> *) (* (eval_fmla sigma pi (subst f x v) <-> *) (* eval_fmla sigma (Cons(x, (get_stack v pi)) pi) f) *) lemma eval_swap_term: forall t:term, sigma:env, pi l:stack, id1 id2:ident, v1 v2:value. id1 <> id2 -> (eval_term sigma (l++(Cons (id1,v1) (Cons (id2,v2) pi))) t = eval_term sigma (l++(Cons (id2,v2) (Cons (id1,v1) pi))) t) lemma eval_swap_term_2: forall t:term, sigma:env, pi:stack, id1 id2:ident, v1 v2:value. id1 <> id2 -> (eval_term sigma (Cons (id1,v1) (Cons (id2,v2) pi)) t = eval_term sigma (Cons (id2,v2) (Cons (id1,v1) pi)) t) lemma eval_swap: forall f:fmla, sigma:env, pi l:stack, id1 id2:ident, v1 v2:value. id1 <> id2 -> (eval_fmla sigma (l++(Cons (id1,v1) (Cons (id2,v2) pi))) f <-> eval_fmla sigma (l++(Cons (id2,v2) (Cons (id1,v1) pi))) f) lemma eval_swap_2: forall f:fmla, id1 id2:ident, v1 v2:value. id1 <> id2 -> forall sigma:env, pi:stack. (eval_fmla sigma (Cons (id1,v1) (Cons (id2,v2) pi)) f <-> eval_fmla sigma (Cons (id2,v2) (Cons (id1,v1) pi)) f) lemma eval_term_change_free : forall t:term, sigma:env, pi:stack, id:ident, v:value. fresh_in_term id t -> eval_term sigma (Cons (id,v) pi) t = eval_term sigma pi t (* Need it for monotonicity*) lemma eval_change_free : forall f:fmla, id:ident, v:value. fresh_in_fmla id f -> forall sigma:env, pi:stack. (eval_fmla sigma (Cons (id,v) pi) f <-> eval_fmla sigma pi f) (** [valid_fmla f] is true when [f] is valid in any environment *) predicate valid_fmla (p:fmla) = forall sigma:env, pi:stack. eval_fmla sigma pi p (* Not needed *) (* axiom msubst_implies : *) (* forall p q:fmla. *) (* valid_fmla (Fimplies p q) -> *) (* forall sigma:env, pi:stack, x:mident, id:ident. *) (* fresh_in_fmla id (Fand p q) -> *) (* eval_fmla sigma (Cons (id, (get_env x sigma)) pi) (Fimplies (msubst p x id) (msubst q x id)) *) (** let id' = t in f[id <- id'] <=> let id = t in f*) (* Not needed *) (* lemma let_equiv : *) (* forall id:ident, id':ident, t:term, f:fmla. *) (* forall sigma:env, pi:stack. *) (* fresh_in_fmla id' f -> *) (* eval_fmla sigma pi (Flet id' t (subst f id id')) *) (* -> eval_fmla sigma pi (Flet id t f) *) (* lemma let_implies : *) (* forall id:ident, t:term, p q:fmla. *) (* valid_fmla (Fimplies p q) -> *) (* valid_fmla (Fimplies (Flet id t p) (Flet id t q)) *) predicate fresh_in_expr (id:ident) (e:expr) = match e with | Evalue _ -> true | Ebin e1 op e2 -> fresh_in_expr id e1 /\ fresh_in_expr id e2 | Evar v -> id <> v | Ederef _ -> true | Eassign x e -> fresh_in_expr id e | Eseq e1 e2 -> fresh_in_expr id e1 /\ fresh_in_expr id e2 | Elet v e1 e2 -> id <> v /\ fresh_in_expr id e1 /\ fresh_in_expr id e2 | Eif e1 e2 e3 -> fresh_in_expr id e1 /\ fresh_in_expr id e2 /\ fresh_in_expr id e3 | Eassert f -> fresh_in_fmla id f | Ewhile cond inv body -> fresh_in_expr id cond /\ fresh_in_fmla id inv /\ fresh_in_expr id body end constant void : expr = Evalue Vvoid (** small-steps semantics for expressions *) inductive one_step env stack expr env stack expr = | one_step_var: forall sigma:env, pi:stack, v:ident. one_step sigma pi (Evar v) sigma pi (Evalue (get_stack v pi)) | one_step_deref: forall sigma:env, pi:stack, v:mident. one_step sigma pi (Ederef v) sigma pi (Evalue (get_env v sigma)) | one_step_bin_ctxt1: forall sigma sigma':env, pi pi':stack, op:operator, e1 e1' e2:expr. one_step sigma pi e1 sigma' pi' e1' -> one_step sigma pi (Ebin e1 op e2) sigma' pi' (Ebin e1' op e2) | one_step_bin_ctxt2: forall sigma sigma':env, pi pi':stack, op:operator, v1:value, e2 e2':expr. one_step sigma pi e2 sigma' pi' e2' -> one_step sigma pi (Ebin (Evalue v1) op e2) sigma' pi' (Ebin (Evalue v1) op e2') | one_step_bin_value: forall sigma sigma':env, pi pi':stack, op:operator, v1 v2:value. one_step sigma pi (Ebin (Evalue v1) op (Evalue v2)) sigma' pi' (Evalue (eval_bin v1 op v2)) | one_step_assign_ctxt: forall sigma sigma':env, pi pi':stack, x:mident, 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 sigma':env, pi:stack, x:mident, v:value. sigma' = IdMap.set sigma x v -> one_step sigma pi (Eassign x (Evalue v)) sigma' pi void | one_step_seq_ctxt: forall sigma sigma':env, pi pi':stack, 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:env, pi:stack, e:expr. one_step sigma pi (Eseq void e) sigma pi e | one_step_let_ctxt: forall sigma sigma':env, pi pi':stack, 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:env, pi:stack, id:ident, v:value, e:expr. one_step sigma pi (Elet id (Evalue v) e) sigma (Cons (id,v) pi) e | one_step_if_ctxt: forall sigma sigma':env, pi pi':stack, 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:env, pi:stack, e1 e2:expr. one_step sigma pi (Eif (Evalue (Vbool True)) e1 e2) sigma pi e1 | one_step_if_false: forall sigma:env, pi:stack, e1 e2 :expr. one_step sigma pi (Eif (Evalue (Vbool False)) e1 e2) sigma pi e2 | one_step_assert: forall sigma:env, pi:stack, f:fmla. (* blocking semantics *) eval_fmla sigma pi f -> one_step sigma pi (Eassert f) sigma pi void | one_step_while_true: forall sigma:env, pi:stack, cond body:expr, inv:fmla. (* blocking semantics *) eval_fmla sigma pi inv -> one_step sigma pi (Ewhile (Evalue (Vbool True)) inv body) sigma pi (Eseq body (Ewhile cond inv body)) | one_step_while_false: forall sigma:env, pi:stack, inv:fmla, body:expr. (* blocking semantics *) eval_fmla sigma pi inv -> one_step sigma pi (Ewhile (Evalue (Vbool False)) inv body) sigma pi void (** many steps of execution *) inductive many_steps env stack expr env stack expr int = | many_steps_refl: forall sigma:env, pi:stack, s:expr. many_steps sigma pi s sigma pi s 0 | many_steps_trans: forall sigma1 sigma2 sigma3:env, pi1 pi2 pi3:stack, s1 s2 s3:expr, n:int. one_step sigma1 pi1 s1 sigma2 pi2 s2 -> many_steps sigma2 pi2 s2 sigma3 pi3 s3 n -> many_steps sigma1 pi1 s1 sigma3 pi3 s3 (n+1) lemma steps_non_neg: forall sigma1 sigma2:env, pi1 pi2:stack, s1 s2:expr, n:int. many_steps sigma1 pi1 s1 sigma2 pi2 s2 n -> n >= 0 (* Used by Hoare_logic/seq_rule*) lemma many_steps_seq: forall sigma1 sigma3:env, pi1 pi3:stack, e1 e2:expr, n:int. many_steps sigma1 pi1 (Eseq e1 e2) sigma3 pi3 void n -> exists sigma2:env, pi2:stack, n1 n2:int. many_steps sigma1 pi1 e1 sigma2 pi2 void n1 /\ many_steps sigma2 pi2 e2 sigma3 pi3 void n2 /\ n = 1 + n1 + n2 (* lemma one_step_change_free : *) (* forall s s':stmt, sigma sigma':env, pi pi':stack, id:ident, v:value. *) (* fresh_in_stmt id s -> *) (* one_step sigma (Cons (id,v) pi) s sigma' pi' s' -> *) (* one_step sigma pi s sigma' pi' s' *) (** {3 Hoare triples} *) (** partial correctness *) predicate valid_triple (p:fmla) (e:expr) (q:fmla) = forall sigma:env, pi:stack. eval_fmla sigma pi p -> forall sigma':env, pi':stack, n:int. many_steps sigma pi e sigma' pi' void n -> eval_fmla sigma' pi' q (*** total correctness *) predicate total_valid_triple (p:fmla) (e:expr) (q:fmla) = forall sigma:env, pi:stack. eval_fmla sigma pi p -> exists sigma':env, pi':stack, n:int. many_steps sigma pi e sigma' pi' void n /\ eval_fmla sigma' pi' q end theory TestSemantics use import ImpExpr function my_sigma : env = IdMap.const (Vint 0) constant x : ident constant y : mident function my_pi : stack = Cons (x, Vint 42) Nil goal Test13 : eval_term my_sigma my_pi (mk_tvalue (Vint 13)) = Vint 13 goal Test13expr : many_steps my_sigma my_pi (Evalue (Vint 13)) my_sigma my_pi (Evalue (Vint 13)) 0 goal Test42 : eval_term my_sigma my_pi (Tvar x) = Vint 42 goal Test42expr : many_steps my_sigma my_pi (Evar x) my_sigma my_pi (Evalue (Vint 42)) 1 goal Test0 : eval_term my_sigma my_pi (Tderef y) = Vint 0 goal Test0expr : many_steps my_sigma my_pi (Ederef y) my_sigma my_pi (Evalue (Vint 0)) 1 goal Test55 : eval_term my_sigma my_pi (Tbin (Tvar x) Oplus (Tvalue (Vint 13))) = Vint 55 goal Test55expr : many_steps my_sigma my_pi (Ebin (Evar x) Oplus (Evalue (Vint 13))) my_sigma my_pi (Evalue (Vint 55)) 2 goal Ass42 : forall sigma':env, pi':stack. one_step my_sigma my_pi (Eassign y (Evalue (Vint 42))) sigma' pi' void -> IdMap.get sigma' y = Vint 42 goal If42 : forall sigma1 sigma2:env, pi1 pi2:stack, e:expr. one_step my_sigma my_pi (Eif (Ebin (Ederef y) Ole (Evalue (Vint 10))) (Eassign y (Evalue (Vint 13))) (Eassign y (Evalue (Vint 42)))) sigma1 pi1 e -> one_step sigma1 pi1 e sigma2 pi2 void -> IdMap.get sigma2 y = Vint 13 end (** {2 Hoare logic} *) theory HoareLogic use import ImpExpr (** Hoare logic rules (partial correctness) *) lemma consequence_rule: forall p p' q q':fmla, s:expr. valid_fmla (Fimplies p' p) -> valid_triple p s q -> valid_fmla (Fimplies q q') -> valid_triple p' s q' lemma skip_rule: forall q:fmla. valid_triple q void q (* lemma assign_rule: *) (* forall p:fmla, x:mident, id:ident, t:term. *) (* fresh_in_fmla id p -> *) (* valid_triple (Flet id t (msubst p x id)) (Eassign x t) p *) lemma seq_rule: forall p q r:fmla, e1 e2:expr. valid_triple p e1 r /\ valid_triple r e2 q -> valid_triple p (Eseq e1 e2) q (* lemma if_rule: *) (* forall t:term, p q:fmla, e1 e2:expr. *) (* valid_triple (Fand p (Fterm t)) e1 q /\ *) (* valid_triple (Fand p (Fnot (Fterm t))) e2 q -> *) (* valid_triple p (Eif t e1 e2) q *) lemma assert_rule: forall f p:fmla. valid_fmla (Fimplies p f) -> valid_triple p (Eassert f) p lemma assert_rule_ext: forall f p:fmla. valid_triple (Fimplies f p) (Eassert f) p (* lemma while_rule: forall e:term, inv:fmla, i:expr. valid_triple (Fand (Fterm e) inv) i inv -> valid_triple inv (Swhile e inv i) (Fand (Fnot (Fterm e)) inv) lemma while_rule_ext: forall e:term, inv inv':fmla, i:expr. valid_fmla (Fimplies inv' inv) -> valid_triple (Fand (Fterm e) inv') i inv' -> valid_triple inv' (Swhile e inv i) (Fand (Fnot (Fterm e)) inv') *) end (** {2 WP calculus} *) theory WP use import ImpExpr use import bool.Bool use set.Set (** [assigns sigma W sigma'] is true when the only differences between [sigma] and [sigma'] are the value of references in [W] *) predicate assigns (sigma:env) (a:Set.set mident) (sigma':env) = forall i:mident. not (Set.mem i a) -> IdMap.get sigma i = IdMap.get sigma' i lemma assigns_refl: forall sigma:env, a:Set.set mident. assigns sigma a sigma lemma assigns_trans: forall sigma1 sigma2 sigma3:env, a:Set.set mident. assigns sigma1 a sigma2 /\ assigns sigma2 a sigma3 -> assigns sigma1 a sigma3 lemma assigns_union_left: forall sigma sigma':env, s1 s2:Set.set mident. assigns sigma s1 sigma' -> assigns sigma (Set.union s1 s2) sigma' lemma assigns_union_right: forall sigma sigma':env, s1 s2:Set.set mident. 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] *) predicate expr_writes (s:expr) (w:Set.set mident) = match s with | Evalue _ | Evar _ | Ederef _ | Eassert _ -> true | Eassign id _ -> Set.mem id w | Eseq e1 e2 -> expr_writes e1 w /\ expr_writes e2 w | Eif e1 e2 e3 -> expr_writes e1 w /\ expr_writes e2 w /\ expr_writes e3 w | Ewhile cond _ body -> expr_writes cond w /\ expr_writes body w | Ebin e1 o e2 -> expr_writes e1 w /\ expr_writes e2 w | Elet id e1 e2 -> expr_writes e1 w /\ expr_writes e2 w end function fresh_from (f:fmla) (s:expr) : ident (* Need it for monotonicity*) axiom fresh_from_fmla: forall s:expr, f:fmla. fresh_in_fmla (fresh_from f s) f axiom fresh_from_expr: forall s:expr, f:fmla. fresh_in_expr (fresh_from f s) s function abstract_effects (s:expr) (f:fmla) : fmla axiom abstract_effects_generalize : forall sigma:env, pi:stack, s:expr, f:fmla. eval_fmla sigma pi (abstract_effects s f) -> eval_fmla sigma pi f axiom abstract_effects_monotonic : forall s:expr, f:fmla. forall sigma:env, pi:stack. eval_fmla sigma pi f -> forall sigma:env, pi:stack. eval_fmla sigma pi (abstract_effects s f) function wp (e:expr) (q:fmla) : fmla = match e with | Evalue v -> Flet result (Tvalue v) q | Evar v -> Flet result (Tvar v) q | Ederef v -> Flet result (Tderef v) q | Eassert f -> (* asymmetric and *) Fand f (Fimplies f q) | Eseq e1 e2 -> wp e1 (wp e2 q) | Elet id e1 e2 -> wp e1 (Flet id (Tvar result) (wp e2 q)) | Ebin e1 op e2 -> let t1 = fresh_from q e in let t2 = fresh_from (Fand (Fterm (Tvar t1)) q) e in let q' = Flet result (Tbin (Tvar t1) op (Tvar t2)) q in let f = wp e2 (Flet t2 (Tvar result) q') in wp e1 (Flet t1 (Tvar result) f) (* let wp_op = subst q (Tvar result) (Tbin (Tvar t1) op (Tvar t2)) in *) (* let wp2 = (subst (wp e2 wp_op) t2 (Tvar result)) in *) (* (subst (wp e1 wp2) t1 (Tvar result)) *) | Eassign x e -> let id = fresh_from q e in let q' = Flet result (Tvalue Vvoid) q in wp e (Flet id (Tvar result) (msubst q' x id)) | Eif e1 e2 e3 -> let f = Fand (Fimplies (Fterm (Tvar result)) (wp e2 q)) (Fimplies (Fnot (Fterm (Tvar result))) (wp e3 q)) in wp e1 f | Ewhile cond inv body -> Fand inv (abstract_effects body (wp cond (Fand (Fimplies (Fand (Fterm (Tvar result)) inv) (wp body inv)) (Fimplies (Fand (Fnot (Fterm (Tvar result))) inv) q)))) end axiom abstract_effects_writes : forall sigma:env, pi:stack, s:expr, 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 -> *) (* subst (wp e q) id id' = wp e (subst q id id') *) lemma monotonicity: forall s:expr, p q:fmla. valid_fmla (Fimplies p q) -> valid_fmla (Fimplies (wp s p) (wp s q) ) lemma distrib_conj: forall s:expr, sigma:env, pi:stack, p q:fmla. (eval_fmla sigma pi (wp s p)) /\ (eval_fmla sigma pi (wp s q)) -> eval_fmla sigma pi (wp s (Fand p q)) lemma wp_reduction: forall sigma sigma':env, pi pi':stack, s s':expr. 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) predicate is_value (e:expr) = match e with | Evalue _ -> true | _ -> false end lemma decide_value : forall e:expr. not (is_value e) \/ exists v:value. e = Evalue v lemma bool_value: forall v:value, sigmat: type_env, pit:type_stack. type_expr sigmat pit (Evalue v) TYbool -> (v = Vbool False) \/ (v = Vbool True) lemma unit_value: forall v:value, sigmat: type_env, pit:type_stack. type_expr sigmat pit (Evalue v) TYunit -> v = Vvoid lemma progress: forall e:expr, sigma:env, pi:stack, sigmat: type_env, pit: type_stack, ty: datatype, q:fmla. type_expr sigmat pit e ty -> type_fmla sigmat (Cons(result, ty) pit) q -> not is_value e -> eval_fmla sigma pi (wp e q) -> exists sigma':env, pi':stack, e':expr. one_step sigma pi e sigma' pi' e' end (*** Local Variables: compile-command: "why3ide blocking_semantics4.mlw" End: *)