UTJML

edu.utep.cs.utjml.compiler
Class JmlInterfaceDeclaration

java.lang.Object
  extended by org.multijava.util.Utils
      extended by org.multijava.util.compiler.Phylum
          extended by org.multijava.mjc.JPhylum
              extended by org.jmlspecs.checker.JmlNode
                  extended by org.jmlspecs.checker.JmlMemberDeclaration
                      extended by org.jmlspecs.checker.JmlTypeDeclaration
                          extended by org.jmlspecs.checker.JmlInterfaceDeclaration
                              extended by 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

UTJML

UTJML is Copyright (C) 2004-2006 by University of Texas at El Paso 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 JML project.