(* Author: Tobias Nipkow *)
section "Hoare Logic"
subsection "Hoare Logic for Partial Correctness"
theory Hoare imports Big_Step begin
type_synonym assn = "state \ bool"
definition
hoare_valid :: "assn \ com \ assn \ bool" ("\ {(1_)}/ (_)/ {(1_)}" 50) where
"\ {P}c{Q} = (\s t. P s \ (c,s) \ t \ Q t)"
abbreviation state_subst :: "state \ aexp \ vname \ state"
("_[_'/_]" [1000,0,0] 999)
where "s[a/x] == s(x := aval a s)"
inductive
hoare :: "assn \ com \ assn \ bool" ("\ ({(1_)}/ (_)/ {(1_)})" 50)
where
Skip: "\ {P} SKIP {P}" |
Assign: "\ {\s. P(s[a/x])} x::=a {P}" |
Seq: "\ \ {P} c\<^sub>1 {Q}; \ {Q} c\<^sub>2 {R} \
\<Longrightarrow> \<turnstile> {P} c\<^sub>1;;c\<^sub>2 {R}" |
If: "\ \ {\s. P s \ bval b s} c\<^sub>1 {Q}; \ {\s. P s \ \ bval b s} c\<^sub>2 {Q} \
\<Longrightarrow> \<turnstile> {P} IF b THEN c\<^sub>1 ELSE c\<^sub>2 {Q}" |
While: "\ {\s. P s \ bval b s} c {P} \
\<turnstile> {P} WHILE b DO c {\<lambda>s. P s \<and> \<not> bval b s}" |
conseq: "\ \s. P' s \ P s; \ {P} c {Q}; \s. Q s \ Q' s \
\<Longrightarrow> \<turnstile> {P'} c {Q'}"
lemmas [simp] = hoare.Skip hoare.Assign hoare.Seq If
lemmas [intro!] = hoare.Skip hoare.Assign hoare.Seq hoare.If
lemma strengthen_pre:
"\ \s. P' s \ P s; \ {P} c {Q} \ \ \ {P'} c {Q}"
by (blast intro: conseq)
lemma weaken_post:
"\ \ {P} c {Q}; \s. Q s \ Q' s \ \ \ {P} c {Q'}"
by (blast intro: conseq)
text\<open>The assignment and While rule are awkward to use in actual proofs
because their pre and postcondition are of a very special form and the actual
goal would have to match this form exactly. Therefore we derive two variants
with arbitrary pre and postconditions.\<close>
lemma Assign': "\s. P s \ Q(s[a/x]) \ \ {P} x ::= a {Q}"
by (simp add: strengthen_pre[OF _ Assign])
lemma While':
assumes "\ {\s. P s \ bval b s} c {P}" and "\s. P s \ \ bval b s \ Q s"
shows "\ {P} WHILE b DO c {Q}"
by(rule weaken_post[OF While[OF assms(1)] assms(2)])
end
¤ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
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.
|
