(* Title: HOL/MicroJava/J/Exceptions.thy
Author: Gerwin Klein, Martin Strecker
Copyright 2002 Technische Universitaet Muenchen
*)
theory Exceptions imports State begin
text \<open>a new, blank object with default values in all fields:\<close>
definition blank :: "'c prog \ cname \ obj" where
"blank G C \ (C,init_vars (fields(G,C)))"
definition start_heap :: "'c prog \ aheap" where
"start_heap G \ Map.empty (XcptRef NullPointer \ blank G (Xcpt NullPointer))
(XcptRef ClassCast \<mapsto> blank G (Xcpt ClassCast))
(XcptRef OutOfMemory \<mapsto> blank G (Xcpt OutOfMemory))"
abbreviation
cname_of :: "aheap \ val \ cname"
where "cname_of hp v == fst (the (hp (the_Addr v)))"
definition preallocated :: "aheap \ bool" where
"preallocated hp \ \x. \fs. hp (XcptRef x) = Some (Xcpt x, fs)"
lemma preallocatedD:
"preallocated hp \ \fs. hp (XcptRef x) = Some (Xcpt x, fs)"
by (unfold preallocated_def) fast
lemma preallocatedE [elim?]:
"preallocated hp \ (\fs. hp (XcptRef x) = Some (Xcpt x, fs) \ P hp) \ P hp"
by (fast dest: preallocatedD)
lemma cname_of_xcp:
"raise_if b x None = Some xcp \ preallocated hp
\<Longrightarrow> cname_of (hp::aheap) xcp = Xcpt x"
proof -
assume "raise_if b x None = Some xcp"
hence "xcp = Addr (XcptRef x)"
by (simp add: raise_if_def split: if_split_asm)
moreover
assume "preallocated hp"
then obtain fs where "hp (XcptRef x) = Some (Xcpt x, fs)" ..
ultimately
show ?thesis by simp
qed
lemma preallocated_start:
"preallocated (start_heap G)"
apply (unfold preallocated_def)
apply (unfold start_heap_def)
apply (rule allI)
apply (case_tac x)
apply (auto simp add: blank_def)
done
end
¤ Dauer der Verarbeitung: 0.15 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.
|
