(** {1 A certified WP calculus} *) (** {2 Formalisation d’un langage impératif jouet} *) (** {3 Syntaxe} *) theory Syntax use export bool.Bool use export int.Int (** 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 lemma mident_decide : forall m1 m2: mident. m1 = m2 \/ m1 <> m2 (** ident for immutable variables *) type ident lemma ident_decide : forall m1 m2: ident. m1 = m2 \/ m1 <> m2 (** Terms *) type term = | Tvalue value | Tvar ident | Tderef mident | Tbin term operator term (** 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 *) (** Statements *) type stmt = | Sskip | Sassign mident term | Sseq stmt stmt | Sif term stmt stmt | Sassert fmla | Swhile term fmla stmt (* while cond invariant inv body *) lemma decide_is_skip: forall s:stmt. s = Sskip \/ s <> Sskip end (** {3 Semantique Operationnelle} *) theory SemOp use export Syntax use map.Map as IdMap use export list.List (** 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 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 (** [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 (** small-steps semantics for statements *) inductive one_step env stack stmt env stack stmt = | one_step_assign : forall sigma sigma':env, pi:stack, x:mident, t:term. sigma' = IdMap.set sigma x (eval_term sigma pi t) -> one_step sigma pi (Sassign x t) sigma' pi Sskip | one_step_seq_noskip: forall sigma sigma':env, pi pi':stack, s1 s1' s2:stmt. one_step sigma pi s1 sigma' pi' s1' -> one_step sigma pi (Sseq s1 s2) sigma' pi' (Sseq s1' s2) | one_step_seq_skip: forall sigma:env, pi:stack, s:stmt. one_step sigma pi (Sseq Sskip s) sigma pi s | one_step_if_true: forall sigma:env, pi:stack, t:term, s1 s2:stmt. eval_term sigma pi t = Vbool True -> one_step sigma pi (Sif t s1 s2) sigma pi s1 | one_step_if_false: forall sigma:env, pi:stack, t:term, s1 s2:stmt. eval_term sigma pi t = Vbool False -> one_step sigma pi (Sif t s1 s2) sigma pi s2 | one_step_assert: forall sigma:env, pi:stack, f:fmla. eval_fmla sigma pi f -> (** blocking semantics *) one_step sigma pi (Sassert f) sigma pi Sskip | one_step_while_true: forall sigma:env, pi:stack, cond:term, inv:fmla, body:stmt. eval_fmla sigma pi inv /\ (** blocking semantics *) 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_false: forall sigma:env, pi:stack, cond:term, inv:fmla, body:stmt. eval_fmla sigma pi inv /\ (** blocking semantics *) eval_term sigma pi cond = Vbool False -> one_step sigma pi (Swhile cond inv body) sigma pi Sskip (** many steps of execution *) inductive many_steps env stack stmt env stack stmt int = | many_steps_refl: forall sigma:env, pi:stack, s:stmt. many_steps sigma pi s sigma pi s 0 | many_steps_trans: forall sigma1 sigma2 sigma3:env, pi1 pi2 pi3:stack, s1 s2 s3:stmt, 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:stmt, n:int. many_steps sigma1 pi1 s1 sigma2 pi2 s2 n -> n >= 0 predicate reductible (sigma:env) (pi:stack) (s:stmt) = exists sigma':env, pi':stack, s':stmt. one_step sigma pi s sigma' pi' s' end theory TestSemantics use import SemOp 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 (Tvalue (Vint 13)) = Vint 13 goal Test42 : eval_term my_sigma my_pi (Tvar x) = Vint 42 goal Test0 : eval_term my_sigma my_pi (Tderef y) = Vint 0 goal Test55 : eval_term my_sigma my_pi (Tbin (Tvar x) Oplus (Tvalue (Vint 13))) = Vint 55 goal Ass42 : forall sigma':env, pi':stack. one_step my_sigma my_pi (Sassign y (Tvalue (Vint 42))) sigma' pi' Sskip -> IdMap.get sigma' y = Vint 42 goal If42 : forall sigma1 sigma2:env, pi1 pi2:stack, s:stmt. one_step my_sigma my_pi (Sif (Tbin (Tderef y) Ole (Tvalue (Vint 10))) (Sassign y (Tvalue (Vint 13))) (Sassign y (Tvalue (Vint 42)))) sigma1 pi1 s -> one_step sigma1 pi1 s sigma2 pi2 Sskip -> IdMap.get sigma2 y = Vint 13 end (** {3 Typage} *) theory Typing use export Syntax use map.Map as IdMap use export list.List 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_forall : forall sigma: type_env, pi:type_stack, x:ident, f:fmla, ty:datatype. type_fmla sigma (Cons (x,ty) pi) f -> type_fmla sigma pi (Fforall x ty f) inductive type_stmt type_env type_stack stmt = | Type_skip : forall sigma: type_env, pi:type_stack. type_stmt sigma pi Sskip | Type_seq : forall sigma: type_env, pi:type_stack, s1 s2:stmt. type_stmt sigma pi s1 -> type_stmt sigma pi s2 -> type_stmt sigma pi (Sseq s1 s2) | Type_assigns : forall sigma: type_env, pi:type_stack, x:mident, t:term, ty:datatype. (get_reftype x sigma = ty) -> type_term sigma pi t ty -> type_stmt sigma pi (Sassign x t) | Type_if : forall sigma: type_env, pi:type_stack, t:term, s1 s2:stmt. type_term sigma pi t TYbool -> type_stmt sigma pi s1 -> type_stmt sigma pi s2 -> type_stmt sigma pi (Sif t s1 s2) | Type_assert : forall sigma: type_env, pi:type_stack, p:fmla. type_fmla sigma pi p -> type_stmt sigma pi (Sassert p) | Type_while : forall sigma: type_env, pi:type_stack, cond:term, body:stmt, inv:fmla. type_fmla sigma pi inv -> type_term sigma pi cond TYbool -> type_stmt sigma pi body -> type_stmt sigma pi (Swhile cond inv body) end (** {3 Relations entre typage et semantique operationnelle} *) theory TypingAndSemantics use import SemOp use import Typing (* inductive compatible datatype value = | Compatible_bool : forall b: bool. compatible TYbool (Vbool b) | Compatible_int : forall n: int. compatible TYint (Vint n) | Compatible_void : compatible TYunit Vvoid *) predicate compatible_env (sigma:env) (sigmat:type_env) (pi:stack) (pit: type_stack) = (forall id: mident. type_value (IdMap.get sigma id) = get_reftype id sigmat) /\ (forall id: ident. type_value (get_stack id pi) = get_vartype id pit) lemma type_inversion : forall v "induction":value. match (type_value v) with | TYbool -> exists b: bool. v = Vbool b | TYint -> exists n: int. v = Vint n | TYunit -> v = Vvoid end lemma eval_type_term: forall t:term, sigma:env, pi:stack, sigmat:type_env, pit:type_stack, ty:datatype. compatible_env sigma sigmat pi pit -> type_term sigmat pit t ty -> type_value (eval_term sigma pi t) = ty lemma type_preservation : forall s1 s2:stmt, sigma1 sigma2:env, pi1 pi2:stack, sigmat:type_env, pit:type_stack. type_stmt sigmat pit s1 /\ compatible_env sigma1 sigmat pi1 pit /\ one_step sigma1 pi1 s1 sigma2 pi2 s2 -> type_stmt sigmat pit s2 /\ compatible_env sigma2 sigmat pi2 pit end (** {2 Problématique des variables fraîches} *) theory FreshVariables use import SemOp use import list.Append lemma Cons_append: forall a: 'a, l1 l2: list 'a. Cons a (l1 ++ l2) = (Cons a l1) ++ l2 lemma Append_nil_l: forall l: list 'a. Nil ++ l = l (** substitution of a reference [x] by a logic variable [v] warning: proper behavior only guaranted if [v] is fresh *) function msubst_term (t:term) (x:mident) (v:ident) : term = match t with | Tvalue _ | Tvar _ -> t | Tderef y -> if x = y then Tvar v else t | Tbin t1 op t2 -> Tbin (msubst_term t1 x v) op (msubst_term t2 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 (** [fresh_in_term id t] is true when [id] does not occur in [t] *) predicate fresh_in_term (id:ident) (t:term) = match t with | Tvalue _ -> true | Tvar i -> id <> i | Tderef _ -> true | Tbin t1 _ t2 -> fresh_in_term id t1 /\ fresh_in_term id t2 end 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 (* Needed for monotonicity and wp_reduction *) 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 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_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_gen: 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: forall f:fmla, sigma:env, pi:stack, id1 id2:ident, v1 v2:value. id1 <> id2 -> (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, sigma:env, pi:stack, id:ident, v:value. fresh_in_fmla id f -> (eval_fmla sigma (Cons (id,v) pi) f <-> eval_fmla sigma pi f) end (** {2 Hoare logic} *) theory HoareLogic use import Syntax use import SemOp use import FreshVariables (* Used by Hoare_logic/seq_rule*) lemma many_steps_seq: forall sigma1 sigma3:env, pi1 pi3:stack, s1 s2:stmt, n:int. many_steps sigma1 pi1 (Sseq s1 s2) sigma3 pi3 Sskip n -> exists sigma2:env, pi2:stack, n1 n2:int. many_steps sigma1 pi1 s1 sigma2 pi2 Sskip n1 /\ many_steps sigma2 pi2 s2 sigma3 pi3 Sskip n2 /\ n = 1 + n1 + n2 (** partial correctness *) predicate valid_triple (p:fmla) (s:stmt) (q:fmla) = forall sigma:env, pi:stack. eval_fmla sigma pi p -> forall sigma':env, pi':stack, n:int. many_steps sigma pi s sigma' pi' Sskip n -> eval_fmla sigma' pi' q (*** total correctness *) predicate total_valid_triple (p:fmla) (s:stmt) (q:fmla) = forall sigma:env, pi:stack. eval_fmla sigma pi p -> exists sigma':env, pi':stack, n:int. many_steps sigma pi s sigma' pi' Sskip n /\ eval_fmla sigma' pi' q (** Hoare logic rules (partial correctness) *) lemma consequence_rule: forall p p' q q':fmla, s:stmt. 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 Sskip 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)) (Sassign x t) p lemma seq_rule: forall p q r:fmla, s1 s2:stmt. valid_triple p s1 r /\ valid_triple r s2 q -> valid_triple p (Sseq s1 s2) q lemma if_rule: forall t:term, p q:fmla, s1 s2:stmt. valid_triple (Fand p (Fterm t)) s1 q /\ valid_triple (Fand p (Fnot (Fterm t))) s2 q -> valid_triple p (Sif t s1 s2) q lemma assert_rule: forall f p:fmla. valid_fmla (Fimplies p f) -> valid_triple p (Sassert f) p lemma assert_rule_ext: forall f p:fmla. valid_triple (Fimplies f p) (Sassert f) p lemma while_rule: forall e:term, inv:fmla, i:stmt. 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 SemOp use import Typing use import TypingAndSemantics use import FreshVariables function fresh_from (f:fmla) : ident (* Need it for monotonicity*) axiom fresh_from_fmla: forall f:fmla. fresh_in_fmla (fresh_from f) f (* intention: abstract_effects s f = "forall w. f" avec w = writes(s) *) function abstract_effects (s:stmt) (f:fmla) : fmla (* hypothese 1: si sigma, pi |= forall w. f alors sigma, pi |= f *) axiom abstract_effects_specialize : forall sigma:env, pi:stack, s:stmt, f:fmla. eval_fmla sigma pi (abstract_effects s f) -> eval_fmla sigma pi f (* hypothese 2: si sigma, pi |= (forall w, p) /\ (forall w, q) alors sigma, pi |= forall w, (f /\ q) *) axiom abstract_effects_distrib_conj : forall s:stmt, p q:fmla, sigma:env, pi:stack. eval_fmla sigma pi (abstract_effects s p) /\ eval_fmla sigma pi (abstract_effects s q) -> eval_fmla sigma pi (abstract_effects s (Fand p q)) (* hypothese 3: si |= p -> q alors |= (forall w, p) -> (forall w, q) remarque : il est essentiel de parler de validité dans tous les etats: on n'a pas sigma,pi |= p -> q implique sigma,pi |= (forall w, p) -> (forall w, q) contre-exemple: sigma(x) = 42 alors true -> x=42 mais on n'a (forall x, true) -> (forall x, x=42) *) axiom abstract_effects_monotonic : forall s:stmt, p q:fmla. valid_fmla (Fimplies p q) -> forall sigma:env, pi:stack. eval_fmla sigma pi (abstract_effects s p) -> eval_fmla sigma pi (abstract_effects s q) function wp (s:stmt) (q:fmla) : fmla = match s with | Sskip -> q | Sassert f -> (* asymmetric and *) Fand f (Fimplies f q) | Sseq s1 s2 -> wp s1 (wp s2 q) | Sassign x t -> let id = fresh_from q in Flet id t (msubst q x id) | Sif t s1 s2 -> Fand (Fimplies (Fterm t) (wp s1 q)) (Fimplies (Fnot (Fterm t)) (wp s2 q)) | Swhile cond inv body -> Fand inv (abstract_effects body (Fand (Fimplies (Fand (Fterm cond) inv) (wp body inv)) (Fimplies (Fand (Fnot (Fterm cond)) inv) q))) 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 monotonicity: forall s:stmt, p q:fmla. valid_fmla (Fimplies p q) -> valid_fmla (Fimplies (wp s p) (wp s q) ) (* remarque l'ordre des quantifications est essentiel, on n'a pas sigma,pi |= p -> q implique sigma,pi |= (wp s p) -> (wp s q) meme contre-exemple: sigma(x) = 42 alors true -> x=42 mais wp (x := 7) true = true wp (x := 7) x=42 = 7=42 *) lemma distrib_conj: forall s:stmt, 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_preserved_by_reduction: forall sigma sigma':env, pi pi':stack, s 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) lemma progress: forall s:stmt, sigma:env, pi:stack, sigmat: type_env, pit: type_stack, q:fmla. compatible_env sigma sigmat pi pit -> type_stmt sigmat pit s -> eval_fmla sigma pi (wp s q) -> s <> Sskip -> reductible sigma pi s (** {3 main soundness result} *) lemma wp_soundness: forall n:int, sigma sigma':env, pi pi':stack, s s':stmt, sigmat: type_env, pit: type_stack, q:fmla. compatible_env sigma sigmat pi pit -> type_stmt sigmat pit s -> many_steps sigma pi s sigma' pi' s' n /\ not (reductible sigma' pi' s') /\ eval_fmla sigma pi (wp s q) -> s' = Sskip /\ eval_fmla sigma' pi' q end (*** Local Variables: compile-command: "why3ide blocking_semantics5.mlw" End: *)