Select Git revision
blocking_semantics3.mlw 26.25 KiB
(** {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
lemma mident_decide :
forall m1 m2: mident. m1 = m2 \/ m1 <> m2
(** ident for immutable variables *)
type ident = { ident_index : int }
lemma 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 *)
(** 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
(** 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_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, guard:term, body:stmt, inv:fmla.
type_fmla sigma pi inv ->
type_term sigma pi guard TYbool ->
type_stmt sigma pi body ->
type_stmt sigma pi (Swhile guard inv body)
(** 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
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 existe_compatible (ty:datatype) (v:value) =
match ty with
| TYbool -> exists b: bool. v = Vbool b
| TYint -> exists n: int. v = Vint n
| TYunit -> v = Vvoid
end
predicate compatible_env (sigma:env) (sigmat:type_env) (pi:stack) (pit: type_stack) =
(forall id: mident. compatible (get_reftype id sigmat) (IdMap.get sigma id)) /\
(forall id: ident. compatible (get_vartype id pit) (get_stack id pi))
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 -> existe_compatible ty (eval_term sigma pi t)
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_stmt (id:ident) (s:stmt) =
match s with
| Sskip -> true
| Sseq s1 s2 -> fresh_in_stmt id s1 /\ fresh_in_stmt id s2
| Sassign _ t -> fresh_in_term id t
| Sif t s1 s2 -> fresh_in_term id t /\ fresh_in_stmt id s1 /\ fresh_in_stmt id s2
| Sassert f -> fresh_in_fmla id f
| Swhile cond inv body -> fresh_in_term id cond /\ fresh_in_fmla id inv /\ fresh_in_stmt id body
end
(** small-steps semantics for expressions *)
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.
(* blocking semantics *)
eval_fmla sigma pi f ->
one_step sigma pi (Sassert f) sigma pi Sskip
| one_step_while_true:
forall sigma:env, pi:stack, cond:term, inv:fmla, body:stmt.
(* blocking semantics *)
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_false:
forall sigma:env, pi:stack, cond:term, inv:fmla, body:stmt.
(* blocking semantics *)
eval_fmla sigma pi inv ->
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
(* 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
(* 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' *)
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
(** {3 Hoare triples} *)
(** 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
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 Test42 :
eval_term my_sigma my_pi (mk_tvar x) = Vint 42
goal Test0 :
eval_term my_sigma my_pi (mk_tderef y) = Vint 0
goal Test55 :
eval_term my_sigma my_pi (mk_tbin (mk_tvar x) Oplus (mk_tvalue (Vint 13))) = Vint 55
goal Ass42 :
forall sigma':env, pi':stack.
one_step my_sigma my_pi (Sassign y (mk_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 (mk_tbin (mk_tderef y) Ole (mk_tvalue (Vint 10)))
(Sassign y (mk_tvalue (Vint 13)))
(Sassign y (mk_tvalue (Vint 42))))
sigma1 pi1 s ->
one_step sigma1 pi1 s sigma2 pi2 Sskip ->
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: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: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 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 stmt_writes (s:stmt) (w:Set.set mident) =
match s with
| Sskip | Sassert _ -> true
| Sassign id _ -> Set.mem id w
| Sseq s1 s2 -> stmt_writes s1 w /\ stmt_writes s2 w
| Sif t s1 s2 -> stmt_writes s1 w /\ stmt_writes s2 w
| Swhile _ _ body -> stmt_writes body w
end
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_generalize :
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
(* hypothese 4: invariance de la formule "forall w. f"
par les effets de s si w = writes s
*)
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))
(* ce lemme sert pour prouver distrib_conj, dans le cas de la sequence (et c'est tout !) *)
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
*)
(* ce lemme sert pour wp_reduction dans le cas du while (et c'est tout !) *)
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_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 ->
exists sigma':env, pi':stack, s':stmt.
one_step sigma pi s sigma' pi' s'
predicate reducible (sigma:env) (pi:stack) (s:stmt) = exists sigma':env, pi':stack, s':stmt.
one_step sigma pi s sigma' pi' s'
lemma progress2:
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 -> reducible 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 (reducible sigma' pi' s') /\
eval_fmla sigma pi (wp s q) ->
s' = Sskip /\ eval_fmla sigma' pi' q
end
(***
Local Variables:
compile-command: "why3ide blocking_semantics3.mlw"
End:
*)