Stufen

Die Firma ist wie angegeben erreichbar. 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


Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/HOL/NanoJava/ (Beweissystem der NASA Version 6.0.9^©) Datei vom 16.11.2025 mit Größe 1 kB

Quelle Decl.thy Sprache: Isabelle

(*  Title:      HOL/NanoJava/Decl.thy
    Author:     David von Oheimb
    Copyright   2001 Technische Universitaet Muenchen
*)

section "Types, class Declarations, and whole programs"

theory Decl imports Term begin

datatype ty
  = NT           \<comment> \<open>null type\<close>
  | Class cname  \<comment> \<open>class type\<close>

text\<open>Field declaration\<close>
type_synonym fdecl
        = "fname \ ty"

record  methd
        = par :: ty
          res :: ty
          lcl ::"(vname \ ty) list"
          bdy :: stmt

text\<open>Method declaration\<close>
type_synonym mdecl
        = "mname \ methd"

record  "class"
        = super   :: cname
          flds    ::"fdecl list"
          methods ::"mdecl list"

text\<open>Class declaration\<close>
type_synonym cdecl
        = "cname \ class"

type_synonym prog
        = "cdecl list"

translations
  (type) "fdecl" \<leftharpoondown> (type) "fname \<times> ty"
  (type) "mdecl" \<leftharpoondown> (type) "mname \<times> ty \<times> ty \<times> stmt"
  (type) "class" \<leftharpoondown> (type) "cname \<times> fdecl list \<times> mdecl list"
  (type) "cdecl" \<leftharpoondown> (type) "cname \<times> class"
  (type) "prog " \<leftharpoondown> (type) "cdecl list"

axiomatization
  Prog    :: prog       \<comment> \<open>program as a global value\<close>
and
  Object  :: cname      \<comment> \<open>name of root class\<close>

definition "class" :: "cname \ class" where
"class \ map_of Prog"

definition is_class   :: "cname => bool" where
"is_class C \ class C \ None"

lemma finite_is_class: "finite {C. is_class C}"
apply (unfold is_class_def class_def)
apply (fold dom_def)
apply (rule finite_dom_map_of)
done

end

quality98%

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