JML

org.jmlspecs.jmlrac
Class DesugarSpec

java.lang.Object
  extended byorg.multijava.util.Utils
      extended byorg.jmlspecs.checker.JmlAbstractVisitor
          extended byorg.jmlspecs.jmlrac.DesugarSpec
All Implemented Interfaces:
Cloneable, Constants, Constants, Constants, JmlVisitor, MjcVisitor

public class DesugarSpec
extends JmlAbstractVisitor
implements JmlVisitor

A JML visitor class for desugaring method specifications. In the desugared form, a generic specification, a normal behavior specification and a exceptional specification are all translated into a (general form of) behavior specification. A case-analysis specification, known as specification cases, and a nested specification are also desugared. The desugaring does not produce a completely desugared method specification, but a partial form sufficient for the further processing by the runtime assertion checker.

In the desugared specification, each specification case is translated into a general behavior specification case. If necessary, a default specification body clause such as ensures clause and signals clause is added. A specification cases specification is desugared by copying specificification variable declarations and specification headers into each specification case. A nested specification is desugared by unfolding the nesting. For example, the following specification:

  also requires p1; {| ensures p2; also ensures p3; |}
  also behavior ensures p4;
  also normal_behavior ensures p5;
  also exceptional_behavior signals (E e) p6;
 
is desugared into:
  also behavior requires p1; ensures p2;
  also behavior requires p1; ensures p3;
  also behavior ensures p4;
  also behavior ensures p5; signals (Exception e) false;
  also behavior signals (E e) p6; ensures false;
 


Field Summary
private  CClassType[] exceptions
          Exceptions that the target method may throw.
private  boolean heavyweight
          True iff the current specification being desugared is heavyweight.
private  Stack resultStack
          for passing results (return values) between visitor methods.
 
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
DesugarSpec()
          Constructs a new instance.
 
Method Summary
private  JmlGenericSpecCase add(JmlGenericSpecCase specCase, JmlSpecVarDecl[] specVarDecls, JmlRequiresClause[] specHeader)
          Adds the given spec var decls, specVarDecls, and spec header, specHeader, to the spec case, specCase.
private  JmlBehaviorSpec addDefaultRequiresClause(JmlBehaviorSpec bs)
          Adds a default requires clause to the given behaviorSpec, bs, and returns it.
protected  JmlEnsuresClause defaultEnsuresClause(TokenReference where)
          Returns a default ensures clause for an exceptional specification.
protected  JmlRequiresClause defaultRequiresClause(TokenReference where)
          Returns a default requires clause for an behavior spec case.
private  JmlSignalsClause defaultSignalsClause(TokenReference where)
          Returns a default signals clause for a normal specification.
private  JmlSignalsClause defaultSignalsClause(TokenReference where, CClassType[] exceptions)
          Returns a default signals clause for a lightweight specification whose method may throw the given exceptions.
private  Object GET_RESULT()
          Pops and returns the top element of the result stack.
 JmlMethodSpecification perform(JmlMethodSpecification mspec, CClassType[] exceptions)
          Returns a desugared specification of the given method specification.
private  void RETURN_RESULT(Object obj)
          Pushes the argument to the result stack.
private  void visitHeavyweightSpec(JmlHeavyweightSpec self)
          Desugars a general/normal/exceptional behavior specification.
 void visitJmlBehaviorSpec(JmlBehaviorSpec self)
          Desugars a behavior specification.
 void visitJmlExceptionalBehaviorSpec(JmlExceptionalBehaviorSpec self)
          Desugars an exceptional behavior specification.
 void visitJmlExceptionalSpecBody(JmlExceptionalSpecBody self)
          Desugars an exceptional specification body.
 void visitJmlExceptionalSpecCase(JmlExceptionalSpecCase self)
          Desugars an exceptional specification case.
 void visitJmlExtendingSpecification(JmlExtendingSpecification self)
          Desugar an extending specification.
 void visitJmlGenericSpecBody(JmlGenericSpecBody self)
          Desugars a generic specification body.
 void visitJmlGenericSpecCase(JmlGenericSpecCase self)
          Desugars a generic specification case.
 void visitJmlNormalBehaviorSpec(JmlNormalBehaviorSpec self)
          Desugars a normal behavior specification.
 void visitJmlNormalSpecBody(JmlNormalSpecBody self)
          Desugars a normal specification body.
 void visitJmlNormalSpecCase(JmlNormalSpecCase self)
          Desugars a normal specification case.
 void visitJmlSpecification(JmlSpecification self)
          Desugars the given JML specification.
