edu.utep.cs.utjml.compiler
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
                              edu.utep.cs.utjml.compiler.JmlInterfaceDeclaration

All Implemented Interfaces:

Cloneable, Comparable, Annotatable, CompilerPassEnterable, JInterfaceDeclarationType, JMemberDeclarationType, JTypeDeclarationType, Constants, PhylumType

public class JmlInterfaceDeclaration
extends JmlInterfaceDeclaration

This class represents a java interface in the syntax tree

Field Summary

protected JmlCallSequence[]

callSequences

Fields inherited from class org.jmlspecs.checker.JmlInterfaceDeclaration

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.Utils

DBG_LEVEL_HIGH, DBG_LEVEL_LOW, DBG_LEVEL_NO

Fields inherited from interface org.jmlspecs.checker.Constants

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, ACC2_RAC_METHOD, 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_dup_x1, opc_dup_x2, opc_dup2, opc_dup2_x1, opc_dup2_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_ldc_w, opc_ldc2_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

Method Summary

void	accept(MjcVisitor p) Accepts the specified visitor.
JmlCallSequence[]	callSequences()
CClassContextType	createContext(CContextType parent) Creates an interface context for this 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, JmlCallSequence[] callSequences, 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.
void	typecheck(CContextType context) Typechecks this interface declaration in the context in which it appears.

Methods inherited from class org.jmlspecs.checker.JmlInterfaceDeclaration

getAllInterfaceModelFields, isClass, makeInstance

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, 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, 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

callSequences

protected JmlCallSequence[] callSequences

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,
                                                   JmlCallSequence[] callSequences,
                                                   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

typecheck

public void typecheck(CContextType context)
               throws PositionedError

Typechecks this interface 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. This method is overriden here to typecheck call sequence clauses.

Specified by:

typecheck in interface JTypeDeclarationType

Overrides:

typecheck in class JmlTypeDeclaration

Parameters:

context - the context in which this type declaration appears

Throws:

PositionedError - if any checks fail

callSequences

public JmlCallSequence[] callSequences()

createContext

public CClassContextType createContext(CContextType parent)

Creates an interface context for this interface declaration.

Specified by:

createContext in interface JInterfaceDeclarationType

Specified by:

createContext in interface JTypeDeclarationType

Overrides:

createContext in class JmlInterfaceDeclaration

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 CompilerPassEnterable

Specified by:

accept in interface JMemberDeclarationType

Overrides:

accept in class JmlInterfaceDeclaration

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

Overrides:

resolveSpecializers in class JmlInterfaceDeclaration

Parameters:

context - the context in which this class declaration appears

Throws:

PositionedError - if the check fails