Quelle Hoare_Logic_Abort.thy Sprache: Isabelle

(*  Title:      HOL/Hoare/Hoare_Logic_Abort.thy
    Author:     Leonor Prensa Nieto & Tobias Nipkow
    Copyright   2003 TUM
    Author:     Walter Guttmann (extension to total-correctness proofs)
*)

section \<open>Hoare Logic with an Abort statement for modelling run time errors\<close>

theory Hoare_Logic_Abort
  imports Hoare_Syntax Hoare_Tac
begin

type_synonym 'a bexp = "'a set"
type_synonym 'a assn = "'a set"
type_synonym 'a var = "'a \<Rightarrow> nat"

datatype 'a com =
  Basic "'a \ 'a"
| Abort
| Seq "'a com" "'a com"
| Cond "'a bexp" "'a com" "'a com"
| While "'a bexp" "'a com"

abbreviation annskip (\<open>SKIP\<close>) where "SKIP == Basic id"

type_synonym 'a sem = "'a option => 'a option => bool"

inductive Sem :: "'a com \ 'a sem"
where
  "Sem (Basic f) None None"
| "Sem (Basic f) (Some s) (Some (f s))"
| "Sem Abort s None"
| "Sem c1 s s'' \ Sem c2 s'' s' \ Sem (Seq c1 c2) s s'"
| "Sem (Cond b c1 c2) None None"
| "s \ b \ Sem c1 (Some s) s' \ Sem (Cond b c1 c2) (Some s) s'"
| "s \ b \ Sem c2 (Some s) s' \ Sem (Cond b c1 c2) (Some s) s'"
| "Sem (While b c) None None"
| "s \ b \ Sem (While b c) (Some s) (Some s)"
| "s \ b \ Sem c (Some s) s'' \ Sem (While b c) s'' s' \
   Sem (While b c) (Some s) s'"

inductive_cases [elim!]:
  "Sem (Basic f) s s'" "Sem (Seq c1 c2) s s'"
  "Sem (Cond b c1 c2) s s'"

lemma Sem_deterministic:
  assumes "Sem c s s1"
      and "Sem c s s2"
    shows "s1 = s2"
proof -
  have "Sem c s s1 \ (\s2. Sem c s s2 \ s1 = s2)"
    by (induct rule: Sem.induct) (subst Sem.simps, blast)+
  thus ?thesis
    using assms by simp
qed

definition Valid :: "'a bexp \ 'a com \ 'a anno \ 'a bexp \ bool"
  where "Valid p c a q \ \s s'. Sem c s s' \ s \ Some ` p \ s' \ Some ` q"

definition ValidTC :: "'a bexp \ 'a com \ 'a anno \ 'a bexp \ bool"
  where "ValidTC p c a q \ \s . s \ p \ (\t . Sem c (Some s) (Some t) \ t \ q)"

lemma tc_implies_pc:
  "ValidTC p c a q \ Valid p c a q"
  by (smt (verit) Sem_deterministic ValidTC_def Valid_def image_iff)

lemma tc_extract_function:
  "ValidTC p c a q \ \f . \s . s \ p \ f s \ q"
  by (meson ValidTC_def)

text \<open>The proof rules for partial correctness\<close>

lemma SkipRule: "p \ q \ Valid p (Basic id) a q"
by (auto simp:Valid_def)

lemma BasicRule: "p \ {s. f s \ q} \ Valid p (Basic f) a q"
by (auto simp:Valid_def)

lemma SeqRule: "Valid P c1 a1 Q \ Valid Q c2 a2 R \ Valid P (Seq c1 c2) (Aseq a1 a2) R"
by (auto simp:Valid_def)

lemma CondRule:
"p \ {s. (s \ b \ s \ w) \ (s \ b \ s \ w')}
  \<Longrightarrow> Valid w c1 a1 q \<Longrightarrow> Valid w' c2 a2 q \<Longrightarrow> Valid p (Cond b c1 c2) (Acond a1 a2) q"
by (fastforce simp:Valid_def image_def)

