src/HOL/MicroJava/J/Type.thy
author haftmann
Tue Nov 24 14:37:23 2009 +0100 (2009-11-24)
changeset 33954 1bc3b688548c
parent 16417 9bc16273c2d4
child 35102 cc7a0b9f938c
permissions -rwxr-xr-x
backported parts of abstract byte code verifier from AFP/Jinja
     1 (*  Title:      HOL/MicroJava/J/Type.thy
     2     ID:         $Id$
     3     Author:     David von Oheimb
     4     Copyright   1999 Technische Universitaet Muenchen
     5 *)
     6 
     7 header {* \isaheader{Java types} *}
     8 
     9 theory Type imports JBasis begin
    10 
    11 typedecl cnam 
    12 
    13  -- "exceptions"
    14 datatype 
    15   xcpt   
    16   = NullPointer
    17   | ClassCast
    18   | OutOfMemory
    19 
    20 -- "class names"
    21 datatype cname  
    22   = Object 
    23   | Xcpt xcpt 
    24   | Cname cnam 
    25 
    26 typedecl vnam   -- "variable or field name"
    27 typedecl mname  -- "method name"
    28 
    29 -- "names for @{text This} pointer and local/field variables"
    30 datatype vname 
    31   = This
    32   | VName vnam
    33 
    34 -- "primitive type, cf. 4.2"
    35 datatype prim_ty 
    36   = Void          -- "'result type' of void methods"
    37   | Boolean
    38   | Integer
    39 
    40 -- "reference type, cf. 4.3"
    41 datatype ref_ty   
    42   = NullT         -- "null type, cf. 4.1"
    43   | ClassT cname  -- "class type"
    44 
    45 -- "any type, cf. 4.1"
    46 datatype ty 
    47   = PrimT prim_ty -- "primitive type"
    48   | RefT  ref_ty  -- "reference type"
    49 
    50 syntax
    51   NT    :: "ty"
    52   Class :: "cname  => ty"
    53 
    54 translations
    55   "NT"      == "RefT NullT"
    56   "Class C" == "RefT (ClassT C)"
    57 
    58 end