org.jmlspecs.jmlrac.qexpr
Class QSet

java.lang.Object
  org.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_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
(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, TransExpression 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.

QSet

QSet()

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