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 ‹Hoare Logic with an Abort statement for modelling run time errors›

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 ==> 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 (‹SKIP›) 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 ‹The proof rules for partial correctness›

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')}
  ==> Valid w c1 a1 q ==> Valid w' c2 a2 q \ 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 ∈ Some ` I ==> s' \ Some ` (I \ -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 ‹The proof rules for total correctness›

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 ‹Concrete syntax›

setup ‹
  Hoare_Syntax.setup
   {Basic = 🍋‹Basic›,
    Skip = 🍋‹annskip›,
    Seq = 🍋‹Seq›,
    Cond = 🍋‹Cond›,
    While = 🍋‹While›,
    Valid = 🍋‹Valid›,
    ValidTC = 🍋‹ValidTC›}
›

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

text ‹
  Note: there is no special syntax for guarded array access. Thus
  you must write ‹j < length a → a[i] := a!j›.
›


subsection ‹Proof methods: VCG›

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 = ‹
  Scan.succeed (fn ctxt => SIMPLE_METHOD' (Hoare_Tac.hoare_tac ctxt (K all_tac)))\
  "verification condition generator"

method_setup vcg_simp = ‹
  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 = ‹
  Scan.succeed (fn ctxt => SIMPLE_METHOD' (Hoare_Tac.hoare_tc_tac ctxt (K all_tac)))\
  "verification condition generator"

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

end