Mise à jour terminée. Pour connaître les apports de la version 13.8.4 par rapport à notre ancienne version vous pouvez lire les "Release Notes" suivantes :
https://about.gitlab.com/releases/2021/02/11/security-release-gitlab-13-8-4-released/
https://about.gitlab.com/releases/2021/02/05/gitlab-13-8-3-released/

Commit c8988ccd authored by MARCHE Claude's avatar MARCHE Claude

blocking semantics: ajout resultat final

parent 890d16c4
......@@ -761,18 +761,40 @@ predicate stmt_writes (s:stmt) (w:Set.set mident) =
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 ->
(* useful ?
type_fmla sigmat pit q ->
*)
eval_fmla sigma pi (wp s q) ->
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
......
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