Commit 11614db7 by MARCHE Claude

### WP with blocking semantics

parent 1d644bdc
 (** {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 (* let id = term in fmla *) | Fforall ident datatype fmla (* forall id : ty, fmla *) use map.Map as IdMap type env = IdMap.map ident value (* map global mutable variables to their value *) function get_env (i:ident) (e:env) : value = IdMap.get e i use export list.List 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 (** 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 (** [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 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: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 (IdMap.set sigma x (get_stack v pi)) pi e 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 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:env, pi:stack, x:ident, v:ident. fresh_in_fmla v f -> (eval_fmla sigma pi (subst f x v) <-> eval_fmla (IdMap.set sigma x (get_stack v pi)) 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_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) (* 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 (* while cond invariant inv body *) constant void : expr = Evalue Vvoid (** small-steps semantics for expressions *) inductive one_step env stack expr env stack expr = | one_step_assign_ctxt: forall sigma sigma':env, pi pi':stack, 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:env, pi:stack, 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 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, id:ident, 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, 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:env, pi:stack, e:term, 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, e:term, 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: forall sigma:env, pi:stack, cond:expr, inv:fmla, body:expr. (* blocking semantics *) eval_fmla sigma pi inv -> one_step sigma pi (Ewhile cond inv body) sigma pi (Eif cond (Eseq body (Ewhile cond inv body)) void) (** many steps of execution *) inductive many_steps env stack expr env stack expr int = | many_steps_refl: forall sigma:env, pi:stack, e:expr. many_steps sigma pi e sigma pi e 0 | many_steps_trans: forall sigma1 sigma2 sigma3:env, pi1 pi2 pi3:stack, e1 e2 e3:expr, n:int. one_step sigma1 pi1 e1 sigma2 pi2 e2 -> many_steps sigma2 pi2 e2 sigma3 pi3 e3 n -> many_steps sigma1 pi1 e1 sigma3 pi3 e3 (n+1) lemma steps_non_neg: forall sigma1 sigma2:env, pi1 pi2:stack, e1 e2:expr, n:int. many_steps sigma1 pi1 e1 sigma2 pi2 e2 n -> n >= 0 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 many_steps_let: forall sigma1 sigma3:env, pi1 pi3:stack, id:ident, e1 e2:expr, v2:value, n:int. many_steps sigma1 pi1 (Elet id e1 e2) sigma3 pi3 (Evalue v2) n -> exists sigma2:env, pi2:stack, v1:value, n1 n2:int. many_steps sigma1 pi1 e1 sigma2 pi2 (Evalue v1) n1 /\ many_steps sigma2 (Cons (id,v1) pi2) e2 sigma3 pi3 (Evalue v2) n2 /\ n = 1 + n1 + n2 (** [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 (** {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, v:value, n:int. many_steps sigma pi e sigma' pi' (Evalue v) n -> eval_fmla sigma' (Cons (result,v) 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, v:value, n:int. many_steps sigma pi e sigma' pi' (Evalue v) n /\ eval_fmla sigma' (Cons (result,v) pi') q end theory TestSemantics use import ImpExpr function my_sigma : env = IdMap.const (Vint 0) function my_pi : stack = Cons (0, Vint 42) Nil goal Test13 : eval_term my_sigma my_pi (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 0) = Vint 42 goal Test42expr : many_steps my_sigma my_pi (Evar 0) my_sigma my_pi (Evalue (Vint 42)) 1 goal Test0 : eval_term my_sigma my_pi (Tderef 0) = Vint 0 goal Test0expr : many_steps my_sigma my_pi (Ederef 0) my_sigma my_pi (Evalue (Vint 0)) 1 goal Test55 : eval_term my_sigma my_pi (Tbin (Tvar 0) Oplus (Tvalue (Vint 13))) = Vint 55 goal Test55expr : many_steps my_sigma my_pi (Ebin (Evar 0) Oplus (Evalue (Vint 13))) my_sigma my_pi (Evalue (Vint 55)) 2 goal Ass42 : let x = 0 in forall sigma':env, pi':stack. one_step my_sigma my_pi (Eassign x (Evalue (Vint 42))) sigma' pi' void -> IdMap.get sigma' x = Vint 42 goal If42 : let x = 0 in forall sigma1 sigma2:env, pi1 pi2:stack, e:expr. one_step my_sigma my_pi (Eif (Ebin (Ederef x) Ole (Evalue (Vint 10))) (Eassign x (Evalue (Vint 13))) (Eassign x (Evalue (Vint 42)))) sigma1 pi1 e -> one_step sigma1 pi1 e sigma2 pi2 void -> IdMap.get sigma2 x = 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, e:expr. valid_fmla (Fimplies p' p) -> valid_triple p e q -> valid_fmla (Fimplies q q') -> valid_triple p' e q' lemma value_rule: forall q:fmla, v:value. fresh_in_fmla result q -> valid_triple q (Evalue v) q lemma assign_rule: forall p q:fmla, x:ident, e:expr. valid_triple p e (subst q x result) -> valid_triple p (Eassign x e) q 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 let_rule: forall p q r:fmla, id:ident, e1 e2:expr. id <> result -> fresh_in_fmla id r -> valid_triple p e1 r /\ valid_triple (Flet result (Tvar id) r) e2 q -> valid_triple p (Elet id e1 e2) q (* lemma if_rule: forall e:expr, p q:fmla, i1 i2:expr. valid_triple (Fand p (Fterm e)) i1 q /\ valid_triple (Fand p (Fnot (Fterm e))) i2 q -> valid_triple p (Eif e 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') *) (*** frame rule ? *) end (** {2 WP calculus} *) theory WP use import ImpExpr 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 ident) (sigma':env) = forall i:ident. not (Set.mem i a) -> IdMap.get sigma i = IdMap.get sigma' i lemma assigns_refl: forall sigma:env, a:Set.set ident. assigns sigma a sigma lemma assigns_trans: forall sigma1 sigma2 sigma3:env, a:Set.set ident. assigns sigma1 a sigma2 /\ assigns sigma2 a sigma3 -> assigns sigma1 a sigma3 lemma assigns_union_left: forall sigma sigma':env, s1 s2:Set.set ident. assigns sigma s1 sigma' -> assigns sigma (Set.union s1 s2) sigma' 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] *) predicate expr_writes (e:expr) (w:Set.set ident) = match e with | Evalue _ | Evar _ | Ederef _ | Eassert _ -> true | Ebin e1 _ e2 -> expr_writes e1 w /\ expr_writes e2 w | Eassign id _ -> Set.mem id w | Eseq e1 e2 -> expr_writes e1 w /\ expr_writes e2 w | Elet id 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 end function fresh_from_fmla (f:fmla) : ident function abstract_effects (e:expr) (f:fmla) : fmla function wp (e:expr) (q:fmla) : fmla = match e with | Evalue v -> (* let result = v in q *) Flet result (Tvalue v) q | Evar v -> Flet result (Tvar v) q | Ederef x -> Flet result (Tderef x) 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_fmla q in let t2 = fresh_from_fmla (Fand (Fterm (Tvar t1)) q) 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) | Eassign x e -> let id = fresh_from_fmla q in let q' = Flet result (Tvalue Vvoid) q in wp e (Flet id (Tvar result) (subst 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 lemma wp_conj: forall sigma:env, pi:stack, e:expr, p q:fmla. eval_fmla sigma pi (wp e (Fand p q)) <-> (eval_fmla sigma pi (wp e p)) /\ (eval_fmla sigma pi (wp e q)) lemma wp_reduction: forall sigma sigma':env, pi pi':stack, e e':expr, q:fmla. one_step sigma pi e sigma' pi' e' /\ eval_fmla sigma pi (wp e q) -> eval_fmla sigma' pi' (wp e' q) predicate not_a_value (e:expr) = match e with | Evalue _ -> false | _ -> true end lemma progress: forall sigma:env, pi:stack, e:expr, q:fmla. eval_fmla sigma pi (wp e q) /\ not_a_value e -> exists sigma':env, pi':stack, e':expr. one_step sigma pi e sigma' pi' e' (* let rec compute_writes (s:expr) : Set.set ident = { } match s with | Sskip -> Set.empty | Sassign i _ -> Set.singleton i | Sseq s1 s2 -> Set.union (compute_writes s1) (compute_writes s2) | Sif _ s1 s2 -> Set.union (compute_writes s1) (compute_writes s2) | Swhile _ _ s -> compute_writes s | Sassert _ -> Set.empty end { forall sigma sigma':env, pi pi':stack, n:int. many_steps sigma pi s sigma' pi' Sskip n -> assigns sigma result sigma' } val fresh_from_fmla (q:fmla) : { } ident { fresh_in_fmla result q } val abstract_effects (i:expr) (f:fmla) : { } fmla { forall sigma:env, pi:stack. eval_fmla sigma pi result -> eval_fmla sigma pi f /\ (*** forall sigma':env, w:Set.set ident. expr_writes i w /\ assigns sigma w sigma' -> eval_fmla sigma' pi result *) forall sigma' pi':env, n:int. many_steps sigma pi i sigma' pi' Sskip n -> eval_fmla sigma' pi' result } use HoareLogic let rec wp (i:expr) (q:fmla) = { true } match i with | Sskip -> q | Sseq i1 i2 -> wp i1 (wp i2 q) | Sassign x e -> let id = fresh_from_fmla q in Flet id e (subst q x id) | Sif e i1 i2 -> Fand (Fimplies (Fterm e) (wp i1 q)) (Fimplies (Fnot (Fterm e)) (wp i2 q)) | Sassert f -> Fimplies f q (* liberal wp, no termination required *) (* Fand f q *) (* strict wp, termination required *) | Swhile e inv i -> Fand inv (abstract_effects i (Fand (Fimplies (Fand (Fterm e) inv) (wp i inv)) (Fimplies (Fand (Fnot (Fterm e)) inv) q))) end { valid_triple result i q } *) end (*** Local Variables: compile-command: "why3ide wp4.mlw" End: *)
 (* This file is generated by Why3's Coq driver *) (* Beware! Only edit allowed sections below *) Require Import ZArith. Require Import Rbase. Require int.Int. (* Why3 assumption *) Definition implb(x:bool) (y:bool): bool := match (x, y) with | (true, false) => false | (_, _) => true end. (* Why3 assumption *) Inductive datatype := | TYunit : datatype | TYint : datatype | TYbool : datatype . (* Why3 assumption *) Inductive value := | Vvoid : value | Vint : Z -> value | Vbool : bool -> value . (* Why3 assumption *) Inductive operator := | Oplus : operator | Ominus : operator | Omult : operator | Ole : operator . (* Why3 assumption *) Definition ident := Z. (* Why3 assumption *) Inductive term := | Tvalue : value -> term | Tvar : Z -> term | Tderef : Z -> term | Tbin : term -> operator -> term -> term .