private  void visitSpecBody(JmlSpecBody self, JmlSpecBodyClause body)
          Desugars a specification body (general, normal, exceptional).
private  void visitSpecCase(JmlGeneralSpecCase self)
          Desugars a specification case (general, normal, exceptional).
private  void visitSpecification(JmlSpecification self)
          Desugars a JML specification or an OR-extending specification.
 
Methods inherited from class org.jmlspecs.checker.JmlAbstractVisitor
visitAddExpression, visitArrayAccessExpression, visitArrayDimsAndInit, visitArrayInitializer, visitArrayLengthExpression, visitAssertStatement, visitAssignmentExpression, visitBinaryExpression, visitBitwiseExpression, visitBlockStatement, visitBooleanLiteral, visitBreakStatement, visitByteLiteral, visitCastExpression, visitCatchClause, visitCharLiteral, visitClassBlock, visitClassDeclaration, visitClassExpression, visitClassOrGFImport, visitCompilationUnit, visitCompoundAssignmentExpression, visitCompoundStatement, visitCompoundStatement, visitConditionalAndExpression, visitConditionalExpression, visitConditionalOrExpression, visitConstructorBlock, visitConstructorDeclaration, visitContinueStatement, visitDivideExpression, visitDoStatement, visitDoubleLiteral, visitEmptyStatement, visitEqualityExpression, visitExplicitConstructorInvocation, visitExpressionListStatement, visitExpressionStatement, visitFieldDeclaration, visitFieldExpression, visitFloatLiteral, visitFormalParameters, visitForStatement, visitGenericFunctionDecl, visitIfStatement, visitInitializerDeclaration, visitInstanceofExpression, visitInterfaceDeclaration, visitIntLiteral, visitJmlAbruptSpecBody, visitJmlAbruptSpecCase, visitJmlAccessibleClause, visitJmlAssertStatement, visitJmlAssignableClause, visitJmlAssignmentStatement, visitJmlAssumeStatement, visitJmlAxiom, visitJmlBreaksClause, visitJmlCallableClause, visitJmlCapturesClause, visitJmlClassBlock, visitJmlClassDeclaration, visitJmlClassOrGFImport, visitJmlCodeContract, visitJmlCompilationUnit, visitJmlConstraint, visitJmlConstructorDeclaration, visitJmlConstructorName, visitJmlContinuesClause, visitJmlDebugStatement, visitJmlDeclaration, visitJmlDivergesClause, visitJmlDurationClause, visitJmlDurationExpression, visitJmlElemTypeExpression, visitJmlEnsuresClause, visitJmlExample, visitJmlExceptionalExample, visitJmlExpression, visitJmlFieldDeclaration, visitJmlForAllVarDecl, visitJmlFormalParameter, visitJmlFreshExpression, visitJmlGeneralSpecCase, visitJmlGuardedStatement, visitJmlHenceByStatement, visitJmlInformalExpression, visitJmlInformalStoreRef, visitJmlInGroupClause, visitJmlInitiallyVarAssertion, visitJmlInterfaceDeclaration, visitJmlInvariant, visitJmlInvariantForExpression, visitJmlInvariantStatement, visitJmlIsInitializedExpression, visitJmlLabelExpression, visitJmlLetVarDecl, visitJmlLockSetExpression, visitJmlLoopInvariant, visitJmlLoopStatement, visitJmlMapsIntoClause, visitJmlMaxExpression, visitJmlMeasuredClause, visitJmlMethodDeclaration, visitJmlMethodName, visitJmlMethodNameList, visitJmlMethodSpecification, visitJmlModelProgram, visitJmlMonitorsForVarAssertion, visitJmlName, visitJmlNode, visitJmlNondetChoiceStatement, visitJmlNondetIfStatement, visitJmlNonNullElementsExpression, visitJmlNormalExample, visitJmlNotAssignedExpression, visitJmlNotModifiedExpression, visitJmlOldExpression, visitJmlOnlyAccessedExpression, visitJmlOnlyAssignedExpression, visitJmlOnlyCalledExpression, visitJmlOnlyCapturedExpression, visitJmlPackageImport, visitJmlPredicate, visitJmlPredicateKeyword, visitJmlPreExpression, visitJmlReachExpression, visitJmlReadableIfVarAssertion, visitJmlRedundantSpec, visitJmlRefinePrefix, visitJmlRelationalExpression, visitJmlRepresentsDecl, visitJmlRequiresClause, visitJmlResultExpression, visitJmlReturnsClause, visitJmlSetComprehension, visitJmlSetStatement, visitJmlSignalsClause, visitJmlSignalsOnlyClause, visitJmlSpaceExpression, visitJmlSpecBody, visitJmlSpecExpression, visitJmlSpecQuantifiedExpression, visitJmlSpecStatement, visitJmlSpecVarDecl, visitJmlStoreRef, visitJmlStoreRefExpression, visitJmlStoreRefKeyword, visitJmlTypeExpression, visitJmlTypeOfExpression, visitJmlUnreachableStatement, visitJmlVariableDefinition, visitJmlVariantFunction, visitJmlWhenClause, visitJmlWorkingSpaceClause, visitJmlWorkingSpaceExpression, visitJmlWritableIfVarAssertion, visitLabeledStatement, visitLocalVariableExpression, visitLongLiteral, visitMathModeExpression, visitMethodCallExpression, visitMethodDeclaration, visitMinusExpression, visitModuloExpression, visitMultExpression, visitNameExpression, visitNewAnonymousClassExpression, visitNewArrayExpression, visitNewObjectExpression, visitNullLiteral, visitOrdinalLiteral, visitPackageImport, visitPackageName, visitParenthesedExpression, visitPostfixExpression, visitPrefixExpression, visitRealLiteral, visitRelationalExpression, visitReturnStatement, visitShiftExpression, visitShortLiteral, visitStringLiteral, visitSuperExpression, visitSwitchGroup, visitSwitchLabel, visitSwitchStatement, visitSynchronizedStatement, visitThisExpression, visitThrowStatement, visitTopLevelMethodDeclaration, visitTryCatchStatement, visitTryFinallyStatement, visitTypeDeclarationStatement, visitTypeNameExpression, visitUnaryExpression, visitUnaryPromoteExpression, visitVariableDeclarationStatement, visitVariableDefinition, visitWarnExpression, visitWhileStatement
 
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.jmlspecs.checker.JmlVisitor
visitJmlAbruptSpecBody, visitJmlAbruptSpecCase, visitJmlAccessibleClause, visitJmlAssertStatement, visitJmlAssignableClause, visitJmlAssignmentStatement, visitJmlAssumeStatement, visitJmlAxiom, visitJmlBreaksClause, visitJmlCallableClause, visitJmlCapturesClause, visitJmlClassBlock, visitJmlClassDeclaration, visitJmlClassOrGFImport, visitJmlCodeContract, visitJmlCompilationUnit, visitJmlConstraint, visitJmlConstructorDeclaration, visitJmlConstructorName, visitJmlContinuesClause, visitJmlDebugStatement, visitJmlDeclaration, visitJmlDivergesClause, visitJmlDurationClause, visitJmlDurationExpression, visitJmlElemTypeExpression, visitJmlEnsuresClause, visitJmlExample, visitJmlExceptionalExample, visitJmlExpression, visitJmlFieldDeclaration, visitJmlForAllVarDecl, visitJmlFormalParameter, visitJmlFreshExpression, visitJmlGeneralSpecCase, visitJmlGuardedStatement, visitJmlHenceByStatement, visitJmlInformalExpression, visitJmlInformalStoreRef, visitJmlInGroupClause, visitJmlInitiallyVarAssertion, visitJmlInterfaceDeclaration, visitJmlInvariant, visitJmlInvariantForExpression, visitJmlInvariantStatement, visitJmlIsInitializedExpression, visitJmlLabelExpression, visitJmlLetVarDecl, visitJmlLockSetExpression, visitJmlLoopInvariant, visitJmlLoopStatement, visitJmlMapsIntoClause, visitJmlMaxExpression, visitJmlMeasuredClause, visitJmlMethodDeclaration, visitJmlMethodName, visitJmlMethodNameList, visitJmlMethodSpecification, visitJmlModelProgram, visitJmlMonitorsForVarAssertion, visitJmlName, visitJmlNode, visitJmlNondetChoiceStatement, visitJmlNondetIfStatement, visitJmlNonNullElementsExpression, visitJmlNormalExample, visitJmlNotAssignedExpression, visitJmlNotModifiedExpression, visitJmlOldExpression, visitJmlOnlyAccessedExpression, visitJmlOnlyAssignedExpression, visitJmlOnlyCalledExpression, visitJmlOnlyCapturedExpression, visitJmlPackageImport, visitJmlPredicate, visitJmlPredicateKeyword, visitJmlPreExpression, visitJmlReachExpression, visitJmlReadableIfVarAssertion, visitJmlRedundantSpec, visitJmlRefinePrefix, visitJmlRelationalExpression, visitJmlRepresentsDecl, visitJmlRequiresClause, visitJmlResultExpression, visitJmlReturnsClause, visitJmlSetComprehension, visitJmlSetStatement, visitJmlSignalsClause, visitJmlSignalsOnlyClause, visitJmlSpaceExpression, visitJmlSpecBody, visitJmlSpecExpression, visitJmlSpecQuantifiedExpression, visitJmlSpecStatement, visitJmlSpecVarDecl, visitJmlStoreRef, visitJmlStoreRefExpression, visitJmlStoreRefKeyword, visitJmlTypeExpression, visitJmlTypeOfExpression, visitJmlUnreachableStatement, visitJmlVariableDefinition, visitJmlVariantFunction, visitJmlWhenClause, visitJmlWorkingSpaceClause, visitJmlWorkingSpaceExpression, visitJmlWritableIfVarAssertion
 
