Specification fieldspec

[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 fieldname , 
         typefuns
   fieldspec
   = mkfs
     ( . .class : classname; comment: Selects the class from a fieldspec.;  . .type : javatype; comment: Selects the type from a fieldspec.; 
       . .field : fieldname; comment: Selects the fieldname from a fieldspec.) comment: Constructor for FieldSpec. ;
   ; comment: Represents the fields of a Java class. Consists of the classname, the type 
          of the field and the fieldname. (Paper p. 13);
   variables 
      fs, fs0, fs1 : fieldspec; 
end data specification