(* 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 assn" "'a var" "'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 x y c) None None"
| "s \ b \ Sem (While b x y c) (Some s) (Some s)"
| "s \ b \ Sem c (Some s) s'' \ Sem (While b x y c) s'' s' \
Sem (While b x y 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 bexp \ bool"
where "Valid p c q \ \s s'. Sem c s s' \ s \ Some ` p \ s' \ Some ` q"
definition ValidTC :: "'a bexp \ 'a com \ 'a bexp \ bool"
where "ValidTC p c q \ \s . s \ p \ (\t . Sem c (Some s) (Some t) \ t \ q)"
lemma tc_implies_pc:
"ValidTC p c q \ Valid p c q"
by (smt Sem_deterministic ValidTC_def Valid_def image_iff)
lemma tc_extract_function:
"ValidTC p c 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) q"
by (auto simp:Valid_def)
lemma BasicRule: "p \ {s. f s \ q} \ Valid p (Basic f) q"
by (auto simp:Valid_def)
lemma SeqRule: "Valid P c1 Q \ Valid Q c2 R \ Valid P (Seq c1 c2) R"
by (auto simp:Valid_def)
lemma CondRule:
"p \ {s. (s \ b \ s \ w) \ (s \ b \ s \ w')}
\<Longrightarrow> Valid w c1 q \<Longrightarrow> Valid w' c2 q \<Longrightarrow> Valid p (Cond b c1 c2) q"
by (fastforce simp:Valid_def image_def)
lemma While_aux:
assumes "Sem (While b i v 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 i v c" s s') auto
lemma WhileRule:
"p \ i \ Valid (i \ b) c i \ i \ (-b) \ q \ Valid p (While b i v c) 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 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) 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) q"
by (metis Ball_Collect Sem.intros(2) ValidTC_def assms)
lemma SeqRuleTC:
assumes "ValidTC p c1 q"
and "ValidTC q c2 r"
shows "ValidTC p (Seq c1 c2) 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 q"
and "ValidTC w' c2 q"
shows "ValidTC p (Cond b c1 c2) 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 (i \ {s . v s < n})"
and "i \ uminus b \ q"
shows "ValidTC p (While b i v c) q"
proof -
{
fix s n
have "s \ i \ v s = n \ (\t . Sem (While b i v c) (Some s) (Some t) \ t \ q)"
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 i v c) (Some s) (Some t) \ t \ q)"
show "s \ i \ v s = n \ (\t . Sem (While b i v 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 i v c) (Some t) (Some u) \ u \ q"
using 1 by auto
thus "\t . Sem (While b i v 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 i v 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" ("(2_ \/ _)" 71)
"_array_update" :: "'a list \ nat \ 'a \ 'a com" ("(2_[_] :=/ _)" [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
¤ Dauer der Verarbeitung: 0.2 Sekunden
(vorverarbeitet)
¤
|
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.
|