Methods inherited from interface org.multijava.mjc.MjcVisitor
visitAddExpression, visitArrayAccessExpression, visitArrayDimsAndInit, visitArrayInitializer, visitArrayLengthExpression, visitAssertStatement, visitAssignmentExpression, visitBitwiseExpression, visitBlockStatement, visitBooleanLiteral, visitBreakStatement, visitCastExpression, visitCatchClause, visitCharLiteral, visitClassBlock, visitClassDeclaration, visitClassExpression, visitClassOrGFImport, visitCompilationUnit, visitCompoundAssignmentExpression, visitCompoundStatement, visitConditionalAndExpression, visitConditionalExpression, visitConditionalOrExpression, visitConstructorBlock, visitConstructorDeclaration, visitContinueStatement, visitDivideExpression, visitDoStatement, visitEmptyStatement, visitEqualityExpression, visitExplicitConstructorInvocation, visitExpressionListStatement, visitExpressionStatement, visitFieldDeclaration, visitFieldExpression, visitFormalParameters, visitForStatement, visitGenericFunctionDecl, visitIfStatement, visitInitializerDeclaration, visitInstanceofExpression, visitInterfaceDeclaration, visitLabeledStatement, visitLocalVariableExpression, visitMathModeExpression, visitMethodCallExpression, visitMethodDeclaration, visitMinusExpression, visitModuloExpression, visitMultExpression, visitNameExpression, visitNewAnonymousClassExpression, visitNewArrayExpression, visitNewObjectExpression, visitNullLiteral, visitOrdinalLiteral, visitPackageImport, visitPackageName, visitParenthesedExpression, visitPostfixExpression, visitPrefixExpression, visitRealLiteral, visitRelationalExpression, visitReturnStatement, visitShiftExpression, visitStringLiteral, visitSuperExpression, visitSwitchGroup, visitSwitchLabel, visitSwitchStatement, visitSynchronizedStatement, visitThisExpression, visitThrowStatement, visitTopLevelMethodDeclaration, visitTryCatchStatement, visitTryFinallyStatement, visitTypeDeclarationStatement, visitTypeNameExpression, visitUnaryExpression, visitUnaryPromoteExpression, visitVariableDeclarationStatement, visitVariableDefinition, visitWarnExpression, visitWhileStatement
 

