JML

org.jmlspecs.checker
Class JmlTypeDeclaration

java.lang.Object
  extended byorg.multijava.util.Utils
      extended byorg.multijava.util.compiler.Phylum
          extended byorg.multijava.mjc.JPhylum
              extended byorg.jmlspecs.checker.JmlNode
                  extended byorg.jmlspecs.checker.JmlMemberDeclaration
                      extended byorg.jmlspecs.checker.JmlTypeDeclaration
All Implemented Interfaces:
Annotatable, Cloneable, Comparable, CompilerPassEnterable, Constants, Constants, Constants, JMemberDeclarationType, JTypeDeclarationType, PhylumType
Direct Known Subclasses:
JmlClassDeclaration, JmlInterfaceDeclaration

public abstract class JmlTypeDeclaration
extends JmlMemberDeclaration
implements JTypeDeclarationType

This type represents a java class or interface in the syntax tree.


Nested Class Summary
 
Nested classes inherited from class org.jmlspecs.checker.JmlNode
JmlNode.DummyInitializerDeclaration
 
Field Summary
protected  JmlAxiom[] axioms
           
private  CContextType cachedContext
           
protected  JmlAxiom[] combinedAxioms
           
protected  JmlConstraint[] combinedConstraints
           
private  JFieldDeclarationType[] combinedFields
          The fields declared within the type represented by this, extracted from fieldsAndInits at initialization time and combined with any declarations refined by this type.
protected  JmlMemberDeclaration[] combinedInners
           
protected  JmlInvariant[] combinedInvariants
           
protected  JmlMemberDeclaration[] combinedMethods
           
protected  JmlRepresentsDecl[] combinedRepresentsDecls
           
protected  JmlVarAssertion[] combinedVarAssertions
           
protected  JmlConstraint[] constraints
           
protected  JmlDataGroupMemberMap dataGroupMap
           
private  JTypeDeclaration delegee
           
protected  boolean hasBeenCombinedWithRefinedDecl
           
private  boolean hasSourceInRefinement
          Indicates whether this type declaration has a source file in the refinement chain.
protected  ArrayList innerList
           
protected  JFieldDeclarationType[] interfaceModelFields
           
protected  boolean[] interfaceWeaklyFlags
           
protected  JmlInvariant[] invariants
           
private  JmlMemberAccess jmlAccess
           
protected  ArrayList methodList
           
protected  JFieldDeclarationType[] modelFields
           
protected  JmlRepresentsDecl[] representsDecls
           
protected  JFieldDeclarationType[] superClassModelFields
           
protected  JmlVarAssertion[] varAssertions
           
 
Fields inherited from class org.jmlspecs.checker.JmlMemberDeclaration
refinedDecl, refiningDecl
 
Fields inherited from class org.jmlspecs.checker.JmlNode
MJCVISIT_MESSAGE
 
Fields inherited from class org.multijava.mjc.JPhylum
EMPTY
 
Fields inherited from class org.multijava.util.compiler.Phylum
 
Fields inherited from class org.multijava.util.Utils
DBG_LEVEL_HIGH, DBG_LEVEL_LOW, DBG_LEVEL_NO
 
Fields inherited from interface org.jmlspecs.checker.Constants
ACC2_RAC_METHOD, ACC_CODE, ACC_CODE_BIGINT_MATH, ACC_CODE_JAVA_MATH, ACC_CODE_SAFE_MATH, ACC_GHOST, ACC_HELPER, ACC_INSTANCE, ACC_MODEL, ACC_MONITORED, ACC_QUERY, ACC_SECRET, ACC_SPEC_BIGINT_MATH, ACC_SPEC_JAVA_MATH, ACC_SPEC_PROTECTED, ACC_SPEC_PUBLIC, ACC_SPEC_SAFE_MATH, ACC_UNINITIALIZED, ACCESS_FLAG_ARRAY, ACCESS_FLAG_NAMES, AMID_BIGINT_MATH, EVERYTHING, JML_JMLObjectSet, NOT_SPECIFIED, NOTHING, OPE_BACKWARD_IMPLIES, OPE_EQUIV, OPE_EXISTS, OPE_FORALL, OPE_IMPLIES, OPE_L_ARROW, OPE_MAX, OPE_MIN, OPE_NOT_EQUIV, OPE_NUM_OF, OPE_PRODUCT, OPE_R_ARROW, OPE_SUBTYPE, OPE_SUM, SAME, TID_BIGINT, TID_REAL, TID_TYPE, TN_JMLOBJECTSET, TN_JMLTYPE, TN_JMLVALUESET
 
