Quelle Hoare.thy Sprache: Isabelle

(* 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"
  (\<open>_[_'/_]\<close> [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

quality97%

¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.