Field Detail

resultStack

private Stack resultStack
for passing results (return values) between visitor methods.

See Also:
GET_RESULT(), RETURN_RESULT(Object)

exceptions

private CClassType[] exceptions
Exceptions that the target method may throw.


heavyweight

private boolean heavyweight
True iff the current specification being desugared is heavyweight.

Constructor Detail

DesugarSpec

public DesugarSpec()
Constructs a new instance.

Method Detail

perform

public JmlMethodSpecification perform(JmlMethodSpecification mspec,
                                      CClassType[] exceptions)
Returns a desugared specification of the given method specification.

Parameters:
mspec - the method specification to be desugared
exceptions - exceptions that the target method may throw.
Returns:
the desugared method specification
See Also:
visitJmlSpecification(JmlSpecification)

visitJmlSpecification

public void visitJmlSpecification(JmlSpecification self)
Desugars the given JML specification. In the desugared specification, each specification case is translated into a general behavior specification case. A default specification body clause such as ensures clause and signals clause is added if necessary. A specification cases specification is desugared by copying specificification variable declarations and specification headers into each specification case. A nested specification is desugared by unfolding the nesting. For example, the following specification:
  also requires p1; {| ensures p2; also ensures p3; |}
  also behavior ensures p4;
  also normal_behavior ensures p5;
  also exceptional_behavior signals (E e) p6;
 