Fields inherited from interface org.multijava.mjc.Constants
ACC_MODIFIER_FLAGS_MASK, ACC_NON_NULL, ACC_NON_NULL_BY_DEFAULT, ACC_NULLABLE, ACC_NULLABLE_BY_DEFAULT, ACC_PURE, AMID_JAVA_MATH, AMID_MAX, AMID_SAFE_MATH, CMP_VERSION, IMPLICITLY_NON_NULL, JAV_ASSERTION_ERROR, JAV_CLASS, JAV_CLASSLOADER, JAV_CLASSNOTFOUND_EXCEPTION, JAV_CLONE, JAV_CLONEABLE, JAV_CONSTRUCTOR, JAV_ERROR, JAV_EXCEPTION, JAV_INIT, JAV_LENGTH, JAV_NAME_SEPARATOR, JAV_NOCLASSDEFFOUND_ERROR, JAV_OBJECT, JAV_OUTER_THIS, JAV_RMJ_RUNTIME_EXCEPTION, JAV_RUNTIME, JAV_RUNTIME_EXCEPTION, JAV_SERIALIZABLE, JAV_STATIC_INIT, JAV_STRING, JAV_STRINGBUFFER, JAV_SUPER, JAV_THIS, JAV_THROWABLE, MJ_ANCHOR, NULLITY_MODS, OPE_BAND, OPE_BNOT, OPE_BOR, OPE_BSR, OPE_BXOR, OPE_EQ, OPE_GE, OPE_GT, OPE_LAND, OPE_LE, OPE_LNOT, OPE_LOR, OPE_LT, OPE_MINUS, OPE_NE, OPE_PERCENT, OPE_PLUS, OPE_POSTDEC, OPE_POSTINC, OPE_PREDEC, OPE_PREINC, OPE_SIMPLE, OPE_SL, OPE_SLASH, OPE_SR, OPE_STAR, TID_ARRAY, TID_BOOLEAN, TID_BYTE, TID_CHAR, TID_CLASS, TID_DOUBLE, TID_FLOAT, TID_INT, TID_LONG, TID_MAX, TID_SHORT, TID_VOID, UNIV_ARRAY_TMP, UNIV_TMP
 
Fields inherited from interface org.multijava.util.classfile.Constants
ACC_ABSTRACT, ACC_FINAL, ACC_INTERFACE, ACC_NATIVE, ACC_PRIVATE, ACC_PROTECTED, ACC_PUBLIC, ACC_STATIC, ACC_STRICT, ACC_SUPER, ACC_SYNCHRONIZED, ACC_SYNTHETIC, ACC_TRANSIENT, ACC_VOLATILE, ATT_ANCHOR, ATT_BRIDGE, ATT_CODE, ATT_CONSTANTVALUE, ATT_DEPRECATED, ATT_DISPATCHER, ATT_EXCEPTIONS, ATT_GENERIC, ATT_GENERIC_FUNCTIONS, ATT_INNERCLASSES, ATT_LINENUMBERTABLE, ATT_LOCALVARIABLETABLE, ATT_MM_BODY, ATT_REDIRECTOR, ATT_RMJ_GLUE, ATT_RMJ_SIGNATURE, ATT_RUNTIME_VISIBLE_ANNOTATIONS, ATT_RUNTIME_VISIBLE_PARAMETER_ANNOTATIONS, ATT_SIGNATURE, ATT_SOURCEFILE, ATT_SYNTHETIC, ATT_UNIVERSE_FIELD, ATT_UNIVERSE_METHOD, ATT_UNIVERSE_VERSION, CST_CLASS, CST_DOUBLE, CST_FIELD, CST_FLOAT, CST_INTEGER, CST_INTERFACEMETHOD, CST_LONG, CST_METHOD, CST_NAMEANDTYPE, CST_STRING, CST_UTF8, ENV_DEBUG_MODE, ENV_USE_CACHE, JAVA_MAGIC, JAVA_MAJOR, JAVA_MINOR, MAX_CODE_PER_METHOD, opc_aaload, opc_aastore, opc_aconst_null, opc_aload, opc_aload_0, opc_aload_1, opc_aload_2, opc_aload_3, opc_anewarray, opc_areturn, opc_arraylength, opc_astore, opc_astore_0, opc_astore_1, opc_astore_2, opc_astore_3, opc_athrow, opc_baload, opc_bastore, opc_bipush, opc_caload, opc_castore, opc_checkcast, opc_d2f, opc_d2i, opc_d2l, opc_dadd, opc_daload, opc_dastore, opc_dcmpg, opc_dcmpl, opc_dconst_0, opc_dconst_1, opc_ddiv, opc_dload, opc_dload_0, opc_dload_1, opc_dload_2, opc_dload_3, opc_dmul, opc_dneg, opc_drem, opc_dreturn, opc_dstore, opc_dstore_0, opc_dstore_1, opc_dstore_2, opc_dstore_3, opc_dsub, opc_dup, opc_dup2, opc_dup2_x1, opc_dup2_x2, opc_dup_x1, opc_dup_x2, opc_f2d, opc_f2i, opc_f2l, opc_fadd, opc_faload, opc_fastore, opc_fcmpg, opc_fcmpl, opc_fconst_0, opc_fconst_1, opc_fconst_2, opc_fdiv, opc_fload, opc_fload_0, opc_fload_1, opc_fload_2, opc_fload_3, opc_fmul, opc_fneg, opc_frem, opc_freturn, opc_fstore, opc_fstore_0, opc_fstore_1, opc_fstore_2, opc_fstore_3, opc_fsub, opc_getfield, opc_getstatic, opc_goto, opc_goto_w, opc_i2b, opc_i2c, opc_i2d, opc_i2f, opc_i2l, opc_i2s, opc_iadd, opc_iaload, opc_iand, opc_iastore, opc_iconst_0, opc_iconst_1, opc_iconst_2, opc_iconst_3, opc_iconst_4, opc_iconst_5, opc_iconst_m1, opc_idiv, opc_if_acmpeq, opc_if_acmpne, opc_if_icmpeq, opc_if_icmpge, opc_if_icmpgt, opc_if_icmple, opc_if_icmplt, opc_if_icmpne, opc_ifeq, opc_ifge, opc_ifgt, opc_ifle, opc_iflt, opc_ifne, opc_ifnonnull, opc_ifnull, opc_iinc, opc_iload, opc_iload_0, opc_iload_1, opc_iload_2, opc_iload_3, opc_imul, opc_ineg, opc_instanceof, opc_invokeinterface, opc_invokespecial, opc_invokestatic, opc_invokevirtual, opc_ior, opc_irem, opc_ireturn, opc_ishl, opc_ishr, opc_istore, opc_istore_0, opc_istore_1, opc_istore_2, opc_istore_3, opc_isub, opc_iushr, opc_ixor, opc_jsr, opc_jsr_w, opc_l2d, opc_l2f, opc_l2i, opc_ladd, opc_laload, opc_land, opc_lastore, opc_lcmp, opc_lconst_0, opc_lconst_1, opc_ldc, opc_ldc2_w, opc_ldc_w, opc_ldiv, opc_lload, opc_lload_0, opc_lload_1, opc_lload_2, opc_lload_3, opc_lmul, opc_lneg, opc_lookupswitch, opc_lor, opc_lrem, opc_lreturn, opc_lshl, opc_lshr, opc_lstore, opc_lstore_0, opc_lstore_1, opc_lstore_2, opc_lstore_3, opc_lsub, opc_lushr, opc_lxor, opc_monitorenter, opc_monitorexit, opc_multianewarray, opc_new, opc_newarray, opc_nop, opc_pop, opc_pop2, opc_putfield, opc_putstatic, opc_ret, opc_return, opc_saload, opc_sastore, opc_sipush, opc_swap, opc_tableswitch, opc_wide, opc_xxxunusedxxx, POO_ASCII_CONSTANT, POO_CLASS_CONSTANT, POO_DOUBLE_CONSTANT, POO_FLOAT_CONSTANT, POO_INTEGER_CONSTANT, POO_LONG_CONSTANT, POO_NAT_CONSTANT, POO_REF_CONSTANT, POO_STRING_CONSTANT, TYP_ADDRESS, TYP_DOUBLE, TYP_FLOAT, TYP_INT, TYP_LONG, TYP_REFERENCE, TYP_VOID
 
Constructor Summary
JmlTypeDeclaration(TokenReference where, boolean[] interfaceWeaklyFlags, JmlInvariant[] invariants, JmlConstraint[] constraints, JmlRepresentsDecl[] representsDecls, JmlAxiom[] axioms, JmlVarAssertion[] varAssertions, JTypeDeclaration delegee)
           
 
Method Summary
 void accumAllTypeSignatures(ArrayList accum)
          Adds the signature CSourceClass of this, and of all nested types, to accum.
 void addMember(JMemberDeclarationType newMember)
          Adds the given member to this type's interface and modifies sourceClass to include the new member
 JmlAxiom[] axioms()
           
 void cachePassParameters(CContextType context)
          Caches the arguments for the compiler passes.
 void checkAssignableClauses()
           
private  void checkFieldsInterface(String javaFileName)
           
private  void checkForCycles(JmlTypeDeclaration refinedType)
          Sets the refinedType field of this JmlTypeDeclaration object.
 void checkInitializers()
          Invokes the checkInitializers method of the implementing class using previously cached arguments.
 void checkInitializers(CContextType context)
          Checks the static initializers created during the checkInterface pass and performs some other checks that can be performed simply before full blown typechecking.
 void checkInterface()
          Invokes the checkInterface method of the implementing class using previously cached arguments.
 void checkInterface(CContextType context)
          Checks the basic interfaces to make sure things generally look OK.
private  void checkMethodsInterface(String javaFileName)
           
private  void checkModelFields(JFieldDeclarationType[] modelFields)
           
 boolean checkRacability(Compiler compiler)
          Checks if every method is rac-compilable.
private  JmlTypeDeclaration checkRedundantRepresents(JmlRepresentsDecl redundantRep, String ident)
           
private  void combineClassSpecs()
           
 JmlAxiom[] combinedAxioms()
           
 JmlConstraint[] combinedConstraints()
           
 JmlInvariant[] combinedInvariants()
           
 JmlRepresentsDecl[] combinedRepresentsDecls()
           
 JmlVarAssertion[] combinedVarAssertions()
           
private  void combineFieldAndMethodModifiersOfNestedTypes()
           
private  void combineFieldModifiersAndSetInitializer()
           
private  void combineFieldSpecs()
           
private  void combineMethodModifiersAndSetBody()
           
private  void combineMethodSpecs()
           
private  void combineNestedClassSpecs()
           
