Commit 5a37c44b authored by MARCHE Claude's avatar MARCHE Claude

more on example blocking_semantics3

parent a7d9e86f
......@@ -93,6 +93,9 @@ type 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 =
......@@ -248,6 +251,15 @@ function eval_term (sigma:env) (pi:stack) (t:term) : value =
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
......@@ -604,16 +616,6 @@ lemma while_rule_ext:
end
theory Simpl_tautology
predicate p
predicate q
lemma simpl_tautology :
(p -> q) <-> (p /\ q <-> p)
end
(** {2 WP calculus} *)
theory WP
......@@ -716,7 +718,9 @@ predicate stmt_writes (s:stmt) (w:Set.set mident) =
forall s:stmt, sigma:env, pi:stack,
sigmat: type_env, pit: type_stack, q:fmla.
type_stmt sigmat pit s ->
(* useful ?
type_fmla sigmat pit q ->
*)
eval_fmla sigma pi (wp s q) ->
s <> Sskip ->
exists sigma':env, pi':stack, s':stmt.
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment