I agree Our site saves small pieces of text information (cookies) on your device in order to deliver better content and for statistical purposes. You can disable the usage of cookies by changing the settings of your browser. By browsing our website without changing the browser settings you grant us permission to store that information on your device.
theory Defs
imports "HOL-IMP.Small_Step" "HOL-IMP.Star" "HOL-IMP.Hoare"
begin
declare [[names_short]]
type_synonym ('n,'l) flowgraph = "'n \<Rightarrow> 'l \<Rightarrow> 'n \<Rightarrow> bool"
datatype label = Assign vname aexp | Cond bexp | Skip
consts step :: "('n\<times>'s) \<Rightarrow> ('n\<times>'s) \<Rightarrow> bool"
consts enabled :: "label \<Rightarrow> state \<Rightarrow> bool"
consts effect :: "label \<Rightarrow> state \<Rightarrow> state"
consts cfg :: "com \<Rightarrow> label \<Rightarrow> com \<Rightarrow> bool"
end
theory Submission
imports Defs
begin
type_synonym ('n,'l) flowgraph = "'n \<Rightarrow> 'l \<Rightarrow> 'n \<Rightarrow> bool"
locale flowgraph =
fixes G :: "('n,'l) flowgraph"
fixes enabled :: "'l \<Rightarrow> 's \<Rightarrow> bool"
fixes effect :: "'l \<Rightarrow> 's \<Rightarrow> 's"
begin
inductive step :: "('n\<times>'s) \<Rightarrow> ('n\<times>'s) \<Rightarrow> bool"
abbreviation "steps \<equiv> star step"
context
fixes I :: "'n \<Rightarrow> ('s \<Rightarrow> bool)"
assumes preserve: "\<lbrakk> I n s; G n l n'; enabled l s \<rbrakk> \<Longrightarrow> I n' (effect l s)"
begin
lemma preserves:
assumes "steps (n,s) (n',s')"
and "I n s"
shows "I n' s'"
sorry
end
end
fun enabled :: "label \<Rightarrow> state \<Rightarrow> bool" where
"enabled _ = undefined"
fun effect :: "label \<Rightarrow> state \<Rightarrow> state" where
"effect _ = undefined"
inductive cfg :: "com \<Rightarrow> label \<Rightarrow> com \<Rightarrow> bool"
where
"cfg (x::=a) (Assign x a) SKIP"
| "cfg (IF b THEN c1 ELSE c2) (Cond (Not b)) c2"
code_pred cfg .
interpretation flowgraph cfg enabled effect .
thm preserves
lemma steps_eq: "cs \<rightarrow>* cs' \<longleftrightarrow> steps cs cs'"
sorry
lemma floyd:
assumes PRE: "\<And>s. P s \<Longrightarrow> I c s"
and PRES: "\<And>n s c l c'. \<lbrakk>cfg c l c'; I c s; enabled l s \<rbrakk> \<Longrightarrow> I c' (effect l s)"
and POST: "\<And>s. I SKIP s \<Longrightarrow> Q s"
shows "\<Turnstile> {P} c {Q}"
sorry
end
theory Check
imports Submission
begin
lemma steps_eq: "cs \<rightarrow>* cs' \<longleftrightarrow> steps cs cs'"
by (rule Submission.steps_eq)
lemma floyd: "(\<And>s. P s \<Longrightarrow> I c s) \<Longrightarrow> (\<And>n s c l c'. \<lbrakk>cfg c l c'; I c s; enabled l s \<rbrakk> \<Longrightarrow> I c' (effect l s)) \<Longrightarrow> (\<And>s. I SKIP s \<Longrightarrow> Q s) \<Longrightarrow> \<Turnstile> {P} c {Q}"
by (rule Submission.floyd)
end