products/sources/formale Sprachen/PVS/vectors image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: RightController.vdmrt   Sprache: Isabelle

Original von: 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

¤ Dauer der Verarbeitung: 0.22 Sekunden  (vorverarbeitet)  ¤





Druckansicht
unsichere Verbindung
Druckansicht
sprechenden Kalenders

Eigene Datei ansehen




schauen Sie vor die Tür

Fenster


Die Firma ist wie angegeben erreichbar.

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff