Commit cb272b65 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

more on example blocking_semantics3

parent a9cb9b1e
......@@ -20,16 +20,12 @@ type value = Vvoid | Vint int | Vbool bool
type operator = Oplus | Ominus | Omult | Ole
(* TODO: introduce two distinct
types mident and ident *)
(** ident for mutable variable*)
(** ident for mutable variables *)
type mident
(** ident for imutable variable*)
(** ident for immutable variables *)
type ident = {| ident_index : int |}
constant result : ident
(** Terms *)
type term_node =
| Tvalue value
......@@ -88,18 +84,14 @@ type 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 *)
(** 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 *)
(** Typing *)
......@@ -183,52 +175,36 @@ inductive type_fmla type_env type_stack 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_ebin :
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_eseq :
forall sigma: type_env, pi:type_stack, e1 e2:expr, op:operator, ty:datatype.
type_expr sigma pi e1 TYunit ->
type_expr sigma pi e2 ty ->
type_expr sigma pi (Eseq e1 e2) ty
| Type_eassigns :
forall sigma: type_env, pi:type_stack, x:mident, e:expr, ty:datatype.
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_expr sigma pi e ty ->
type_expr sigma pi (Eassign x e) TYunit
| Type_elet :
forall sigma: type_env, pi:type_stack, x:ident, e1 e2:expr, ty1 ty2 ty:datatype.
type_expr sigma pi e1 ty1 ->
type_expr sigma (Cons (x,ty2) pi) e2 ty2 ->
type_expr sigma pi (Elet x e1 e2) ty2
| Type_eif :
forall sigma: type_env, pi:type_stack, e1 e2 e3:expr, ty:datatype.
type_expr sigma pi e1 TYbool ->
type_expr sigma pi e2 ty ->
type_expr sigma pi e3 ty ->
type_expr sigma pi (Eif e1 e2 e3) ty
| Type_eassert :
forall sigma: type_env, pi:type_stack, p:fmla, ty:datatype.
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_expr sigma pi (Eassert p) TYbool
| Type_ewhile :
forall sigma: type_env, pi:type_stack, guard body:expr, inv:fmla, ty:datatype.
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_expr sigma pi guard TYbool ->
type_expr sigma pi body TYunit ->
type_expr sigma pi (Ewhile guard inv body) TYunit
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 *)
......@@ -419,159 +395,112 @@ lemma let_implies :
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
| Eseq e1 e2
| Ebin e1 _ e2 -> fresh_in_expr id e1 /\ fresh_in_expr id e2
| Evar v -> id <> v
| Ederef _ -> true
| Eassign _ e -> fresh_in_expr id e
| 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
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
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:env, pi:stack, x:mident, 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)
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, e:term, e1 e2:expr.
one_step sigma pi (Eif (Evalue (Vbool True)) e1 e2) sigma pi e1
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, e:term, e1 e2:expr.
one_step sigma pi (Eif (Evalue (Vbool False)) e1 e2) sigma pi e2
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 (Eassert f) sigma pi void
one_step sigma pi (Sassert f) sigma pi Sskip
| one_step_while:
forall sigma:env, pi:stack, cond:expr, inv:fmla, body:expr.
| one_step_while_true:
forall sigma:env, pi:stack, cond:term, inv:fmla, body:stmt.
(* 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)
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_falsee:
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 expr env stack expr int =
inductive many_steps env stack stmt env stack stmt int =
| many_steps_refl:
forall sigma:env, pi:stack, e:expr. many_steps sigma pi e sigma pi e 0
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, 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)
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, e1 e2:expr, n:int.
many_steps sigma1 pi1 e1 sigma2 pi2 e2 n -> n >= 0
forall sigma1 sigma2:env, pi1 pi2:stack, s1 s2:stmt, n:int.
many_steps sigma1 pi1 s1 sigma2 pi2 s2 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 ->
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 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 /\
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 e e':expr, sigma sigma':env, pi pi':stack, id:ident, v:value.
fresh_in_expr id e ->
one_step sigma (Cons (id,v) pi) e sigma' pi' e' ->
one_step sigma pi e sigma' pi' e'
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) =
predicate valid_triple (p:fmla) (s:stmt) (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
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) (e:expr) (q:fmla) =
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, v:value, n:int.
many_steps sigma pi e sigma' pi' (Evalue v) n /\
eval_fmla sigma' (Cons (result,v) pi') q
exists sigma':env, pi':stack, n:int.
many_steps sigma pi s sigma' pi' Sskip n /\
eval_fmla sigma' pi' q
end
......@@ -589,40 +518,28 @@ 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 (mk_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 (mk_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 (mk_tbin (mk_tvar x) Oplus (mk_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 ->
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, e:expr.
forall sigma1 sigma2:env, pi1 pi2:stack, s:stmt.
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 ->
(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
......@@ -637,47 +554,38 @@ use import ImpExpr
(** Hoare logic rules (partial correctness) *)
lemma consequence_rule:
forall p p' q q':fmla, e:expr.
forall p p' q q':fmla, s:stmt.
valid_fmla (Fimplies p' p) ->
valid_triple p e q ->
valid_triple p s q ->
valid_fmla (Fimplies q q') ->
valid_triple p' e q'
valid_triple p' s q'
lemma value_rule:
forall q:fmla, v:value. fresh_in_fmla result q ->
valid_triple q (Evalue v) q
lemma skip_rule:
forall q:fmla. valid_triple q Sskip q
lemma assign_rule:
forall p q:fmla, x:mident, e:expr.
valid_triple p e (msubst q x result) ->
valid_triple p (Eassign x e) q
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, e1 e2:expr.
valid_triple p e1 r /\ valid_triple r e2 q ->
valid_triple p (Eseq e1 e2) q
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 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 (mk_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
*)
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 (Eassert f) p
valid_triple p (Sassert f) p
lemma assert_rule_ext:
forall f p:fmla.
valid_triple (Fimplies f p) (Eassert f) p
valid_triple (Fimplies f p) (Sassert f) p
(*
lemma while_rule:
......@@ -739,120 +647,80 @@ lemma assigns_union_right:
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 mident) =
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
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) (e:expr) : ident
function fresh_from (f:fmla) (s:stmt) : ident
axiom fresh_from_fmla: forall e:expr, f:fmla.
fresh_in_fmla (fresh_from f e) f
axiom fresh_from_fmla: forall s:stmt, f:fmla.
fresh_in_fmla (fresh_from f s) f
axiom fresh_from_expr: forall e:expr, f:fmla.
fresh_in_expr (fresh_from f e) e
axiom fresh_from_stmt: forall s:stmt, f:fmla.
fresh_in_stmt (fresh_from f s) s
function abstract_effects (e:expr) (f:fmla) : fmla
function abstract_effects (s:stmt) (f:fmla) : fmla
function wp (e:expr) (q:fmla) : fmla =
match e with
| Evalue v ->
(* let result = v in q *)
Flet result (mk_tvalue v) q
| Evar v -> Flet result (mk_tvar v) q
| Ederef x -> Flet result (mk_tderef x) q
| Eassert f ->
function wp (s:stmt) (q:fmla) : fmla =
match s with
| Sskip -> q
| Sassert f ->
(* asymmetric and *)
Fand f (Fimplies f (Flet result (mk_tvalue Vvoid) q))
| Eseq e1 e2 -> wp e1 (wp e2 q)
| Elet id e1 e2 -> wp e1 (Flet id (mk_tvar result) (wp e2 q))
| Ebin e1 op e2 ->
let t1 = fresh_from q e in
let t2 = fresh_from (Fand (Fterm (mk_tvar t1)) q) e in
let q' = Flet result (mk_tbin (mk_tvar t1) op (mk_tvar t2)) q in
let f = wp e2 (Flet t2 (mk_tvar result) q') in
wp e1 (Flet t1 (mk_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 (mk_tvalue Vvoid) q in
wp e (Flet id (mk_tvar result) (msubst q' x id))
| Eif e1 e2 e3 ->
let f =
Fand (Fimplies (Fterm (mk_tvar result)) (wp e2 q))
(Fimplies (Fnot (Fterm (mk_tvar result))) (wp e3 q))
in
wp e1 f
| Ewhile cond inv body ->
Fand f (Fimplies f q)
| Sseq s1 s2 -> wp s1 (wp s2 q)
| Sassign x t ->
let id = fresh_from q s 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
(wp cond
(Fand
(Fimplies (Fand (Fterm (mk_tvar result)) inv) (wp body inv))
(Fimplies (Fand (Fnot (Fterm (mk_tvar result))) inv) q))))
(Fand
(Fimplies (Fand (Fterm cond) inv) (wp body inv))
(Fimplies (Fand (Fnot (Fterm cond)) inv) q)))
end
lemma result_always_fresh_in_wp:
forall e:expr, q:fmla. fresh_in_fmla result (wp e q)
(* lemma wp_subst: *)
(* forall e:expr, q:fmla, id :mident, id':ident. *)
(* fresh_in_expr id e -> *)
(* fresh_in_stmt id e -> *)
(* subst (wp e q) id id' = wp e (subst q id id') *)
lemma distrib_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))
forall sigma:env, pi:stack, s:stmt, p q:fmla.
eval_fmla sigma pi (wp s (Fand p q)) <->
(eval_fmla sigma pi (wp s p)) /\
(eval_fmla sigma pi (wp s q))
lemma monotonicity:
forall e:expr, p q:fmla.
forall s:stmt, p q:fmla.
valid_fmla (Fimplies p q)
-> valid_fmla (Fimplies (wp e p) (wp e q) )
-> valid_fmla (Fimplies (wp s p) (wp s q) )
lemma wp_reduction:
forall sigma sigma':env, pi pi':stack, e e':expr.
one_step sigma pi e sigma' pi' e' ->
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 e q) ->
eval_fmla sigma' pi' (wp e' 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
eval_fmla sigma pi (wp s q) ->
eval_fmla sigma' pi' (wp s' q)
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 ->
eval_fmla sigma pi (wp e q) -> not is_value e ->
exists sigma':env, pi':stack, e':expr.
one_step sigma pi e sigma' pi' e'
forall s:stmt, sigma:env, pi:stack,
sigmat: type_env, pit: type_stack, q:fmla.
type_stmt sigmat pit s ->
type_fmla sigmat pit q ->
eval_fmla sigma pi (wp s q) ->
s <> Sskip ->
exists sigma':env, pi':stack, s':stmt.
one_step sigma pi s sigma' pi' s'
end
......