Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Hoare.thy Sprache: Isabelle

Original von: 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"
  ("_[_'/_]" [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.14 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.