is desugared into:
  also behavior requires p1; ensures p2;
  also behavior requires p1; ensures p3;
  also behavior ensures p4;
  also behavior ensures p5; signals (Exception e) false;
  also behavior signals (E e) p6; ensures false;
 
Both the subclassing contract and redundant specifications are not desugared.

 also
   requires self != null && resultStack != null;
   assignable resultStack;
   ensures resultStack.size() == \old(resultStack.size() + 1);
 

Specified by:
visitJmlSpecification in interface JmlVisitor
Overrides:
visitJmlSpecification in class JmlAbstractVisitor

visitSpecification

private void visitSpecification(JmlSpecification self)
Desugars a JML specification or an OR-extending specification.

 requires self != null && resultStack != null;
 requires (self instanceof JmlSpecification) ||
    (* self is an OR-extending specification *);
 assignable resultStack;
 ensures resultStack.size() == \old(resultStack.size() + 1);
 


addDefaultRequiresClause

private JmlBehaviorSpec addDefaultRequiresClause(JmlBehaviorSpec bs)
Adds a default requires clause to the given behaviorSpec, bs, and returns it.


visitJmlExtendingSpecification

public void visitJmlExtendingSpecification(JmlExtendingSpecification self)
Desugar an extending specification. In the desugared specification, each conjoinable specification is translated into a corresponding behavior conjoinable specification, if necssary, with a default specification body clause added. For example, the method specification of:
  and ensures p1; 
  and behavior ensures p2;
  and normal_behavior ensures p3;
  and exceptional_behavior signals (E e) p4;
 
is desugared into:
  and behavior ensures p1;
  and behavior ensures p2;
  and behavior ensures p3; signals (Exception e) false;
  and behavior signals (E e) p4; ensures false;
 
Redundant specifications are not desugared.

 also
   requires self != null && resultStack != null;
   assignable resultStack;
   ensures resultStack.size() == \old(resultStack.size() + 1);
 

Specified by:
visitJmlExtendingSpecification in interface JmlVisitor
Overrides:
visitJmlExtendingSpecification in class JmlAbstractVisitor

visitJmlBehaviorSpec

public void visitJmlBehaviorSpec(JmlBehaviorSpec self)
Desugars a behavior specification.

 also
   requires self != null && resultStack != null;
   assignable resultStack;
   ensures resultStack.size() == \old(resultStack.size() + 1);
 

Specified by:
visitJmlBehaviorSpec in interface JmlVisitor
Overrides:
visitJmlBehaviorSpec in class JmlAbstractVisitor

visitJmlNormalBehaviorSpec

public void visitJmlNormalBehaviorSpec(JmlNormalBehaviorSpec self)
Desugars a normal behavior specification.

 also
   requires self != null && resultStack != null;
   assignable resultStack;
   ensures resultStack.size() == \old(resultStack.size() + 1);
 

Specified by:
visitJmlNormalBehaviorSpec in interface JmlVisitor
Overrides:
visitJmlNormalBehaviorSpec in class JmlAbstractVisitor

visitJmlExceptionalBehaviorSpec

public void visitJmlExceptionalBehaviorSpec(JmlExceptionalBehaviorSpec self)
Desugars an exceptional behavior specification.

 also
   requires self != null && resultStack != null;
   assignable resultStack;
   ensures resultStack.size() == \old(resultStack.size() + 1);
 

Specified by:
visitJmlExceptionalBehaviorSpec in interface JmlVisitor
Overrides:
visitJmlExceptionalBehaviorSpec in class JmlAbstractVisitor

visitJmlGenericSpecCase

public void visitJmlGenericSpecCase(JmlGenericSpecCase self)
Desugars a generic specification case.

 also
   requires self != null && resultStack != null;
   assignable resultStack;
   ensures resultStack.size() == \old(resultStack.size() + 1);
 

Specified by:
visitJmlGenericSpecCase in interface JmlVisitor
Overrides:
visitJmlGenericSpecCase in class JmlAbstractVisitor

visitJmlGenericSpecBody

public void visitJmlGenericSpecBody(JmlGenericSpecBody self)
Desugars a generic specification body.

 also
   requires self != null && resultStack != null;
   assignable resultStack;
   ensures resultStack.size() == \old(resultStack.size() + 1);
 

