Quelle Name.thy Sprache: Isabelle

(*  Title:      HOL/Bali/Name.thy
    Author:     David von Oheimb
*)
subsection \<open>Java names\<close>

theory Name imports Basis begin

(* cf. 6.5 *)
typedecl tnam   \<comment> \<open>ordinary type name, i.e. class or interface name\<close>
typedecl pname  \<comment> \<open>package name\<close>
typedecl mname  \<comment> \<open>method name\<close>
typedecl vname  \<comment> \<open>variable or field name\<close>
typedecl label  \<comment> \<open>label as destination of break or continue\<close>

datatype ename        \<comment> \<open>expression name\<close>
        = VNam vname
        | Res         \<comment> \<open>special name to model the return value of methods\<close>

datatype lname        \<comment> \<open>names for local variables and the This pointer\<close>
        = EName ename
        | This
abbreviation VName   :: "vname \ lname"
      where "VName n == EName (VNam n)"

abbreviation Result :: lname
      where "Result == EName Res"

datatype xname          \<comment> \<open>names of standard exceptions\<close>
        = Throwable
        | NullPointer | OutOfMemory | ClassCast
        | NegArrSize  | IndOutBound | ArrStore

lemma xn_cases:
  "xn = Throwable \ xn = NullPointer \
         xn = OutOfMemory \<or> xn = ClassCast \<or>
         xn = NegArrSize  \<or> xn = IndOutBound \<or> xn = ArrStore"
apply (induct xn)
apply auto
done

datatype tname  \<comment> \<open>type names for standard classes and other type names\<close>
        = Object'
        | SXcpt' xname
        | TName   tnam

record   qtname = \<comment> \<open>qualified tname cf. 6.5.3, 6.5.4\<close>
          pid :: pname
          tid :: tname

class has_pname =
  fixes pname :: "'a \ pname"

instantiation pname :: has_pname
begin

definition
  pname_pname_def: "pname (p::pname) \ p"

instance ..

end

class has_tname =
  fixes tname :: "'a \ tname"

instantiation tname :: has_tname
begin

definition
  tname_tname_def: "tname (t::tname) = t"

instance ..

end

definition
  qtname_qtname_def: "qtname (q::'a qtname_scheme) = q"

translations
  (type) "qtname" <= (type) "\pid::pname,tid::tname\"
  (type) "'a qtname_scheme" <= (type) "\pid::pname,tid::tname,\::'a\"

axiomatization java_lang::pname \<comment> \<open>package java.lang\<close>

definition
  Object :: qtname
  where "Object = \pid = java_lang, tid = Object'\"

definition SXcpt :: "xname \ qtname"
  where "SXcpt = (\x. \pid = java_lang, tid = SXcpt' x\)"

lemma Object_neq_SXcpt [simp]: "Object \ SXcpt xn"
by (simp add: Object_def SXcpt_def)

lemma SXcpt_inject [simp]: "(SXcpt xn = SXcpt xm) = (xn = xm)"
by (simp add: SXcpt_def)

end

quality97%

¤ Dauer der Verarbeitung: 0.19 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.