Anforderungen  |   Konzepte  |   Entwurf  |   Entwicklung  |   Qualitätssicherung  |   Lebenszyklus  |   Steuerung
 
 
 
 

products/sources/formale Sprachen/Isabelle/Doc/Tutorial/Recdef/   (Beweissystem Isabelle Version 2025-1©)  Datei vom 16.11.2025 mit Größe 3 kB image not shown  

Quellcode-Bibliothek 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

100%


¤ 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.0.12Bemerkung:  (vorverarbeitet)  ¤

*Bot Zugriff




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.