private  void combineParameterModifiers(JmlMethodDeclaration meth)
           
 void combineSpecifications()
           
 int compareTo(Object o)
          Compares this to a given object.
 JmlConstraint[] constraints()
           
 JFieldDeclarationType[] fields()
           
 JPhylum[] fieldsAndInits()
          Returns an array of the static and instance initializers for the type represented by this.
 JmlTypeDeclaration findTypeWithRepresentsFor(CField field)
          Finds the applicable representsclause for a given model field by searching through the superclass and interface hierachies starting from the given type declaration.
 void generateInterface(Main compiler, CClass owner, CMemberHost host, String prefix, boolean isAnon, boolean isMember)
          Generates a CSourceClass class signature singleton for this declaration.
 JFieldDeclarationType[] getAllInterfaceModelFields()
          Returns all model fields inherited through the interface hierarchy.
 ArrayList getAllMethods()
          Walks up the extends hierarchy and adds all methods to the returned ArrayList.
 JFieldDeclarationType[] getAllSuperClassModelFields()
          Returns all model fields inherited from abstract superclasses.
 JFieldDeclarationType[] getCombinedFields()
           
 JmlMemberDeclaration[] getCombinedInners()
           
 JmlMemberDeclaration[] getCombinedMethods()
           
 JmlDataGroupMemberMap getDataGroupMap()
          Computes the data group map (if it has not already been computed) and returns it.
 JConstructorDeclarationType getDefaultConstructor()
           
 JFieldDeclarationType[] getModelFields()
          Computes and stores the model fields of this type into an array.
 boolean hasSourceInRefinement()
          Returns true if this type declaration has a source file in the refinement chain.
 String ident()
          Returns the identifier for this type declaration.
private  void includeAllFields()
           
private  void includeAllMethods()
           
private  void includeAllNestedClasses()
           
protected  void initializeDataGroupMap()
          Initializes the map from JmlSourceField, a data group, to a JmlAssignableFieldSet, the set of fields in that data group.
 boolean inJavaFile()
          Returns true if this member is declared in a '.java' file.
 ArrayList inners()
          Returns null unless overridden by a subclass.
 CClassType[] interfaces()
          Returns the set of interfaces that this type implements or extends.
 boolean[] interfaceWeaklyFlags()
           
 JmlInvariant[] invariants()
           
 boolean isAtTopLevel()
           
abstract  boolean isClass()
          Returns true if this is a class declaration.
 boolean isFinal()
          Returns true if this type declaration is for a final type.
 boolean isInterface()
          Returns true if this is an interface declaration.
 JmlMemberAccess jmlAccess()
           
private  void linkFieldRefinements()
          Links the fields in a refinement chain of this JmlTypeDeclaration object.
private  void linkInnerTypeRefinements()
          Links the inner types of a refinement chain of this JmlTypeDeclaration object.
private  void linkMethodRefinements()
          Links the methods in a refinement chain of this JmlTypeDeclaration object.
 ArrayList methods()
           
 long modifiers()
           
 CClass owner()
          Returns the logical owner of this type.
 void preprocessDependencies()
          Performs preliminary processing on compilation units and types.
 void preprocessDependencies(CContextType context)
          Performs preliminary processing on compilation units and types.
 JmlRepresentsDecl[] representsDecls()
           
 void resolveSpecializers()
          Resolves value specializer expressions to the compile-time constants they represent.
abstract  void resolveSpecializers(CContextType context)
          Computes the values of specializer expressions used to dispatch on compile-time constants.
 void resolveTopMethods()
          Finds the top method of every declared method.
 void setDefaultConstructor(JConstructorDeclarationType defaultConstructor)
           
 void setFields(JPhylum[] fields)
           
 void setFieldsOnly(JFieldDeclarationType[] fields)
           
 void setHasSourceInRefinement(boolean flag)
          Sets that if this type declaration has a source file in the refinement chain.
 void setIdent(String ident)
           
 void setInners(ArrayList v)
           
 void setMembersToCombinedMembers()
           
 void setMethods(ArrayList m)
           
 void setRefinedType(JmlBinaryType refinedType)
          Registers that the given type declaration, refinedType, is refined by this type declaration.
 void setRefinedType(JmlTypeDeclaration refinedType)
          Registers that the given type declaration, refinedType, is refined by this type declaration.
private  void setRefiningType(JmlTypeDeclaration refiningDecl)
           
 void setStatic()
          Marks this type as static.
 void syntheticOuterThisInaccessible()
          Records the fact that even though the class is an inner class, we should not generate an outer this for it, because the outer this is not accessible.
 void translateMJ()
          Invokes the translateMJ method of the implementing class using previously cached arguments.
 void translateMJ(CContextType context)
          Refactors this to include dispatchers for multimethods and other code necessary for running MultiJava code on a standard JVM.
 void typecheck()
          Invokes the typecheck method of the implementing class using previously cached arguments.
 void typecheck(CContextType context)
          Typechecks this type declaration in the context in which it appears.
private  void typecheckSuperTypes()
           
 CTypeVariable[] typevariables()
           
 void unsetStatic()
          Marks this type as non-static.
 JmlVarAssertion[] varAssertions()
           
 
Methods inherited from class org.jmlspecs.checker.JmlMemberDeclaration
accept, checkRefinedModifiers, findJavaFileInRefinement, genComments, getCClass, getCombinedSpecification, getCombinedVarAssertions, getField, getMethod, getMostRefined, getRefinedMember, getRefiningMember, inBinaryClassFile, isDeprecated, isRefined, isRefiningMember, javadocComment, setRefinedMember, setRefiningMember, stringRepresentation
 
