Theory Type

Up to index of Isabelle/HOL/jsr

(*  Title:      HOL/MicroJava/J/Type.thy
    ID:         $Id: Type.html,v 1.1 2002/11/28 14:17:20 kleing Exp $
    Author:     David von Oheimb
    Copyright   1999 Technische Universitaet Muenchen
*)

header {* \isaheader{Java types} *}

theory Type = JBasis:

typedecl cnam 

 -- "exceptions"
datatype 
  xcpt   
  = NullPointer
  | ClassCast
  | OutOfMemory

-- "class names"
datatype cname  
  = Object 
  | Xcpt xcpt 
  | Cname cnam 

typedecl vnam   -- "variable or field name"
typedecl mname  -- "method name"

-- "names for @{text This} pointer and local/field variables"
datatype vname 
  = This
  | VName vnam

-- "primitive type, cf. 4.2"
datatype prim_ty 
  = Void          -- "'result type' of void methods"
  | Boolean
  | Integer
  | RetA nat      -- "bytecode return addresses"

-- "reference type, cf. 4.3"
datatype ref_ty   
  = NullT         -- "null type, cf. 4.1"
  | ClassT cname  -- "class type"

-- "any type, cf. 4.1"
datatype ty 
  = PrimT prim_ty -- "primitive type"
  | RefT  ref_ty  -- "reference type"

syntax
  NT    :: "ty"
  Class :: "cname  => ty"
  RA    :: "nat => ty"

translations
  "NT"      == "RefT NullT"
  "Class C" == "RefT (ClassT C)"
  "RA pc"   == "PrimT (RetA pc)"



text {* 
For object initialization in the JVM, we tag each location with the
current init status. The tags use an extended type system for object
initialization.
 
We have either  
\begin{itemize}
\item usual initialized types, or
\item a class that is not yet initialized and has been created
      by a @{text New} instruction at a certain line number, or 
\item a partly initialized class (on which the next super class 
      constructor has to be called). We store the name of the class
      the superclass constructor has to be called of.
\end{itemize}
*}  
datatype init_ty = Init ty | UnInit cname nat | PartInit cname


end