JML

org.jmlspecs.checker
Class JmlRepresentsDecl

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.JmlDeclaration
                      extended byorg.jmlspecs.checker.JmlRepresentsDecl
All Implemented Interfaces:
Cloneable, Constants, Constants, Constants, PhylumType

public class JmlRepresentsDecl
extends JmlDeclaration

This AST node represents a JML represents declaration annotation. The syntax for the represents declaration is as follows.

  represents-decl ::= represents-keyword store-ref "<-" spec-expression ";"
    | represents-keyword store-ref "=" spec-expression ";"
    | represetns-keyword store-ref "\such_that" predicate ";"
  represents-keyword ::= "represents" | "represents_redundantly"
 

Version:
$Revision: 1.18 $
Author:
Curtis Clifton

Nested Class Summary
 
Nested classes inherited from class org.jmlspecs.checker.JmlNode
JmlNode.DummyInitializerDeclaration
 
Field Summary
private  JmlPredicate predicate
           
private  JmlSpecExpression specExpression
           
protected  JmlStoreRefExpression storeRef
          An AST for the storeRef expression of the more abstract variable in this.
 
Fields inherited from class org.jmlspecs.checker.JmlDeclaration
modifiers, redundantly
 
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
JmlRepresentsDecl(TokenReference where, long modifiers, boolean redundantly, JmlStoreRefExpression storeRef, JmlPredicate predicate)
          Creates a new JmlRepresentsDecl instance.
JmlRepresentsDecl(TokenReference where, long modifiers, boolean redundantly, JmlStoreRefExpression storeRef, JmlSpecExpression specExpression)
          Creates a new JmlRepresentsDecl instance.
 
Method Summary
 void accept(MjcVisitor p)
          Accepts the specified visitor.
protected  void checkRightHandSide(JmlExpressionContext context)
          Performs type-checking of right-hand side of the represents clause.
protected  void checkStoreRef(JmlExpressionContext context)
          Checks the store ref of this depends/represents clause.
 JmlSourceField getField()
          Returns the JmlSourceField of the model variable that this represents clause specifies for.
 String ident()
          Returns the identifier of the represented model field.
protected static boolean isInheritedOrOuter(JClassFieldExpression field)
          Returns true if the given field expression refers to a field declared in this class, inherited from a superclasse or interface, or defined in an outer class or interface.
 JmlPredicate predicate()
          Returns the predicate of this represents declaration.
 JmlSpecExpression specExpression()
          Returns the spec expression of this represents declaration.
 JmlStoreRefExpression storeRef()
          Returns the store ref expression of this represents declaration.
 void typecheck(CContextType context)
          Typechecks this depends/represents clause in the context in which it appears.
 boolean usesAbstractionFunction()
          Indicates whether this represents declaration uses an abstraction function.
 boolean usesAbstractionRelation()
          Indicates whether this represents declaration uses an abstraction relations.
 
Methods inherited from class org.jmlspecs.checker.JmlDeclaration
checkModifiers, clone, createContext, createContextHelper, isRedundantly, isStatic, modifiers, privacy
 
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
equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Field Detail

storeRef

protected JmlStoreRefExpression storeRef
An AST for the storeRef expression of the more abstract variable in this.


specExpression

private JmlSpecExpression specExpression

predicate

private JmlPredicate predicate
Constructor Detail

JmlRepresentsDecl

public JmlRepresentsDecl(TokenReference where,
                         long modifiers,
                         boolean redundantly,
                         JmlStoreRefExpression storeRef,
                         JmlSpecExpression specExpression)
Creates a new JmlRepresentsDecl instance.

Parameters:
where - a TokenReference value
modifiers - modifier bit-mask
redundantly - true ==> this is a representsDecl_redundantly statement
storeRef - the model variable whose representation is being defined
specExpression - the abstract function that gives the value of storeRef based on its dependees

JmlRepresentsDecl

public JmlRepresentsDecl(TokenReference where,
                         long modifiers,
                         boolean redundantly,
                         JmlStoreRefExpression storeRef,
                         JmlPredicate predicate)
Creates a new JmlRepresentsDecl instance.

Parameters:
where - a TokenReference value
modifiers - modifier bit-mask
redundantly - true ==> this is a representsDecl_redundantly statement
storeRef - the model variable whose representation is being defined
predicate - the abstract relation that relates the value of storeRef to its dependees
Method Detail

storeRef

public JmlStoreRefExpression storeRef()
Returns the store ref expression of this represents declaration.


specExpression

public JmlSpecExpression specExpression()
Returns the spec expression of this represents declaration. If this declaration uses an abstraction relation, null is returned.


predicate

public JmlPredicate predicate()
Returns the predicate of this represents declaration. If this declaration uses an abstraction function, null is returned.


usesAbstractionFunction

public boolean usesAbstractionFunction()
Indicates whether this represents declaration uses an abstraction function.

 ensures \result <==> specExpression != null;
 


usesAbstractionRelation

public boolean usesAbstractionRelation()
Indicates whether this represents declaration uses an abstraction relations.

 ensures \result <==> predicate != null;
 


ident

public String ident()
Returns the identifier of the represented model field. This method can be called before typechecking. But to get the accurate result, one should call the getField method after typechecking.


getField

public JmlSourceField getField()
Returns the JmlSourceField of the model variable that this represents clause specifies for. This method must be called after typechecking.


typecheck

public void typecheck(CContextType context)
               throws PositionedError
Typechecks this depends/represents clause in the context in which it appears. The type checking rules for depends/represents clauses are defined as follows.

Parameters:
context - the context in which this type declaration appears
Throws:
PositionedError - if any checks fail

checkStoreRef

protected void checkStoreRef(JmlExpressionContext context)
                      throws PositionedError
Checks the store ref of this depends/represents clause. The store ref on the left-hand side must be type-correct and refer to a model field. If this clause is non-static, the store ref must refer to a non-static model field. For static, this clause must appear in the same class (interface) where the model field on the left-hand side is declared in. For non-static, this clause must appear in in a type descended from or nested in the type where the model field (on the left-hand side) is declared.

Throws:
PositionedError

checkRightHandSide

protected void checkRightHandSide(JmlExpressionContext context)
                           throws PositionedError
Performs type-checking of right-hand side of the represents clause. E.g., typechecks the right-hand side spec-expression (or predicate). For a functional abstraction form, the spec-expression must be assignment-compatible to the model field on the left-hand side.

Throws:
PositionedError

isInheritedOrOuter

protected static boolean isInheritedOrOuter(JClassFieldExpression field)
Returns true if the given field expression refers to a field declared in this class, inherited from a superclasse or interface, or defined in an outer class or interface.


accept

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

Overrides:
accept in class JmlDeclaration
Parameters:
p - the visitor

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.