primrec assertions :: "'a ann_com \ ('a assn) set" where "assertions (AnnBasic r f) = {r}"
| "assertions (AnnSeq c1 c2) = assertions c1 \ assertions c2"
| "assertions (AnnCond1 r b c1 c2) = {r} \ assertions c1 \ assertions c2"
| "assertions (AnnCond2 r b c) = {r} \ assertions c"
| "assertions (AnnWhile r b i c) = {r, i} \ assertions c"
| "assertions (AnnAwait r b c) = {r}"
primrec atomics :: "'a ann_com \ ('a assn \ 'a com) set" where "atomics (AnnBasic r f) = {(r, Basic f)}"
| "atomics (AnnSeq c1 c2) = atomics c1 \ atomics c2"
| "atomics (AnnCond1 r b c1 c2) = atomics c1 \ atomics c2"
| "atomics (AnnCond2 r b c) = atomics c"
| "atomics (AnnWhile r b i c) = atomics c"
| "atomics (AnnAwait r b c) = {(r \ b, c)}"
primrec com :: "'a ann_triple_op \ 'a ann_com_op" where "com (c, q) = c"
primrecpost :: "'a ann_triple_op \ 'a assn" where "post (c, q) = q"
definition interfree_aux :: "('a ann_com_op \ 'a assn \ 'a ann_com_op) \ bool" where "interfree_aux \ \(co, q, co'). co'= None \
(\<forall>(r,a) \<in> atomics (the co'). \<parallel>= (q \<inter> r) a q \<and>
(co = None \<or> (\<forall>p \<in> assertions (the co). \<parallel>= (p \<inter> r) a p)))"
definition interfree :: "(('a ann_triple_op) list) \ bool" where "interfree Ts \ \i j. i < length Ts \ j < length Ts \ i \ j \
interfree_aux (com (Ts!i), post (Ts!i), com (Ts!j)) "
inductive
oghoare :: "'a assn \ 'a com \ 'a assn \ bool" (\(3\- _//_//_)\ [90,55,90] 50) and ann_hoare :: "'a ann_com \ 'a assn \ bool" (\(2\ _// _)\ [60,90] 45) where
AnnBasic: "r \ {s. f s \ q} \ \ (AnnBasic r f) q"
| AnnCond1: "\ r \ b \ pre c1; \ c1 q; r \ -b \ pre c2; \ c2 q\ \<Longrightarrow> \<turnstile> (AnnCond1 r b c1 c2) q"
| AnnCond2: "\ r \ b \ pre c; \ c q; r \ -b \ q \ \ \ (AnnCond2 r b c) q"
| AnnWhile: "\ r \ i; i \ b \ pre c; \ c i; i \ -b \ q \ \<Longrightarrow> \<turnstile> (AnnWhile r b i c) q"
| AnnAwait: "\ atom_com c; \- (r \ b) c q \ \ \ (AnnAwait r b c) q"
| Seq: "\ \- p c1 r; \- r c2 q \ \ \- p (Seq c1 c2) q "
| Cond: "\ \- (p \ b) c1 q; \- (p \ -b) c2 q \ \ \- p (Cond b c1 c2) q"
| While: "\ \- (p \ b) c p \ \ \- p (While b i c) (p \ -b)"
| Conseq: "\ p' \ p; \- p c q ; q \ q' \ \ \- p' c q'"
section \<open>Soundness\<close> (* In the version Isabelle-10-Sep-1999: HOL: The THEN and ELSE parts of conditional expressions (if P then x else y) are no longer simplified. (This allows the simplifier to unfold recursive functional programs.) To restore the old behaviour, we declare
@{text "lemmas [cong del] = if_weak_cong"}. *)
subsection \<open>Soundness of the System for Component Programs\<close>
inductive_cases ann_transition_cases: "(None,s) -1\ (c', s')" "(Some (AnnBasic r f),s) -1\ (c', s')" "(Some (AnnSeq c1 c2), s) -1\ (c', s')" "(Some (AnnCond1 r b c1 c2), s) -1\ (c', s')" "(Some (AnnCond2 r b c), s) -1\ (c', s')" "(Some (AnnWhile r b I c), s) -1\ (c', s')" "(Some (AnnAwait r b c),s) -1\ (c', s')"
text\<open>Strong Soundness for Component Programs:\<close>
lemma ann_hoare_case_analysis [rule_format]: "\ C q' \
((\<forall>r f. C = AnnBasic r f \<longrightarrow> (\<exists>q. r \<subseteq> {s. f s \<in> q} \<and> q \<subseteq> q')) \<and>
(\<forall>c0 c1. C = AnnSeq c0 c1 \<longrightarrow> (\<exists>q. q \<subseteq> q' \<and> \<turnstile> c0 pre c1 \<and> \<turnstile> c1 q)) \<and>
(\<forall>r b c1 c2. C = AnnCond1 r b c1 c2 \<longrightarrow> (\<exists>q. q \<subseteq> q' \<and>
r \<inter> b \<subseteq> pre c1 \<and> \<turnstile> c1 q \<and> r \<inter> -b \<subseteq> pre c2 \<and> \<turnstile> c2 q)) \<and>
(\<forall>r b c. C = AnnCond2 r b c \<longrightarrow>
(\<exists>q. q \<subseteq> q' \<and> r \<inter> b \<subseteq> pre c \<and> \<turnstile> c q \<and> r \<inter> -b \<subseteq> q)) \<and>
(\<forall>r i b c. C = AnnWhile r b i c \<longrightarrow>
(\<exists>q. q \<subseteq> q' \<and> r \<subseteq> i \<and> i \<inter> b \<subseteq> pre c \<and> \<turnstile> c i \<and> i \<inter> -b \<subseteq> q)) \<and>
(\<forall>r b c. C = AnnAwait r b c \<longrightarrow> (\<exists>q. q \<subseteq> q' \<and> \<parallel>- (r \<inter> b) c q)))" apply(rule ann_hoare_induct) apply simp_all apply(rule_tac x=q in exI,simp)+ apply(rule conjI,clarify,simp,clarify,rule_tac x=qa in exI,fast)+ apply(clarify,simp,clarify,rule_tac x=qa in exI,fast) done
lemmaHelp: "(transition \ {(x,y). True}) = (transition)" apply force done
lemma Strong_Soundness_aux: "\ (Some c, s) -*\ (co, t); s \ pre c; \ c q \ \<Longrightarrow> if co = None then t \<in> q else t \<in> pre (the co) \<and> \<turnstile> (the co) q" apply(erule rtrancl_induct2) apply simp apply(case_tac "a") apply(fast elim: ann_transition_cases) apply(erule Strong_Soundness_aux_aux) apply simp apply simp_all done
lemma Strong_Soundness: "\ (Some c, s)-*\(co, t); s \ pre c; \ c q \ \<Longrightarrow> if co = None then t\<in>q else t \<in> pre (the co)" apply(force dest:Strong_Soundness_aux) done
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 ist noch experimentell.
