Specification javatype

[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

data specification 
   using classname
   javatype
   = boolean_type | int_type | short_type | byte_type | long_type | float_type | double_type | char_type | 
     mkclasstype( . .class : classname) with is_classtype | mkarraytype( . .type : javatype) with is_arraytype | void_type with is_void_type | 
     abstract_type comment: used for non-Java types (abstract data types).;
   ; comment: Represents the different types in Java. 
          A value is either of one of the basictypes, a class, an array or null.;
   variables 
      ty, ty0, ty1, ty2 : javatype; 
end data specification