lemma While_aux:
  assumes "Sem (While b c) s s'"
  shows "\s s'. Sem c s s' \ s \ Some ` (I \ b) \ s' \ Some ` I \
    s \<in> Some ` I \<Longrightarrow> s' \<in> Some ` (I \<inter> -b)"
  using assms
  by (induct "While b c" s s') auto

lemma WhileRule:
"p \ i \ Valid (i \ b) c (A 0) i \ i \ (-b) \ q \ Valid p (While b c) (Awhile i v A) q"
apply (clarsimp simp:Valid_def)
apply(drule While_aux)
  apply assumption
apply blast
apply blast
done

lemma AbortRule: "p \ {s. False} \ Valid p Abort a q"
by(auto simp:Valid_def)

text \<open>The proof rules for total correctness\<close>

lemma SkipRuleTC:
  assumes "p \ q"
    shows "ValidTC p (Basic id) a q"
  by (metis Sem.intros(2) ValidTC_def assms id_def subsetD)

lemma BasicRuleTC:
  assumes "p \ {s. f s \ q}"
    shows "ValidTC p (Basic f) a q"
  by (metis Ball_Collect Sem.intros(2) ValidTC_def assms)

lemma SeqRuleTC:
  assumes "ValidTC p c1 a1 q"
      and "ValidTC q c2 a2 r"
    shows "ValidTC p (Seq c1 c2) (Aseq a1 a2) r"
  by (meson assms Sem.intros(4) ValidTC_def)

lemma CondRuleTC:
assumes "p \ {s. (s \ b \ s \ w) \ (s \ b \ s \ w')}"
     and "ValidTC w c1 a1 q"
     and "ValidTC w' c2 a2 q"
   shows "ValidTC p (Cond b c1 c2) (Acons a1 a2) q"
proof (unfold ValidTC_def, rule allI)
  fix s
  show "s \ p \ (\t . Sem (Cond b c1 c2) (Some s) (Some t) \ t \ q)"
    apply (cases "s \ b")
    apply (metis (mono_tags, lifting) Ball_Collect Sem.intros(6) ValidTC_def assms(1,2))
    by (metis (mono_tags, lifting) Ball_Collect Sem.intros(7) ValidTC_def assms(1,3))
qed

lemma WhileRuleTC:
  assumes "p \ i"
      and "\n::nat . ValidTC (i \ b \ {s . v s = n}) c (A n) (i \ {s . v s < n})"
      and "i \ uminus b \ q"
    shows "ValidTC p (While b c) (Awhile i v A) q"
proof -
  have "s \ i \ v s = n \ (\t . Sem (While b c) (Some s) (Some t) \ t \ q)" for s n
  proof (induction "n" arbitrary: s rule: less_induct)
    fix n :: nat
    fix s :: 'a
    assume 1: "\(m::nat) s::'a . m < n \ s \ i \ v s = m \ (\t . Sem (While b c) (Some s) (Some t) \ t \ q)"
    show "s \ i \ v s = n \ (\t . Sem (While b c) (Some s) (Some t) \ t \ q)"
    proof (rule impI, cases "s \ b")
      assume 2: "s \ b" and "s \ i \ v s = n"
      hence "s \ i \ b \ {s . v s = n}"
        using assms(1) by auto
      hence "\t . Sem c (Some s) (Some t) \ t \ i \ {s . v s < n}"
        by (metis assms(2) ValidTC_def)
      from this obtain t where 3: "Sem c (Some s) (Some t) \ t \ i \ {s . v s < n}"
        by auto
      hence "\u . Sem (While b c) (Some t) (Some u) \ u \ q"
        using 1 by auto
      thus "\t . Sem (While b c) (Some s) (Some t) \ t \ q"
        using 2 3 Sem.intros(10) by force
    next
      assume "s \ b" and "s \ i \ v s = n"
      thus "\t . Sem (While b c) (Some s) (Some t) \ t \ q"
        using Sem.intros(9) assms(3) by fastforce
    qed
  qed
  thus ?thesis
    using assms(1) ValidTC_def by force
qed

subsection \<open>Concrete syntax\<close>

setup \<open>
  Hoare_Syntax.setup
   {Basic = \<^const_syntax>\<open>Basic\<close>,
    Skip = \<^const_syntax>\<open>annskip\<close>,
    Seq = \<^const_syntax>\<open>Seq\<close>,
    Cond = \<^const_syntax>\<open>Cond\<close>,
    While = \<^const_syntax>\<open>While\<close>,
    Valid = \<^const_syntax>\<open>Valid\<close>,
    ValidTC = \<^const_syntax>\<open>ValidTC\<close>}
\<close>

\<comment> \<open>Special syntax for guarded statements and guarded array updates:\<close>
syntax
  "_guarded_com" :: "bool \ 'a com \ 'a com"
    (\<open>(\<open>indent=2 notation=\<open>mixfix Hoare guarded statement\<close>\<close>_ \<rightarrow>/ _)\<close> 71)
  "_array_update" :: "'a list \ nat \ 'a \ 'a com"
    (\<open>(\<open>indent=2 notation=\<open>mixfix Hoare array update\<close>\<close>_[_] :=/ _)\<close> [70, 65] 61)
translations
  "P \ c" \ "IF P THEN c ELSE CONST Abort FI"
  "a[i] := v" \<rightharpoonup> "(i < CONST length a) \<rightarrow> (a := CONST list_update a i v)"
  \<comment> \<open>reverse translation not possible because of duplicate \<open>a\<close>\<close>

text \<open>
  Note: there is no special syntax for guarded array access. Thus
  you must write \<open>j < length a \<rightarrow> a[i] := a!j\<close>.
\<close>

subsection \<open>Proof methods: VCG\<close>

declare BasicRule [Hoare_Tac.BasicRule]
  and SkipRule [Hoare_Tac.SkipRule]
  and AbortRule [Hoare_Tac.AbortRule]
  and SeqRule [Hoare_Tac.SeqRule]
  and CondRule [Hoare_Tac.CondRule]
  and WhileRule [Hoare_Tac.WhileRule]

declare BasicRuleTC [Hoare_Tac.BasicRuleTC]
  and SkipRuleTC [Hoare_Tac.SkipRuleTC]
  and SeqRuleTC [Hoare_Tac.SeqRuleTC]
  and CondRuleTC [Hoare_Tac.CondRuleTC]
  and WhileRuleTC [Hoare_Tac.WhileRuleTC]

method_setup vcg = \<open>
  Scan.succeed (fn ctxt => SIMPLE_METHOD' (Hoare_Tac.hoare_tac ctxt (K all_tac)))\
  "verification condition generator"

method_setup vcg_simp = \<open>
  Scan.succeed (fn ctxt =>
    SIMPLE_METHOD' (Hoare_Tac.hoare_tac ctxt (asm_full_simp_tac ctxt)))\
  "verification condition generator plus simplification"

method_setup vcg_tc = \<open>
  Scan.succeed (fn ctxt => SIMPLE_METHOD' (Hoare_Tac.hoare_tc_tac ctxt (K all_tac)))\
  "verification condition generator"

method_setup vcg_tc_simp = \<open>
  Scan.succeed (fn ctxt =>
    SIMPLE_METHOD' (Hoare_Tac.hoare_tc_tac ctxt (asm_full_simp_tac ctxt)))\
  "verification condition generator plus simplification"

end

quality98%

¤ Dauer der Verarbeitung: 0.7 Sekunden ¤

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.