Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale Sprachen/Isabelle/HOL/Mutabelle/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 18 kB

SSL Name.thy Interaktion und
PortierbarkeitIsabelle

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

¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.25Angebot Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können ¤

*Eine klare Vorstellung vom Zielzustand

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.