JML

org.jmlspecs.jmlrac.qexpr
Class QSet

java.lang.Object
  extended byorg.jmlspecs.jmlrac.qexpr.QSet
All Implemented Interfaces:
Constants, Constants, Constants, RacConstants
Direct Known Subclasses:
QSet.Composite, QSet.Leaf, QSet.Top

abstract class QSet
extends Object
implements RacConstants

An abstract class that represetns qsets of quantified expressions. A qset of a quantified expression is a static, conservative, approximation of the set of all objects that need be examined to determine the truth of the quantified expression. To decide the truth of the quantified expression, each element of the qset is bound and the quantified expression is evaluated. The qset classes are organized with the Composite Pattern [GoF95].

  {abstract} QSet
  +- Top        ^
  +- Leaf       |left, right
  +- Composite -+
      +- Union
      +- Intersection
 


Nested Class Summary
private static class QSet.Composite
          An abstract qset class consisting of two other qset objects, e.g., union or intersection qsets.
private static class QSet.Intersection
          A concrete qset class representating a qset that is an intersection of two qsets.
private static class QSet.Leaf
          A concrete qset class consisting of only one JML expression.
private static class QSet.Top
          A special, concrete qset class that represents the universe of all objects.
private static class QSet.Union
          A concrete qset class representating a union of two qsets.
 
Field Summary
private static CClassType JAVA_COLLECTION
          Java collection type recognized in translating quantified expressions.
private static CClassType JML_COLLECTION
          JML model collection type recognized in translating quantified expressions.
static QSet TOP
           
 
Fields inherited from interface org.jmlspecs.jmlrac.RacConstants
MN_CHECK_HC, MN_CHECK_INV, MN_CHECK_POST, MN_CHECK_PRE, MN_CHECK_XPOST, MN_EVAL_OLD, MN_GHOST, MN_INIT, MN_INTERNAL, MN_MODEL, MN_MODEL_PUBLIC, MN_RESTORE_FROM, MN_SAVE_TO, MN_SPEC, MN_SPEC_PUBLIC, TN_JMLCHECKABLE, TN_JMLSURROGATE, TN_JMLUNIT_TEST_POSTFIX, TN_JMLUNIT_TESTDATA_POSTFIX, TN_JMLVALUE, TN_SURROGATE, VN_ASSERTION, VN_CATCH_VAR, VN_CLASS_INIT, VN_CONSTRUCTED, VN_DELEGEE, VN_ERROR_SET, VN_EXCEPTION, VN_FREE_VAR, VN_INIT, VN_OLD_VAR, VN_POST_VAR, VN_PRE_VAR, VN_PRECOND, VN_RAC_COMPILED, VN_RAC_LEVEL, VN_RESULT, VN_STACK_VAR, VN_XRESULT
 
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
(package private) QSet()
           
 
Method Summary
static QSet build(JExpression expr, String var)
          Returns a new qset built from a JML expression and a quantified variable.
private static QSet calculate(JExpression expr, String var)
          Returns the qset of an expression expr with respect to the quantified variable var.
private static QSet calculate(JMethodCallExpression expr, String var)
          Returns the qset of a method call expression expr with respect to the quantified variable var.
private static void initCollectionTypes()
          Initializes collection types such as java.lang.Collection and JMLCollection recognized in translating quantified expressions.
 QSet intersect(QSet s)
          Returns a qset representing the intersection of this and argument.
 boolean isTop()
          Is this a special qset TOP?
abstract  RacNode translate(VarGenerator varGen, String resultVar, AbstractExpressionTranslator transExp)
          Returns Java source code that computes the qset represented by this object.
 QSet union(QSet s)
          Returns a qset representing the union of this and argument.
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Field Detail

TOP

public static final QSet TOP

JAVA_COLLECTION

private static CClassType JAVA_COLLECTION
Java collection type recognized in translating quantified expressions.


JML_COLLECTION

private static CClassType JML_COLLECTION
JML model collection type recognized in translating quantified expressions.

Constructor Detail

QSet

QSet()
Method Detail

build

public static QSet build(JExpression expr,
                         String var)
                  throws NonExecutableQuantifierException
Returns a new qset built from a JML expression and a quantified variable.

Throws:
NonExecutableQuantifierException

union

public QSet union(QSet s)
Returns a qset representing the union of this and argument.


intersect

public QSet intersect(QSet s)
Returns a qset representing the intersection of this and argument.


isTop

public boolean isTop()
Is this a special qset TOP?


calculate

private static QSet calculate(JExpression expr,
                              String var)
                       throws NonExecutableQuantifierException
Returns the qset of an expression expr with respect to the quantified variable var. A qset for a quantified expression is a static, conservative, approximation of the set of all objects that need be examined to determine the truth of the quantified expression. To decide the truth of the quantified expression, each element of the qset is bound and the quantified expression is evaluated.

Parameters:
expr - the expression whose qset is being computed.
var - the name of the quantified variable with respect to it the qset is computed.
Returns:
the qset of the expression expr with repect to the quantified variable var.
  Q[[p && q]] == Q[[p]] intersect Q[[q]]
  Q[[p || q]] == Q[[p]] union Q[[q]]
  Q[[e.contains(x)]] == 
    e   if e is of type Collection and x equals to var.
    TOP otherwise
  Q[[ ... ]]  == TOP
 
Throws:
NonExecutableQuantifierException

calculate

private static QSet calculate(JMethodCallExpression expr,
                              String var)
Returns the qset of a method call expression expr with respect to the quantified variable var.

Parameters:
expr - the method call expression whose qset is being computed.
var - the name of the quantified variable with respect to it the qset is computed.
Returns:
the qset of the expression expr with repect to the quantified variable var.
  Q[[e.contains(x)]] == 
    e   if e is of type Collection and x equals to var.
    TOP otherwise
 

translate

public abstract RacNode translate(VarGenerator varGen,
                                  String resultVar,
                                  AbstractExpressionTranslator transExp)
                           throws NonExecutableQuantifierException
Returns Java source code that computes the qset represented by this object.

Parameters:
varGen - the variable generator to be used in the translation for generating unique local variables.
resultVar - the variable name to refer to the qset object in the translated code.
transExp - the translator to use for translating JML expressions.
Throws:
NonExecutableQuantifierException

initCollectionTypes

private static void initCollectionTypes()
Initializes collection types such as java.lang.Collection and JMLCollection recognized in translating quantified expressions.


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.