Specified by:
visitJmlGenericSpecBody in interface JmlVisitor
Overrides:
visitJmlGenericSpecBody in class JmlAbstractVisitor

visitJmlNormalSpecCase

public void visitJmlNormalSpecCase(JmlNormalSpecCase self)
Desugars a normal specification case.

 also
   requires self != null && resultStack != null;
   assignable resultStack;
   ensures resultStack.size() == \old(resultStack.size() + 1);
 

Specified by:
visitJmlNormalSpecCase in interface JmlVisitor
Overrides:
visitJmlNormalSpecCase in class JmlAbstractVisitor

visitJmlNormalSpecBody

public void visitJmlNormalSpecBody(JmlNormalSpecBody self)
Desugars a normal specification body.

 also
   requires self != null && resultStack != null;
   assignable resultStack;
   ensures resultStack.size() == \old(resultStack.size() + 1);
 

Specified by:
visitJmlNormalSpecBody in interface JmlVisitor
Overrides:
visitJmlNormalSpecBody in class JmlAbstractVisitor

visitJmlExceptionalSpecCase

public void visitJmlExceptionalSpecCase(JmlExceptionalSpecCase self)
Desugars an exceptional specification case.

 also
   requires self != null && resultStack != null;
   assignable resultStack;
   ensures resultStack.size() == \old(resultStack.size() + 1);
 

Specified by:
visitJmlExceptionalSpecCase in interface JmlVisitor
Overrides:
visitJmlExceptionalSpecCase in class JmlAbstractVisitor

visitJmlExceptionalSpecBody

public void visitJmlExceptionalSpecBody(JmlExceptionalSpecBody self)
Desugars an exceptional specification body.

 also
   requires self != null && resultStack != null;
   assignable resultStack;
   ensures resultStack.size() == \old(resultStack.size() + 1);
 

Specified by:
visitJmlExceptionalSpecBody in interface JmlVisitor
Overrides:
visitJmlExceptionalSpecBody in class JmlAbstractVisitor

visitHeavyweightSpec

private void visitHeavyweightSpec(JmlHeavyweightSpec self)
Desugars a general/normal/exceptional behavior specification.

 requires self != null && resultStack != null;
 assignable resultStack;
 assignable_redundantly heavyweight;
 ensures resultStack.size() == \old(resultStack.size() + 1);
 


defaultRequiresClause

protected JmlRequiresClause defaultRequiresClause(TokenReference where)
Returns a default requires clause for an behavior spec case.

 requires where != null;
 ensures \result != null;
 


defaultSignalsClause

private JmlSignalsClause defaultSignalsClause(TokenReference where)
Returns a default signals clause for a normal specification. The returned signals clause has the form: signals (Exception e) false.

 requires where != null;
 ensures \result != null;
 


defaultSignalsClause

private JmlSignalsClause defaultSignalsClause(TokenReference where,
                                              CClassType[] exceptions)
Returns a default signals clause for a lightweight specification whose method may throw the given exceptions. The returned signals clause has the form:
  signals (Throwable e) e instanceof E1 || ... || e instanceof En;
 


defaultEnsuresClause

protected JmlEnsuresClause defaultEnsuresClause(TokenReference where)
Returns a default ensures clause for an exceptional specification.

 requires where != null;
 ensures \result != null;
 


visitSpecCase

private void visitSpecCase(JmlGeneralSpecCase self)
Desugars a specification case (general, normal, exceptional).

 requires self != null && resultStack != null;
 assignable resultStack;
 ensures resultStack.size() == \old(resultStack.size() + 1);
 


visitSpecBody

private void visitSpecBody(JmlSpecBody self,
                           JmlSpecBodyClause body)
Desugars a specification body (general, normal, exceptional).

 requires self != null && resultStack != null;
 assignable resultStack;
 ensures resultStack.size() == \old(resultStack.size() + 1);
 


add

private JmlGenericSpecCase add(JmlGenericSpecCase specCase,
                               JmlSpecVarDecl[] specVarDecls,
                               JmlRequiresClause[] specHeader)
Adds the given spec var decls, specVarDecls, and spec header, specHeader, to the spec case, specCase.


GET_RESULT

private Object GET_RESULT()
Pops and returns the top element of the result stack.

 requires resultStack != null;
 assignable resultStack;
 ensures resultStack != null;
 


RETURN_RESULT

private void RETURN_RESULT(Object obj)
Pushes the argument to the result stack.

 requires obj != null && resultStack != null;
 assignable resultStack;
 ensures resultStack != null;
 


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.