Methods inherited from class org.jmlspecs.checker.JmlNode
enterSpecScope, enterSpecScope, exitSpecScope, exitSpecScope, privacy, privacyString
 
Methods inherited from class org.multijava.mjc.JPhylum
check, check, check, check, fail, fail, fail, warn, warn, warn, warn
 
Methods inherited from class org.multijava.util.compiler.Phylum
getTokenReference, setTokenReference
 
Methods inherited from class org.multijava.util.Utils
assertTrue, assertTrue, combineArrays, escapeString, escapeString, fail, fail, getFilePath, hasFlag, hasOtherFlags, parsePathParts, relativePathTo, splitQualifiedName, splitQualifiedName, stripJavaModifiers, stripNonJavaModifiers, stripPrivateModifier, unescapeString, vectorToArray, vectorToIntArray
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 
Methods inherited from interface org.multijava.mjc.JTypeDeclarationType
createContext
 
Methods inherited from interface org.multijava.mjc.JMemberDeclarationType
accept, genComments, getCClass, getField, getMethod, isDeprecated
 
Methods inherited from interface org.multijava.util.compiler.PhylumType
getTokenReference, setTokenReference
 
Methods inherited from interface org.multijava.javadoc.Annotatable
javadocComment
 
Methods inherited from interface org.multijava.mjc.CompilerPassEnterable
accept, getTokenReference
 

Field Detail

cachedContext

private CContextType cachedContext

delegee

private JTypeDeclaration delegee

jmlAccess

private JmlMemberAccess jmlAccess

interfaceWeaklyFlags

protected boolean[] interfaceWeaklyFlags

invariants

protected JmlInvariant[] invariants

constraints

protected JmlConstraint[] constraints

representsDecls

protected JmlRepresentsDecl[] representsDecls

axioms

protected JmlAxiom[] axioms

varAssertions

protected JmlVarAssertion[] varAssertions

combinedInvariants

protected JmlInvariant[] combinedInvariants

combinedConstraints

protected JmlConstraint[] combinedConstraints

combinedRepresentsDecls

protected JmlRepresentsDecl[] combinedRepresentsDecls

combinedAxioms

protected JmlAxiom[] combinedAxioms

combinedVarAssertions

protected JmlVarAssertion[] combinedVarAssertions

combinedFields

private JFieldDeclarationType[] combinedFields
The fields declared within the type represented by this, extracted from fieldsAndInits at initialization time and combined with any declarations refined by this type.


methodList

protected ArrayList methodList

combinedMethods

protected JmlMemberDeclaration[] combinedMethods

innerList

protected ArrayList innerList

combinedInners

protected JmlMemberDeclaration[] combinedInners

modelFields

protected JFieldDeclarationType[] modelFields

superClassModelFields

protected JFieldDeclarationType[] superClassModelFields

interfaceModelFields

protected JFieldDeclarationType[] interfaceModelFields

dataGroupMap

protected JmlDataGroupMemberMap dataGroupMap

hasSourceInRefinement

private boolean hasSourceInRefinement
Indicates whether this type declaration has a source file in the refinement chain. This field is used by jmlrac.


hasBeenCombinedWithRefinedDecl

protected boolean hasBeenCombinedWithRefinedDecl
Constructor Detail

JmlTypeDeclaration

public JmlTypeDeclaration(TokenReference where,
                          boolean[] interfaceWeaklyFlags,
                          JmlInvariant[] invariants,
                          JmlConstraint[] constraints,
                          JmlRepresentsDecl[] representsDecls,
                          JmlAxiom[] axioms,
                          JmlVarAssertion[] varAssertions,
                          JTypeDeclaration delegee)
Method Detail

generateInterface

public void generateInterface(Main compiler,
                              CClass owner,
                              CMemberHost host,
                              String prefix,
                              boolean isAnon,
                              boolean isMember)
Generates a CSourceClass class signature singleton for this declaration.

Specified by:
generateInterface in interface JTypeDeclarationType
Parameters:
compiler - the compiler instance for which this singleton is generated
owner - the class signature singleton for the logical outer class of this, or null if this is a top level declaration
host - the signature singleton of the context in which this is declared, a CCompilationUnit for top-level declarations
prefix - the prefix prepended to this declaration's identifier to achieve the fully qualified name, just the package name (using '/' separators) for top-level classes, package name plus $-delimited outer class names plus synthetic index for inner classes
isAnon - true if this is an anonymous class, in which case the fully qualified name is just prefix
isMember - true if this is a member type, i.e., a nested type that is not a local type or an anonymous class

interfaceWeaklyFlags

public boolean[] interfaceWeaklyFlags()

invariants

public JmlInvariant[] invariants()

constraints

public JmlConstraint[] constraints()

representsDecls

public JmlRepresentsDecl[] representsDecls()

axioms

public JmlAxiom[] axioms()

varAssertions

public JmlVarAssertion[] varAssertions()

combinedInvariants

public JmlInvariant[] combinedInvariants()

combinedConstraints

public JmlConstraint[] combinedConstraints()

combinedRepresentsDecls

public JmlRepresentsDecl[] combinedRepresentsDecls()

combinedAxioms

public JmlAxiom[] combinedAxioms()

combinedVarAssertions

public JmlVarAssertion[] combinedVarAssertions()

typevariables

public CTypeVariable[] typevariables()

interfaces

public CClassType[] interfaces()
Description copied from interface: JTypeDeclarationType
Returns the set of interfaces that this type implements or extends.

Specified by:
interfaces in interface JTypeDeclarationType

fieldsAndInits

public JPhylum[] fieldsAndInits()
Returns an array of the static and instance initializers for the type represented by this.

Specified by:
fieldsAndInits in interface JTypeDeclarationType

methods

public ArrayList methods()
Specified by:
methods in interface JTypeDeclarationType

setMethods

public void setMethods(ArrayList m)

inners

public ArrayList inners()
Description copied from class: JmlMemberDeclaration
Returns null unless overridden by a subclass. Returns null if it does not have any inner type declarations.

Specified by:
inners in interface JTypeDeclarationType
Overrides:
inners in class JmlMemberDeclaration

setInners

public void setInners(ArrayList v)
Specified by:
setInners in interface JTypeDeclarationType

isAtTopLevel

public boolean isAtTopLevel()
Specified by:
isAtTopLevel in interface JTypeDeclarationType
Returns:
true if this class is at top level

fields

public JFieldDeclarationType[] fields()
Specified by:
fields in interface JTypeDeclarationType

getDefaultConstructor

public JConstructorDeclarationType getDefaultConstructor()
Specified by:
getDefaultConstructor in interface JTypeDeclarationType

setDefaultConstructor

public void setDefaultConstructor(JConstructorDeclarationType defaultConstructor)
Specified by:
setDefaultConstructor in interface JTypeDeclarationType

setIdent

public void setIdent(String ident)
Specified by:
setIdent in interface JTypeDeclarationType

ident

public String ident()
Returns the identifier for this type declaration.

Specified by:
ident in interface JTypeDeclarationType
Returns:
the unqualified identifier for this type declaration

addMember

public void addMember(JMemberDeclarationType newMember)
Adds the given member to this type's interface and modifies sourceClass to include the new member

Specified by:
addMember in interface JTypeDeclarationType
Parameters:
newMember - a member to be added to this type

setFields

public void setFields(JPhylum[] fields)

setFieldsOnly

public void setFieldsOnly(JFieldDeclarationType[] fields)

owner

public CClass owner()
Returns the logical owner of this type.

Specified by:
owner in interface JTypeDeclarationType

modifiers

public long modifiers()
Specified by:
modifiers in interface JTypeDeclarationType

setStatic

public void setStatic()
Marks this type as static.

 also
   requires (* this.generateInterface(...) has not been invoked *);
   requires_redundantly (* sourceClass == null *); 
   ensures hasFlag(delegee.modifiers(), ACC_STATIC);
 

Specified by:
setStatic in interface JTypeDeclarationType

unsetStatic

public void unsetStatic()
Marks this type as non-static.

 also 
 ensures !hasFlag(delegee.modifiers,ACC_STATIC);
 

Specified by:
unsetStatic in interface JTypeDeclarationType

syntheticOuterThisInaccessible

public void syntheticOuterThisInaccessible()
Records the fact that even though the class is an inner class, we should not generate an outer this for it, because the outer this is not accessible. The sourceClass field should not be null.

Specified by:
syntheticOuterThisInaccessible in interface JTypeDeclarationType

accumAllTypeSignatures

public void accumAllTypeSignatures(ArrayList accum)
Adds the signature CSourceClass of this, and of all nested types, to accum.

Specified by:
accumAllTypeSignatures in interface JTypeDeclarationType

isFinal

public boolean isFinal()
Returns true if this type declaration is for a final type.


isClass

public abstract boolean isClass()
Returns true if this is a class declaration.


isInterface

public boolean isInterface()
Returns true if this is an interface declaration.


hasSourceInRefinement

public boolean hasSourceInRefinement()
Returns true if this type declaration has a source file in the refinement chain. This method is used by jmlrac.


setHasSourceInRefinement

public void setHasSourceInRefinement(boolean flag)
Sets that if this type declaration has a source file in the refinement chain. This method is used by jmlrac.


jmlAccess

public JmlMemberAccess jmlAccess()
Returns:
the member access information object for this member.

inJavaFile

public boolean inJavaFile()
Returns true if this member is declared in a '.java' file.

Overrides:
inJavaFile in class JmlMemberDeclaration

getDataGroupMap

public JmlDataGroupMemberMap getDataGroupMap()
Computes the data group map (if it has not already been computed) and returns it. The data group map is a map from each field to the set of fields in its data group. Only model, spec_public, and spec_protected fields can have more than one field (itself) in this set.


getModelFields

public JFieldDeclarationType[] getModelFields()
Computes and stores the model fields of this type into an array. These are the fields that need to have a represents clause and have an associated data group. Returns an array of the model fields of this type (not including model fields inherited from interfaces implemented or from the superclass).


initializeDataGroupMap

protected void initializeDataGroupMap()
Initializes the map from JmlSourceField, a data group, to a JmlAssignableFieldSet, the set of fields in that data group.


getAllSuperClassModelFields

public JFieldDeclarationType[] getAllSuperClassModelFields()
Returns all model fields inherited from abstract superclasses. This method must be called at the end of typechecking.


getAllInterfaceModelFields

public JFieldDeclarationType[] getAllInterfaceModelFields()
Returns all model fields inherited through the interface hierarchy. This method must be called at the end of typechecking.


findTypeWithRepresentsFor

public JmlTypeDeclaration findTypeWithRepresentsFor(CField field)
Finds the applicable representsclause for a given model field by searching through the superclass and interface hierachies starting from the given type declaration. If such a clause is found, returns the type declaration that includes the clause; otherwise, returns null.

 requires field != null && hasFlag(field.modifiers(),ACC_MODEL);
 ensures \result != null ==> (* \result has represents clause  r 
   such that !r.isRedundantly() && r.usesAbstractionFunction() && 
   r.storeRef() refers to field *);
 


checkRedundantRepresents

private JmlTypeDeclaration checkRedundantRepresents(JmlRepresentsDecl redundantRep,
                                                    String ident)

getAllMethods

public ArrayList getAllMethods()
Walks up the extends hierarchy and adds all methods to the returned ArrayList.

Specified by:
getAllMethods in interface JTypeDeclarationType
Returns:
a ArrayList that includes the CMethods for all methods in this class and all direct ancestors

preprocessDependencies

public void preprocessDependencies(CContextType context)
                            throws PositionedError
Performs preliminary processing on compilation units and types. Processes type imports so external methods' receiver types can be analyzed and supertypes can be resolved. Groups external methods by name, corresponding to the anchor classes that will eventually be generated. Mutates the name space management in CTopLevel to record a CGenericFunctionCollection singleton for each anchor class.

Specified by:
preprocessDependencies in interface JTypeDeclarationType
Throws:
PositionedError

checkInterface

public void checkInterface(CContextType context)
                    throws PositionedError
Checks the basic interfaces to make sure things generally look OK. This pass gathers information about the type signatures of everything (imported class files, classes being compiled, methods, fields, etc...) needed for the later passes. This information is stored in a CCompilationUnit instance and instances of CMember that are bound to the AST. Also adds things like the default constructor and the initializer method to the AST (these are suppressed during pretty-printing).

Specified by:
checkInterface in interface JTypeDeclarationType
Parameters:
context - the context in which this decl appears
Throws:
PositionedError - an error with reference to the source file

checkInitializers

public void checkInitializers(CContextType context)
                       throws PositionedError
Checks the static initializers created during the checkInterface pass and performs some other checks that can be performed simply before full blown typechecking.

Specified by:
checkInitializers in interface JTypeDeclarationType
Parameters:
context - the context in which this class declaration appears
Throws:
PositionedError - if check fails

resolveSpecializers

public abstract void resolveSpecializers(CContextType context)
                                  throws PositionedError
Computes the values of specializer expressions used to dispatch on compile-time constants. The JML-specific combining of specifications is done during this pass so computing the data group members and the assignable fields of a method can be computed during typechecking.

Specified by:
resolveSpecializers in interface JTypeDeclarationType
Parameters:
context - the context in which this class declaration appears
Throws:
PositionedError - if the check fails

resolveTopMethods

public void resolveTopMethods()
                       throws PositionedError
Finds the top method of every declared method. Called after the checkInitializers pass. This cannot be done before then because the external generic function mappings are not complete until the end of the checkInterface pass and the constant value specializers are not known until after the checkInitializers pass. This must be done before the typecheck pass so that all specialized argument positions for generic functions are known for ambiguity checking.

Specified by:
resolveTopMethods in interface JTypeDeclarationType
Throws:
PositionedError

typecheck

public void typecheck(CContextType context)
               throws PositionedError
Typechecks this type declaration in the context in which it appears. Mutates the context to record the information learned during checking. Actually just updates the context by adding a CSourceClass representation of this. Overriding methods in subclasses of this handle the actual checks.

Specified by:
typecheck in interface JTypeDeclarationType
Parameters:
context - the context in which this type declaration appears
Throws:
PositionedError - if any checks fail

translateMJ

public void translateMJ(CContextType context)
Refactors this to include dispatchers for multimethods and other code necessary for running MultiJava code on a standard JVM.

Specified by:
translateMJ in interface JTypeDeclarationType

compareTo

public int compareTo(Object o)
              throws ClassCastException
Compares this to a given object.

 also
   requires o instanceof JmlTypeDeclaration;
	 ensures (* \result is ordered according to suffix of the source files *);
 also
   requires o != null && !(o instanceof JmlTypeDeclaration);
	 signals_only ClassCastException;
 

Specified by:
compareTo in interface Comparable
Parameters:
o - an Object value to compare to this
Returns:
0 if this.equals(o)
Throws:
ClassCastException - if o is incomparable to this

cachePassParameters

public void cachePassParameters(CContextType context)
Caches the arguments for the compiler passes.

Specified by:
cachePassParameters in interface JTypeDeclarationType
See Also:
!FIXME! this spec (or the implementation) is wrong, delegee's state is not changed

 also
  ensures delegee.arePassParametersCached;
 

preprocessDependencies

public void preprocessDependencies()
                            throws PositionedError
Performs preliminary processing on compilation units and types. Processes type imports so external methods' receiver types can be analyzed and supertypes can be resolved. Groups external methods by name, corresponding to the anchor classes that will eventually be generated. Mutates the name space management in CTopLevel to record a CGenericFunctionCollection singleton for each anchor class.

Specified by:
preprocessDependencies in interface CompilerPassEnterable
Throws:
PositionedError

checkInterface

public void checkInterface()
                    throws PositionedError
Description copied from interface: CompilerPassEnterable
Invokes the checkInterface method of the implementing class using previously cached arguments.

 requires arePassParametersCached;
 

Specified by:
checkInterface in interface CompilerPassEnterable
Throws:
PositionedError

checkInitializers

public void checkInitializers()
                       throws PositionedError
Description copied from interface: CompilerPassEnterable
Invokes the checkInitializers method of the implementing class using previously cached arguments.

 requires arePassParametersCached;
 

Specified by:
checkInitializers in interface CompilerPassEnterable
Throws:
PositionedError

resolveSpecializers

public void resolveSpecializers()
                         throws PositionedError
Description copied from interface: CompilerPassEnterable
Resolves value specializer expressions to the compile-time constants they represent. Must come after the checkInitializers phase.

Specified by:
resolveSpecializers in interface CompilerPassEnterable
Throws:
PositionedError

typecheck

public void typecheck()
               throws PositionedError
Description copied from interface: CompilerPassEnterable
Invokes the typecheck method of the implementing class using previously cached arguments.

 requires arePassParametersCached;
 

Specified by:
typecheck in interface CompilerPassEnterable
Throws:
PositionedError

translateMJ

public void translateMJ()
Description copied from interface: CompilerPassEnterable
Invokes the translateMJ method of the implementing class using previously cached arguments.

 requires arePassParametersCached;
 

Specified by:
translateMJ in interface CompilerPassEnterable

setRefinedType

public void setRefinedType(JmlBinaryType refinedType)
Registers that the given type declaration, refinedType, is refined by this type declaration.


setRefinedType

public void setRefinedType(JmlTypeDeclaration refinedType)
                    throws PositionedError
Registers that the given type declaration, refinedType, is refined by this type declaration.

Throws:
PositionedError

checkForCycles

private void checkForCycles(JmlTypeDeclaration refinedType)
                     throws PositionedError
Sets the refinedType field of this JmlTypeDeclaration object. Throws an exception if setting this field would have created a cycle in the refinement sequence.

Throws:
PositionedError

setRefiningType

private void setRefiningType(JmlTypeDeclaration refiningDecl)

checkFieldsInterface

private void checkFieldsInterface(String javaFileName)

checkModelFields

private void checkModelFields(JFieldDeclarationType[] modelFields)

typecheckSuperTypes

private void typecheckSuperTypes()

checkMethodsInterface

private void checkMethodsInterface(String javaFileName)

checkAssignableClauses

public void checkAssignableClauses()
                            throws PositionedError
Throws:
PositionedError

getCombinedFields

public JFieldDeclarationType[] getCombinedFields()

getCombinedMethods

public JmlMemberDeclaration[] getCombinedMethods()

getCombinedInners

public JmlMemberDeclaration[] getCombinedInners()

setMembersToCombinedMembers

public void setMembersToCombinedMembers()

combineFieldModifiersAndSetInitializer

private void combineFieldModifiersAndSetInitializer()

combineMethodModifiersAndSetBody

private void combineMethodModifiersAndSetBody()

combineParameterModifiers

private void combineParameterModifiers(JmlMethodDeclaration meth)

combineFieldAndMethodModifiersOfNestedTypes

private void combineFieldAndMethodModifiersOfNestedTypes()

combineSpecifications

public void combineSpecifications()
Description copied from class: JmlMemberDeclaration
Combine the specifications of this declaration with the specifications of the declarations it refines.


linkFieldRefinements

private void linkFieldRefinements()
Links the fields in a refinement chain of this JmlTypeDeclaration object.


linkMethodRefinements

private void linkMethodRefinements()
Links the methods in a refinement chain of this JmlTypeDeclaration object.


linkInnerTypeRefinements

private void linkInnerTypeRefinements()
                               throws PositionedError
Links the inner types of a refinement chain of this JmlTypeDeclaration object.

Throws:
PositionedError

combineMethodSpecs

private void combineMethodSpecs()

includeAllMethods

private void includeAllMethods()

combineFieldSpecs

private void combineFieldSpecs()

includeAllFields

private void includeAllFields()

combineNestedClassSpecs

private void combineNestedClassSpecs()

includeAllNestedClasses

private void includeAllNestedClasses()

combineClassSpecs

private void combineClassSpecs()

checkRacability

public boolean checkRacability(Compiler compiler)
Checks if every method is rac-compilable. That is, checks that all concrete methods have body.


JML

JML is Copyright (C) 1998-2002 by Iowa State University and is distributed under the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version. This release depends on code from the MultiJava project and is based in part on the Kopi project Copyright (C) 1990-99 DMS Decision Management Systems Ges.m.b.H.