|
(* 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
¤ Dauer der Verarbeitung: 0.16 Sekunden
(vorverarbeitet)
¤
|
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.
|
