section‹Facilitating the Hoare Logic› theory Vcg importsStateSpace"HOL-Statespace.StateSpaceLocale" Generalise
keywords "procedures""hoarestate" :: thy_defn begin
method_setup hoare_rule = "Hoare.hoare_rule" "apply single hoare rule and solve certain sideconditions"
text‹Variables of the programming language are represented as components
a record. To avoid cluttering up the namespace of Isabelle with lots of
variable names, we append a unusual suffix at the end of each name by
›
definition list_multsel:: "'a list ==> nat list ==> 'a list" (infixl‹!!›100) where"xs !! ns = map (nth xs) ns"
definition list_multupd:: "'a list ==> nat list ==> 'a list ==> 'a list" where"list_multupd xs ns ys = foldl (λxs (n,v). xs[n:=v]) xs (zip ns ys)"
translations "_Do c" => "c" "b∙ c" => "CONST condCatch c b SKIP" "b∙ (_DoPre c)" <= "CONST condCatch c b SKIP" "l∙ (CONST whileAnnoG gs b I V c)" <= "l∙ (_DoPre (CONST whileAnnoG gs b I V c))" "l∙ (CONST whileAnno b I V c)" <= "l∙ (_DoPre (CONST whileAnno b I V c))" "CONST condCatch c b SKIP" <= "(_DoPre (CONST condCatch c b SKIP))" "_Do c" <= "_DoPre c" "c;; d" == "CONST Seq c d" "_guarantee g" => "(CONST True, g)" "_guaranteeStrip g" == "CONST guaranteeStripPair (CONST True) g" "_grd g" => "(CONST False, g)" "_grds g gs" => "g#gs" "_last_grd g" => "[g]" "_guards gs c" == "CONST guards gs c"
"{|s. P|}" == "{|_antiquoteCur((=) s) ∧ P |}" "{|b|}" => "CONST Collect (_quote b)" "IF b THEN c1 ELSE c2 FI" => "CONST Cond {|b|} c1 c2" "IF b THEN c1 FI" == "IF b THEN c1 ELSE SKIP FI" "IFg b THEN c1 FI" == "IFg b THEN c1 ELSE SKIP FI"
"_While_inv_var b I V c" => "CONST whileAnno {|b|} I V c" "_While_inv_var b I V (_DoPre c)" <= "CONST whileAnno {|b|} I V c" "_While_inv b I c" == "_While_inv_var b I (CONST undefined) c" "_While b c" == "_While_inv b {|CONST undefined|} c"
"_While_guard_inv_var gs b I V c" => "CONST whileAnnoG gs {|b|} I V c" (* "_While_guard_inv_var gs b I V (_DoPre c)" <= "CONST whileAnnoG gs {|b|} I V c"*) "_While_guard_inv gs b I c" == "_While_guard_inv_var gs b I (CONST undefined) c" "_While_guard gs b c" == "_While_guard_inv gs b {|CONST undefined|} c"
"_GuardedWhile_inv b I c" == "_GuardedWhile_inv_var b I (CONST undefined) c" "_GuardedWhile b c" == "_GuardedWhile_inv b {|CONST undefined|} c" (* "\<^bsup>s\<^esup>A" => "A s"*) "TRY c1 CATCH c2 END" == "CONST Catch c1 c2" "ANNO s. P c Q,A" => "CONST specAnno (λs. P) (λs. c) (λs. Q) (λs. A)" "ANNO s. P c Q" == "ANNO s. P c Q,{}"
"_WhileFix_inv_var b z I V c" => "CONST whileAnnoFix {|b|} (λz. I) (λz. V) (λz. c)" "_WhileFix_inv_var b z I V (_DoPre c)" <= "_WhileFix_inv_var {|b|} z I V c" "_WhileFix_inv b z I c" == "_WhileFix_inv_var b z I (CONST undefined) c"
"_GuardedWhileFix_inv b z I c" == "_GuardedWhileFix_inv_var b z I (CONST undefined) c"
"_GuardedWhileFix_inv_var b z I V c" => "_GuardedWhileFix_inv_var_hook {|b|} (λz. I) (λz. V) (λz. c)"
"_WhileFix_guard_inv_var gs b z I V c" => "CONST whileAnnoGFix gs {|b|} (λz. I) (λz. V) (λz. c)" "_WhileFix_guard_inv_var gs b z I V (_DoPre c)" <= "_WhileFix_guard_inv_var gs {|b|} z I V c" "_WhileFix_guard_inv gs b z I c" == "_WhileFix_guard_inv_var gs b z I (CONST undefined) c" "LEMMA x c END" == "CONST lem x c" translations "(_switchcase V c)" => "(V,c)" "(_switchcasesSingle b)" => "[b]" "(_switchcasesCons b bs)" => "CONST Cons b bs" "(_Switch v vs)" => "CONST switch (_quote v) vs"
parse_ast_translation‹
let
fun tr c asts = Ast.mk_appl (Ast.Constant c) (map Ast.strip_positions asts)
in
[(@{syntax_const "_antiquoteCur0"}, K (tr @{syntax_const "_antiquoteCur"})),
(@{syntax_const "_antiquoteOld0"}, K (tr @{syntax_const "_antiquoteOld"}))]
end ›
print_ast_translation‹
let
fun tr c asts = Ast.mk_appl (Ast.Constant c) asts
in
[(@{syntax_const "_antiquoteCur"}, K (tr @{syntax_const "_antiquoteCur0"})),
(@{syntax_const "_antiquoteOld"}, K (tr @{syntax_const "_antiquoteOld0"}))]
end ›
print_ast_translation‹
let
fun dest_abs (Ast.Appl [Ast.Constant @{syntax_const "_abs"}, x, t]) = (x, t)
| dest_abs _ = raise Match;
fun spec_tr' [P, c, Q, A] =
let
val (x',P') = dest_abs P;
val (_ ,c') = dest_abs c;
val (_ ,Q') = dest_abs Q;
val (_ ,A') = dest_abs A;
in
if (A' = Ast.Constant @{const_syntax bot})
then Ast.mk_appl (Ast.Constant @{syntax_const "_SpecNoAbrupt"}) [x', P', c', Q']
else Ast.mk_appl (Ast.Constant @{syntax_const "_Spec"}) [x', P', c', Q', A']
end;
fun whileAnnoFix_tr' [b, I, V, c] =
let
val (x',I') = dest_abs I;
val (_ ,V') = dest_abs V;
val (_ ,c') = dest_abs c;
in
Ast.mk_appl (Ast.Constant @{syntax_const "_WhileFix_inv_var"}) [b, x', I', V', c']
end;
in
[(@{const_syntax specAnno}, K spec_tr'),
(@{const_syntax whileAnnoFix}, K whileAnnoFix_tr')]
end ›
translations "s may_only_modify_globals Z in []" => "s may_not_modify_globals Z"
definitionLet':: "['a, 'a => 'b] => 'b" where"Let' = Let"
ML_file ‹hoare_syntax.ML›
parse_translation‹
let
val argsC = @{syntax_const "_modifyargs"};
val globalsN = "globals";
val ex = @{const_syntax mex};
val eq = @{const_syntax meq};
val varn = Hoare.varname;
fun extract_args (Const (argsC,_)$Free (n,_)$t) = varn n::extract_args t
| extract_args (Free (n,_)) = [varn n]
| extract_args t = raise TERM ("extract_args", [t])
fun idx [] y = error "idx: element not in list"
| idx (x::xs) y = if x=y then 0 else (idx xs y)+1
fun gen_update ctxt names (name,t) =
Hoare_Syntax.update_comp ctxt NONE [] false true name (Bound (idx names name)) t
fun gen_updates ctxt names t = Library.foldr (gen_update ctxt names) (names,t)
fun gen_ex (name,t) = Syntax.const ex $ Abs (name,dummyT,t)
fun gen_exs names t = Library.foldr gen_ex (names,t)
fun tr ctxt s Z names =
let val upds = gen_updates ctxt (rev names) (Syntax.free globalsN$Z);
val eq = Syntax.const eq $ (Syntax.free globalsN$s) $ upds;
in gen_exs names eq end;
fun may_modify_tr ctxt [s,Z,names] = tr ctxt s Z
(sort_strings (extract_args names))
fun may_not_modify_tr ctxt [s,Z] = tr ctxt s Z []
in
[(@{syntax_const "_may_modify"}, may_modify_tr),
(@{syntax_const "_may_not_modify"}, may_not_modify_tr)]
end ›
print_translation‹
let
val argsC = @{syntax_const "_modifyargs"};
val chop = Hoare.chopsfx Hoare.deco;
fun get_state ( _ $ _ $ t) = get_state t (* for record-updates*)
| get_state ( _ $ _ $ _ $ _ $ _ $ t) = get_state t (* for statespace-updates *)
| get_state (globals$(s as Const (@{syntax_const "_free"},_) $ Free _)) = s
| get_state (globals$(s as Const (@{syntax_const "_bound"},_) $ Free _)) = s
| get_state (globals$(s as Const (@{syntax_const "_var"},_) $ Var _)) = s
| get_state (globals$(s as Const _)) = s
| get_state (globals$(s as Free _)) = s
| get_state (globals$(s as Bound _)) = s
| get_state t = raise Match;
fun tr' names (Abs (n,_,t)) = tr' (n::names) t
| tr' names (Const (@{const_syntax mex},_) $ t) = tr' names t
| tr' names (Const (@{const_syntax meq},_) $ (globals$s) $ upd) = let val Z = get_state upd;
in (case names of
[] => Syntax.const @{syntax_const "_may_not_modify"} $ s $ Z
| xs => Syntax.const @{syntax_const "_may_modify"} $ s $ Z $ mk_args (rev names)) end;
fun may_modify_tr' [t] = tr' [] t fun may_not_modify_tr' [_$s,_$Z] = Syntax.const @{syntax_const "_may_not_modify"} $ s $ Z in
[(@{const_syntax mex}, K may_modify_tr'),
(@{const_syntax meq}, K may_not_modify_tr')] end ›
parse_translation‹
let
fun quote_tr ctxt [t] = Hoare_Syntax.quote_tr ctxt @{syntax_const "_antiquoteCur"} t
| quote_tr ctxt ts = raise TERM ("quote_tr", ts);
in [(@{syntax_const "_quote"}, quote_tr)] end ›
print_translation‹
let
fun spec_tr' ctxt ((coll as Const _)$
((splt as Const _) $ (t as (Abs (s,T,p))))::ts) =
let
fun selector (Const (c, T)) = Hoare.is_state_var c
| selector (Const (@{syntax_const "_free"}, _) $ (Free (c, T))) =
Hoare.is_state_var c
| selector _ = false;
in
if Hoare_Syntax.antiquote_applied_only_to selector p then
Syntax.const @{const_syntax Spec} $ coll $
(splt $ Hoare_Syntax.quote_mult_tr' ctxt selector
Hoare_Syntax.antiquoteCur Hoare_Syntax.antiquoteOld (Abs (s,T,t)))
else raise Match
end
| spec_tr' _ ts = raise Match
in [(@{const_syntax Spec}, spec_tr')] end ›
print_translation‹
let
fun selector (Const (c,T)) = Hoare.is_state_var c
| selector _ = false;
fun measure_tr' ctxt ((t as (Abs (_,_,p)))::ts) =
if Hoare_Syntax.antiquote_applied_only_to selector p
then Hoare_Syntax.app_quote_tr' ctxt (Syntax.const @{syntax_const "_Measure"}) (t::ts)
else raise Match
| measure_tr' _ _ = raise Match
fun mlex_tr' ctxt ((t as (Abs (_,_,p)))::r::ts) =
if Hoare_Syntax.antiquote_applied_only_to selector p
then Hoare_Syntax.app_quote_tr' ctxt (Syntax.const @{syntax_const "_Mlex"}) (t::r::ts)
else raise Match
| mlex_tr' _ _ = raise Match
in
[(@{const_syntax measure}, measure_tr'),
(@{const_syntax mlex_prod}, mlex_tr')]
end ›
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.
