Quelle Exceptions.thy Sprache: Isabelle

(*  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

quality100%

¤ Dauer der Verarbeitung: 0.0 Sekunden (vorverarbeitet) ¤

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.