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.14 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.