Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: min_lem.pvs 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.35 Sekunden (vorverarbeitet) ¤

Druckansicht unsichere Verbindung
Druckansicht sprechenden Kalenders
Eigene Datei ansehen

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.