Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Term.thy Sprache: Isabelle

Original von: Isabelle^©

(*  Title:      HOL/NanoJava/Term.thy
    Author:     David von Oheimb, Technische Universitaet Muenchen
*)

section "Statements and expression emulations"

theory Term imports Main begin

typedecl cname  \<comment> \<open>class    name\<close>
typedecl mname  \<comment> \<open>method   name\<close>
typedecl fname  \<comment> \<open>field    name\<close>
typedecl vname  \<comment> \<open>variable name\<close>

axiomatization
  This \<comment> \<open>This pointer\<close>
  Par  \<comment> \<open>method parameter\<close>
  Res  :: vname \<comment> \<open>method result\<close>
\<comment> \<open>Inequality axioms are not required for the meta theory.\<close>
(*
where
  This_neq_Par [simp]: "This \<noteq> Par"
  Par_neq_Res  [simp]: "Par \<noteq> Res"
  Res_neq_This [simp]: "Res \<noteq> This"
*)

datatype stmt
  = Skip                   \<comment> \<open>empty statement\<close>
  | Comp       stmt stmt   ("_;; _"             [91,90   ] 90)
  | Cond expr  stmt stmt   ("If '(_') _ Else _" [ 3,91,91] 91)
  | Loop vname stmt        ("While '(_') _"     [ 3,91   ] 91)
  | LAss vname expr        ("_ :== _"           [99,   95] 94) \<comment> \<open>local assignment\<close>
  | FAss expr  fname expr  ("_.._:==_"          [95,99,95] 94) \<comment> \<open>field assignment\<close>
  | Meth "cname \ mname" \ \virtual method\
  | Impl "cname \ mname" \ \method implementation\
and expr
  = NewC cname       ("new _"        [   99] 95) \<comment> \<open>object creation\<close>
  | Cast cname expr                              \<comment> \<open>type cast\<close>
  | LAcc vname                                   \<comment> \<open>local access\<close>
  | FAcc expr  fname ("_.._"         [95,99] 95) \<comment> \<open>field access\<close>
  | Call cname expr mname expr
                     ("{_}_.._'(_')" [99,95,99,95] 95) \<comment> \<open>method call\<close>

end

¤ Dauer der Verarbeitung: 0.6 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.