Quelle Hoare_Sound_Complete.thy Sprache: Isabelle

(* Author: Tobias Nipkow *)

subsection \<open>Soundness and Completeness\<close>

theory Hoare_Sound_Complete
imports Hoare
begin

subsubsection "Soundness"

lemma hoare_sound: "\ {P}c{Q} \ \ {P}c{Q}"
proof(induction rule: hoare.induct)
  case (While P b c)
  have "(WHILE b DO c,s) \ t \ P s \ P t \ \ bval b t" for s t
  proof(induction "WHILE b DO c" s t rule: big_step_induct)
    case WhileFalse thus ?case by blast
  next
    case WhileTrue thus ?case
      using While.IH unfolding hoare_valid_def by blast
  qed
  thus ?case unfolding hoare_valid_def by blast
qed (auto simp: hoare_valid_def)

subsubsection "Weakest Precondition"

definition wp :: "com \ assn \ assn" where
"wp c Q = (\s. \t. (c,s) \ t \ Q t)"

lemma wp_SKIP[simp]: "wp SKIP Q = Q"
by (rule ext) (auto simp: wp_def)

lemma wp_Ass[simp]: "wp (x::=a) Q = (\s. Q(s[a/x]))"
by (rule ext) (auto simp: wp_def)

lemma wp_Seq[simp]: "wp (c\<^sub>1;;c\<^sub>2) Q = wp c\<^sub>1 (wp c\<^sub>2 Q)"
by (rule ext) (auto simp: wp_def)

lemma wp_If[simp]:
"wp (IF b THEN c\<^sub>1 ELSE c\<^sub>2) Q =
(\<lambda>s. if bval b s then wp c\<^sub>1 Q s else wp c\<^sub>2 Q s)"
by (rule ext) (auto simp: wp_def)

lemma wp_While_If:
"wp (WHILE b DO c) Q s =
  wp (IF b THEN c;;WHILE b DO c ELSE SKIP) Q s"
unfolding wp_def by (metis unfold_while)

lemma wp_While_True[simp]: "bval b s \
  wp (WHILE b DO c) Q s = wp (c;; WHILE b DO c) Q s"
by(simp add: wp_While_If)

lemma wp_While_False[simp]: "\ bval b s \ wp (WHILE b DO c) Q s = Q s"
by(simp add: wp_While_If)

subsubsection "Completeness"

lemma wp_is_pre: "\ {wp c Q} c {Q}"
proof(induction c arbitrary: Q)
  case If thus ?case by(auto intro: conseq)
next
  case (While b c)
  let ?w = "WHILE b DO c"
  show "\ {wp ?w Q} ?w {Q}"
  proof(rule While')
    show "\ {\s. wp ?w Q s \ bval b s} c {wp ?w Q}"
    proof(rule strengthen_pre[OF _ While.IH])
      show "\s. wp ?w Q s \ bval b s \ wp c (wp ?w Q) s" by auto
    qed
    show "\s. wp ?w Q s \ \ bval b s \ Q s" by auto
  qed
qed auto

lemma hoare_complete: assumes "\ {P}c{Q}" shows "\ {P}c{Q}"
proof(rule strengthen_pre)
  show "\s. P s \ wp c Q s" using assms
    by (auto simp: hoare_valid_def wp_def)
  show "\ {wp c Q} c {Q}" by(rule wp_is_pre)
qed

corollary hoare_sound_complete: "\ {P}c{Q} \ \ {P}c{Q}"
by (metis hoare_complete hoare_sound)

end

quality100%

¤ Dauer der Verarbeitung: 0.11 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.