JML

org.jmlspecs.checker
Class JmlInterfaceDeclaration

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
                          extended byorg.jmlspecs.checker.JmlInterfaceDeclaration
All Implemented Interfaces:
Annotatable, Cloneable, Comparable, CompilerPassEnterable, Constants, Constants, Constants, JInterfaceDeclarationType, JMemberDeclarationType, JTypeDeclarationType, PhylumType

public class JmlInterfaceDeclaration
extends JmlTypeDeclaration
implements JInterfaceDeclarationType

This class represents a java interface in the syntax tree


Nested Class Summary
 
Nested classes inherited from class org.jmlspecs.checker.JmlNode
JmlNode.DummyInitializerDeclaration
 
Field Summary
protected  JInterfaceDeclarationWrapper delegee
           
 
Fields inherited from class org.jmlspecs.checker.JmlTypeDeclaration
axioms, combinedAxioms, combinedConstraints, combinedInners, combinedInvariants, combinedMethods, combinedRepresentsDecls, combinedVarAssertions, constraints, dataGroupMap, hasBeenCombinedWithRefinedDecl, innerList, interfaceModelFields, interfaceWeaklyFlags, invariants, methodList, modelFields, representsDecls, superClassModelFields, 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
protected JmlInterfaceDeclaration(TokenReference where, boolean[] interfaceWeaklyFlags, JmlInvariant[] invariants, JmlConstraint[] constraints, JmlRepresentsDecl[] representsDecls, JmlAxiom[] axioms, JmlVarAssertion[] varAssertions, JInterfaceDeclarationWrapper delegee)
          Constructs a new JML interface declaration; clients should use factory method makeInstance instead.
 
Method Summary
 void accept(MjcVisitor p)
          Accepts the specified visitor.
 CClassContextType createContext(CContextType parent)
          Creates an interface context for this interface declaration.
 JFieldDeclarationType[] getAllInterfaceModelFields()
          Returns all model fields inherited through the interface hierarchy.
 boolean isClass()
          Returns true if this is an interface declaration.
static JmlInterfaceDeclaration makeInstance(TokenReference where, long modifiers, String ident, CTypeVariable[] typevariables, CClassType[] interfaces, boolean[] interfaceWeaklyFlags, ArrayList methods, ArrayList inners, JPhylum[] fieldsAndInits, JmlInvariant[] invariants, JmlConstraint[] constraints, JmlRepresentsDecl[] representsDecls, JmlAxiom[] axioms, JmlVarAssertion[] varAssertions, JavadocComment javadoc, JavaStyleComment[] comment, boolean isRefinedType)
          Constructs an interface declaration in the parsing tree.
 void resolveSpecializers(CContextType context)
          Computes the values of specializer expressions used to dispatch on compile-time constants.
 
Methods inherited from class org.jmlspecs.checker.JmlTypeDeclaration
accumAllTypeSignatures, addMember, axioms, cachePassParameters, checkAssignableClauses, checkInitializers, checkInitializers, checkInterface, checkInterface, checkRacability, combinedAxioms, combinedConstraints, combinedInvariants, combinedRepresentsDecls, combinedVarAssertions, combineSpecifications, compareTo, constraints, fields, fieldsAndInits, findTypeWithRepresentsFor, generateInterface, getAllMethods, getAllSuperClassModelFields, getCombinedFields, getCombinedInners, getCombinedMethods, getDataGroupMap, getDefaultConstructor, getModelFields, hasSourceInRefinement, ident, initializeDataGroupMap, inJavaFile, inners, interfaces, interfaceWeaklyFlags, invariants, isAtTopLevel, isFinal, isInterface, jmlAccess, methods, modifiers, owner, preprocessDependencies, preprocessDependencies, representsDecls, resolveSpecializers, resolveTopMethods, setDefaultConstructor, setFields, setFieldsOnly, setHasSourceInRefinement, setIdent, setInners, setMembersToCombinedMembers, setMethods, setRefinedType, setRefinedType, setStatic, syntheticOuterThisInaccessible, translateMJ, translateMJ, typecheck, typecheck, typevariables, unsetStatic, varAssertions
 
Methods inherited from class org.jmlspecs.checker.JmlMemberDeclaration
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
accumAllTypeSignatures, addMember, cachePassParameters, checkInitializers, checkInterface, fields, fieldsAndInits, generateInterface, getAllMethods, getDefaultConstructor, ident, inners, interfaces, isAtTopLevel, methods, modifiers, owner, preprocessDependencies, resolveTopMethods, setDefaultConstructor, setIdent, setInners, setStatic, syntheticOuterThisInaccessible, translateMJ, typecheck, unsetStatic
 
Methods inherited from interface org.multijava.mjc.JMemberDeclarationType
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
checkInitializers, checkInterface, getTokenReference, preprocessDependencies, resolveSpecializers, translateMJ, typecheck
 
Methods inherited from interface java.lang.Comparable
compareTo
 

Field Detail

delegee

protected JInterfaceDeclarationWrapper delegee
Constructor Detail

JmlInterfaceDeclaration

protected JmlInterfaceDeclaration(TokenReference where,
                                  boolean[] interfaceWeaklyFlags,
                                  JmlInvariant[] invariants,
                                  JmlConstraint[] constraints,
                                  JmlRepresentsDecl[] representsDecls,
                                  JmlAxiom[] axioms,
                                  JmlVarAssertion[] varAssertions,
                                  JInterfaceDeclarationWrapper delegee)
Constructs a new JML interface declaration; clients should use factory method makeInstance instead. Because this class and the super class both hold aliases to the same delegee (to avoid casts during delegation), this constructor is private.

Method Detail

makeInstance

public static JmlInterfaceDeclaration makeInstance(TokenReference where,
                                                   long modifiers,
                                                   String ident,
                                                   CTypeVariable[] typevariables,
                                                   CClassType[] interfaces,
                                                   boolean[] interfaceWeaklyFlags,
                                                   ArrayList methods,
                                                   ArrayList inners,
                                                   JPhylum[] fieldsAndInits,
                                                   JmlInvariant[] invariants,
                                                   JmlConstraint[] constraints,
                                                   JmlRepresentsDecl[] representsDecls,
                                                   JmlAxiom[] axioms,
                                                   JmlVarAssertion[] varAssertions,
                                                   JavadocComment javadoc,
                                                   JavaStyleComment[] comment,
                                                   boolean isRefinedType)
Constructs an interface declaration in the parsing tree.

Parameters:
where - the line of this node in the source code
modifiers - the list of modifiers of this class
ident - the short name of this class
interfaces - the names of this types's interfaces
methods - a list of JMethodDeclarationTypes giving the methods of this type
inners - a list of JTypeDeclarationTypes giving the inner classes (and interfaces) of this type
fieldsAndInits - the fields and initializers of this type, passed together because the order matters for class and object initialization, members of the array should be instances of JFieldDeclarationType or JClassBlock
javadoc - javadoc comments including whether this type declaration is deprecated
comment - regular java comments
See Also:
JMethodDeclarationType, JFieldDeclarationType, JClassBlock

isClass

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


getAllInterfaceModelFields

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

Overrides:
getAllInterfaceModelFields in class JmlTypeDeclaration

createContext

public CClassContextType createContext(CContextType parent)
Creates an interface context for this interface declaration.

Specified by:
createContext in interface JInterfaceDeclarationType
Parameters:
parent - the parent context or null
Returns:
returns a CClassContextType that represents this context

accept

public void accept(MjcVisitor p)
Accepts the specified visitor.

Specified by:
accept in interface JMemberDeclarationType
Overrides:
accept in class JmlMemberDeclaration
Parameters:
p - the visitor

resolveSpecializers

public void resolveSpecializers(CContextType context)
                         throws PositionedError
Computes the values of specializer expressions used to dispatch on compile-time constants.

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

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.