org.jmlspecs.checker
Class JmlInterfaceDeclaration

java.lang.Object
  org.multijava.util.Utils
      org.multijava.util.compiler.Phylum
          org.multijava.mjc.JPhylum
              org.jmlspecs.checker.JmlNode
                  org.jmlspecs.checker.JmlMemberDeclaration
                      org.jmlspecs.checker.JmlTypeDeclaration
                          org.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.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_NON_NULL, ACC_NON_NULL_BY_DEFAULT, ACC_NULLABLE, ACC_NULLABLE_BY_DEFAULT, 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_PURE, AMID_JAVA_MATH, AMID_MAX, AMID_SAFE_MATH, CMP_VERSION, 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, 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_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, 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, 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

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.

makeInstance

public static JmlInterfaceDeclaration makeInstance(TokenReference where,
                                                   long modifiers,
                                                   String ident,
                                                   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