products/Sources/formale Sprachen/Isabelle/HOL/MicroJava/J/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: root.bib   Sprache: Isabelle

Original von: 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


¤ Dauer der Verarbeitung: 0.0 Sekunden  (vorverarbeitet)  ¤



Kontakt
Drucken
Kontakt
sprechenden Kalenders

Eigene Datei ansehen




schauen Sie vor die Tür

Fenster


Die Firma ist wie angegeben erreichbar.

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff