Overview  Package   Class  Use  Tree  Deprecated  Index  Help 
JML
 PREV CLASS   NEXT CLASS FRAMES    NO FRAMES    
SUMMARY: NESTED | FIELD | CONSTR | METHOD DETAIL: FIELD | CONSTR | METHOD

org.jmlspecs.jmlrac
Class RacPrettyPrinter

java.lang.Object
  extended byorg.multijava.util.Utils
      extended byorg.multijava.mjc.MjcPrettyPrinter
          extended byorg.jmlspecs.jmlrac.RacPrettyPrinter
All Implemented Interfaces:
Cloneable, Constants, Constants, Constants, JmlVisitor, MjcVisitor, RacConstants, RacVisitor
Direct Known Subclasses:
OrigPrettyPrinter, WrapperPrettyPrinter
public class RacPrettyPrinter
extends MjcPrettyPrinter
implements RacVisitor

A visitor class for pretty-printing JML specifications with generated RAC code. Each node of AST is visited and printed to an external file or writer object.

Approach to printing JML specifications. The problem is that some JML annotations such as non_null should be printed context-sensitively depending on their surrounding environment. For example, if a non_null annotation appears in a Java field declaration, it should be printed inside a pair of JML annotation markers, e.g., 

  private /*@ non_null @*/ HashSet elems;
However, if it appears in a model field declaration, it should be printed without the surrounding JML annotation markers, e.g. 
  //@ private model non_null JMLObjectSet elems;
To handle this, we use a flag variable isAnnotation and the class JmlModifier to indicate the context of printing. JML annotation ASTs such as those for non_null annotations can print themselves correctly by refering to the flag. The class JmlModifier, which returns a string corresponding to a modifier, produces a JML modifier without enclosing JML annotation markers if indicated as such using the method setWithoutMarkers; by default, a JML modifier is returned with annotation markers. A top-level JML specification AST such as a model field declaration is responsible for setting and clearing the isAnnotation flag (e.g., by using mayStartAnnotation and mayEndAnnotation, and directing the return form to the class JmlModifier.

It is the convention that each AST node, if necessary, advances to the next line before printing its code.

Model programs and specification statements are not implemented yet.

Version:
$Revision: 1.75 $
Author:
Yoonsik Cheon
See Also:
JmlModifier, JmlModifier.withoutMarkers(), JmlModifier.setWithoutMarkers(boolean)

Field Summary
private  int annotationDepth
          the depth of annotations.
private  int atMarkerPos
          the column number where annotation markers were written.
private  boolean inAnnotation
          indicates if currently printing inside a JML annotation marker.
private  JmlModifier jmlModUtil
          Modifier utility to manipulating modifiers, e.g., to get string representations of modifiers from bit mask encoding.
static String NEW_LINE
           
protected  int offset
          the space from '@' to the current print position for specification.
 
Fields inherited from class org.multijava.mjc.MjcPrettyPrinter
forInit, modUtil, nl, p, pos, TAB_SIZE, WIDTH
 
Fields inherited from class org.multijava.util.Utils
DBG_LEVEL_HIGH, DBG_LEVEL_LOW, DBG_LEVEL_NO
 
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
RacPrettyPrinter(File file, JmlModifier modUtil)
          Constructs a pretty printer object for JML specifications
RacPrettyPrinter(Writer writer, JmlModifier modUtil)
          Constructs a pretty printer object for JML specifications
RacPrettyPrinter(String fileName, JmlModifier modUtil)
          Constructs a pretty printer object for JML specifications
RacPrettyPrinter(TabbedPrintWriter writer)
          Constructs a pretty printer object for JML specifications
 
Method Summary
protected  void acceptAll(JPhylum[] all)
          Visits each element of the argument.
protected  void applyBinaryExpression(JExpression left, JExpression right, String oper)
          prints a binary expression with the given operator and binary exps.
 void close()
          Close the stream at the end
protected  void mayEndAnnotation()
          Stops the annotation printing mode if currently in that mode; also prints the closing annotation marker @*/.
protected  void mayEndAnnotation(boolean flag)
          Stops the annotation printing mode if the flag is true and currently in the annotation mode; also prints the closing annotation marker @*/.
protected  void mayStartAnnotation()
          Starts the annotation printing mode if not already in; also prints the opening annotation marker /*@.
protected  void mayStartAnnotation(boolean flag)
          Starts the annotation printing mode if flag is true and not already in the annotation mode; also prints the opening annotation marker /*@.
protected  void newLine()
          Prints a new line marker.
protected  void newLineOffset()
          Prints a new line marker.
protected  void print(String s)
          Prints a string.
protected  void print(CType t)
          Prints a type.
protected  void printJml(String s)
          Prints a string enclosed in the JML annotation markers.
protected  void println(String code)
          Prints multi-lined code with proper line-breaking and indentation.
private  void printVariableDefinition(JVariableDefinition self, boolean typeAndMod)
          Prints the given variable definition, self.
protected  String toString(CType type)
          Returns the string for the given type.
 void visitArrayAccessExpression(JArrayAccessExpression self)
          prints an array length expression
protected  void visitBigintLiteral(long value)
          Translates a \bigint literal.
protected  void visitBinaryExpression(JBinaryExpression self, String oper)
          prints a binary expression with the given operator
 void visitBitwiseExpression(JBitwiseExpression self)
          prints a bitwise expression
 void visitCastExpression(JCastExpression self)
          Prints a cast expression.
 void visitCharLiteral(JCharLiteral self)
          Prints a character literal.
protected  void visitClassBody(JmlTypeDeclaration self)
          Prints a JML type declaration.
 void visitCompilationUnit(JCompilationUnit self)
          Prints a compilation unit.
 void visitCompoundAssignmentExpression(JCompoundAssignmentExpression self)
          prints a compound assignment expression
protected  void visitDoubleLiteral(double value)
          Prints a double literal.
 void visitEqualityExpression(JEqualityExpression self)
          prints an equality expression
protected  void visitExample(JmlExample self)
          Prints example specifications.
 void visitFieldExpression(JClassFieldExpression self)
          prints a field expression, if it's not a model field then invoke the method in super class
protected  void visitFloatLiteral(float value)
          Prints a float literal.
 void visitFormalParameters(JFormalParameter self)
          visits a formal parameter
 void visitGeneralSpecCase(JmlGeneralSpecCase self)
          Prints the given general spec case.
 void visitJmlAbruptSpecBody(JmlAbruptSpecBody self)
          Prints a JML abrupt spec body.
 void visitJmlAbruptSpecCase(JmlAbruptSpecCase self)
          Prints a JML abrupt spec case.
 void visitJmlAccessibleClause(JmlAccessibleClause self)
          Prints a JML accessible clause.
 void visitJmlAssertStatement(JmlAssertStatement self)
          Prints a JML assignable clause.
 void visitJmlAssignableClause(JmlAssignableClause self)
          Prints a JML assignable clause.
 void visitJmlAssignmentStatement(JmlAssignmentStatement self)
           
 void visitJmlAssumeStatement(JmlAssumeStatement self)
          Prints a JML assume statement.
 void visitJmlAxiom(JmlAxiom self)
          Prints a JML axim.
 void visitJmlBehaviorSpec(JmlBehaviorSpec self)
          Prints a JML behavior spec.
 void visitJmlBreaksClause(JmlBreaksClause self)
          Prints a JML break clause.
 void visitJmlCallableClause(JmlCallableClause self)
          Prints a JML callable clause.
 void visitJmlCapturesClause(JmlCapturesClause self)
          Prints a JML captures clause.
 void visitJmlClassBlock(JmlClassBlock self)
          Prints static or instance initializer
 void visitJmlClassDeclaration(JmlClassDeclaration self)
          Prints a JML class declaration.
 void visitJmlClassOrGFImport(JmlClassOrGFImport self)
          Prints a JML classOrGFImport clause.
 void visitJmlCodeContract(JmlCodeContract self)
          Prints a JML code contract.
 void visitJmlCompilationUnit(JmlCompilationUnit self)
          Prints a JML compilation unit.
 void visitJmlConstraint(JmlConstraint self)
          Prints a JML constraint clause.
 void visitJmlConstructorDeclaration(JmlConstructorDeclaration self)
          Prints a JML constructor declaration.
 void visitJmlConstructorName(JmlConstructorName self)
          Prints a JML constructor name.
 void visitJmlContinuesClause(JmlContinuesClause self)
          Prints a JML continues statement.
 void visitJmlDebugStatement(JmlDebugStatement self)
          Prints a JML debug statement.
 void visitJmlDeclaration(JmlDeclaration self)
           
 void visitJmlDivergesClause(JmlDivergesClause self)
          Prints a JML diverges clause.
 void visitJmlDurationClause(JmlDurationClause self)
          Prints a JML duration clause.
 void visitJmlDurationExpression(JmlDurationExpression self)
          Prints a JML \duration expression.
 void visitJmlElemTypeExpression(JmlElemTypeExpression self)
          Prints a JML elemtype expression.
 void visitJmlEnsuresClause(JmlEnsuresClause self)
          Prints a JML ensures clause.
 void visitJmlExample(JmlExample self)
          Prints a JML example.
 void visitJmlExceptionalBehaviorSpec(JmlExceptionalBehaviorSpec self)
          Prints a JML exceptional behavior specification.
 void visitJmlExceptionalExample(JmlExceptionalExample self)
          Prints a JML exceptional example.
 void visitJmlExceptionalSpecBody(JmlExceptionalSpecBody self)
          Prints a JML exceptional spec body.
 void visitJmlExceptionalSpecCase(JmlExceptionalSpecCase self)
          Prints a JML exceptional spec case.
 void visitJmlExpression(JmlExpression self)
           
 void visitJmlExtendingSpecification(JmlExtendingSpecification self)
          Prints a JML method extending specification.
 void visitJmlFieldDeclaration(JmlFieldDeclaration self)
          Prints the given JML field declaration.
 void visitJmlForAllVarDecl(JmlForAllVarDecl self)
          Prints a JML forall variable declaration.
 void visitJmlFormalParameter(JmlFormalParameter self)
          Prints a JML formal parameter.
 void visitJmlFreshExpression(JmlFreshExpression self)
          Prints a JML fresh expression.
 void visitJmlGeneralSpecCase(JmlGeneralSpecCase self)
           
 void visitJmlGenericSpecBody(JmlGenericSpecBody self)
          Prints a JML generic spec body.
 void visitJmlGenericSpecCase(JmlGenericSpecCase self)
          Prints a JML generic spec case.
 void visitJmlGuardedStatement(JmlGuardedStatement self)
          Prints a JML guarded statement.
 void visitJmlHenceByStatement(JmlHenceByStatement self)
          Prints a JML henceby statement.
 void visitJmlInformalExpression(JmlInformalExpression self)
          Prints a JML informal expression.
 void visitJmlInformalStoreRef(JmlInformalStoreRef self)
          Prints a JML informal store reference.
 void visitJmlInGroupClause(JmlInGroupClause self)
          Prints a JML in data group clause.
 void visitJmlInitiallyVarAssertion(JmlInitiallyVarAssertion self)
          Prints a JML initially variable assertion.
 void visitJmlInterfaceDeclaration(JmlInterfaceDeclaration self)
          Prints a JML interface declaration.
 void visitJmlInvariant(JmlInvariant self)
          Prints a JML invariant.
 void visitJmlInvariantForExpression(JmlInvariantForExpression self)
          Prints a JML invariant for expression.
 void visitJmlInvariantStatement(JmlInvariantStatement self)
          Prints a JML invariant statement.
 void visitJmlIsInitializedExpression(JmlIsInitializedExpression self)
          Prints a JML isinitialized expression.
 void visitJmlLabelExpression(JmlLabelExpression self)
          Prints a JML label expression.
 void visitJmlLetVarDecl(JmlLetVarDecl self)
          Prints a JML old variable declaration.
 void visitJmlLockSetExpression(JmlLockSetExpression self)
          Prints a JML lockset expression.
 void visitJmlLoopInvariant(JmlLoopInvariant self)
          Prints a JML loop invariant.
 void visitJmlLoopStatement(JmlLoopStatement self)
          Prints a JML loop statement.
 void visitJmlMapsIntoClause(JmlMapsIntoClause self)
          Prints a JML maps into data group clause.
 void visitJmlMaxExpression(JmlMaxExpression self)
          Prints a JML \max expression.
 void visitJmlMeasuredClause(JmlMeasuredClause self)
          Prints a JML measured clause.
 void visitJmlMethodDeclaration(JmlMethodDeclaration self)
          Prints a JML method declaration.
 void visitJmlMethodName(JmlMethodName self)
          Prints a JML method name.
 void visitJmlMethodNameList(JmlMethodNameList self)
           
 void visitJmlMethodSpecification(JmlMethodSpecification self)
           
 void visitJmlModelProgram(JmlModelProgram self)
          Prints a JML model program.
 void visitJmlMonitorsForVarAssertion(JmlMonitorsForVarAssertion self)
          Prints a JML MonitorsFor variable assertion.
 void visitJmlName(JmlName self)
          Prints a JML name.
 void visitJmlNode(JmlNode self)
           
 void visitJmlNondetChoiceStatement(JmlNondetChoiceStatement self)
          Prints a JML nondeterministic choice statement.
 void visitJmlNondetIfStatement(JmlNondetIfStatement self)
          Prints a JML nondeterministic if statement.
 void visitJmlNonNullElementsExpression(JmlNonNullElementsExpression self)
          Prints a JML \nonnullelements expression.
 void visitJmlNormalBehaviorSpec(JmlNormalBehaviorSpec self)
          Prints a JML normal behavior specification.
 void visitJmlNormalExample(JmlNormalExample self)
          Prints a JML normal example.
 void visitJmlNormalSpecBody(JmlNormalSpecBody self)
          Prints a JML normal spec body.
 void visitJmlNormalSpecCase(JmlNormalSpecCase self)
          Prints a JML normal spec case.
 void visitJmlNotAssignedExpression(JmlNotAssignedExpression self)
          Prints a JML \not_assigned expression.
 void visitJmlNotModifiedExpression(JmlNotModifiedExpression self)
          Prints a JML \not_modified expression.
 void visitJmlOldExpression(JmlOldExpression self)
          Prints a JML \old expression.
 void visitJmlOnlyAccessedExpression(JmlOnlyAccessedExpression self)
          Prints a JML \only_accessed expression.
 void visitJmlOnlyAssignedExpression(JmlOnlyAssignedExpression self)
          Prints a JML \only_assigned expression.
 void visitJmlOnlyCalledExpression(JmlOnlyCalledExpression self)
          Prints a JML \only_called expression.
 void visitJmlOnlyCapturedExpression(JmlOnlyCapturedExpression self)
          Prints a JML \only_captured expression.
 void visitJmlPackageImport(JmlPackageImport self)
          Prints a JML package import statement.
 void visitJmlPredicate(JmlPredicate self)
          Prints a JML predicate.
 void visitJmlPredicateKeyword(JmlPredicateKeyword self)
           
 void visitJmlPreExpression(JmlPreExpression self)
          Prints a JML \pre expression.
 void visitJmlReachExpression(JmlReachExpression self)
          Prints a JML reach expression.
 void visitJmlReadableIfVarAssertion(JmlReadableIfVarAssertion self)
          Prints a JML readableif variable assertion.
 void visitJmlRedundantSpec(JmlRedundantSpec self)
          Prints a JML redundant specifications including implies_that and for_example.
 void visitJmlRefinePrefix(JmlRefinePrefix self)
          Prints a JML refine prefix.
 void visitJmlRelationalExpression(JmlRelationalExpression self)
          Prints a JML relational expression.
 void visitJmlRepresentsDecl(JmlRepresentsDecl self)
          Prints a JML represents declaration.
 void visitJmlRequiresClause(JmlRequiresClause self)
          Prints a JML requires clause.
 void visitJmlResultExpression(JmlResultExpression self)
          Prints a JML \result expression.
 void visitJmlReturnsClause(JmlReturnsClause self)
          Prints a JML return clause.
 void visitJmlSetComprehension(JmlSetComprehension self)
          Prints a JML set comprehension expression.
 void visitJmlSetStatement(JmlSetStatement self)
          Prints the given JML set statement.
 void visitJmlSignalsClause(JmlSignalsClause self)
          Prints a JML signals clause
 void visitJmlSignalsOnlyClause(JmlSignalsOnlyClause self)
          Prints a JML signals_only clause
 void visitJmlSpaceExpression(JmlSpaceExpression self)
          Prints a JML \space expression.
 void visitJmlSpecBody(JmlSpecBody self)
           
 void visitJmlSpecExpression(JmlSpecExpression self)
          Prints a JML specification expression.
 void visitJmlSpecification(JmlSpecification self)
          Prints a JML specification.
 void visitJmlSpecQuantifiedExpression(JmlSpecQuantifiedExpression self)
          Prints a JML specification quantified expression.
 void visitJmlSpecStatement(JmlSpecStatement self)
          Prints a JML specification statement.
 void visitJmlSpecVarDecl(JmlSpecVarDecl self)
           
 void visitJmlStoreRef(JmlStoreRef self)
           
 void visitJmlStoreRefExpression(JmlStoreRefExpression self)
          Prints a JML store reference expression.
 void visitJmlStoreRefKeyword(JmlStoreRefKeyword self)
          Prints a JML store reference keywords such as \everything, \nothing, and \not_specified.
 void visitJmlStoreRefListWrapper(JmlStoreRefListWrapper self)
           
 void visitJmlTypeExpression(JmlTypeExpression self)
          Prints a JML \type expression.
 void visitJmlTypeOfExpression(JmlTypeOfExpression self)
          Prints a JML \typeof expression.
 void visitJmlUnreachableStatement(JmlUnreachableStatement self)
          Prints a JML unreachable statement.
 void visitJmlVariableDefinition(JmlVariableDefinition self)
          Prints a JML variable declaration.
 void visitJmlVariantFunction(JmlVariantFunction self)
          Prints a JML variant function.
 void visitJmlWhenClause(JmlWhenClause self)
          Prints a JML when clause.
 void visitJmlWorkingSpaceClause(JmlWorkingSpaceClause self)
          Prints a JML working space clause.
 void visitJmlWorkingSpaceExpression(JmlWorkingSpaceExpression self)
          Prints a JML \working_space expression.
 void visitJmlWritableIfVarAssertion(JmlWritableIfVarAssertion self)
           
private  void visitMethodSpecification(JmlSpecification self)
          Prints a JML method extending specification.
 void visitNewArrayExpression(JNewArrayExpression self)
          Prints an array allocator expression.
 void visitNewObjectExpression(JNewObjectExpression self)
          Prints an object allocator expression.
 void visitOrdinalLiteral(JOrdinalLiteral self)
          Prints an ordinal literal.
 void visitPostfixExpression(JPostfixExpression self)
          prints a postfix expression
 void visitPrefixExpression(JPrefixExpression self)
          prints a prefix expression
 void visitRacJmlMethodDeclaration(JmlMethodDeclaration self)
          Prints a JML method declaration in Racc.
 void visitRacNode(RacNode self)
          Prints a given RacNode.
 void visitRacPredicate(RacPredicate self)
          Prints a RAC predicate.
 void visitShiftExpression(JShiftExpression self)
          prints a shift expression
protected  void visitSpecBody(JmlSpecBody self)
          Prints specification body.
 void visitSpecBodyClause(JmlPredicateClause self, String keyword)
          Prints specfication body clause.
protected  void visitSpecCases(JmlSpecCase[] specCases)
          Prints spec cases.
 void visitUnaryExpression(JUnaryExpression self)
          prints an unary expression
 void visitUnaryPromoteExpression(JUnaryPromote self)
          prints a unaryPrompte expression
private  void visitVarDecls(JVariableDefinition[] varDefs)
          Prints a Java variable delcaration.
 void visitVariableDeclarationStatement(JVariableDeclarationStatement self)
          prints a variable declaration statement
 
Methods inherited from class org.multijava.mjc.MjcPrettyPrinter
acceptAll, print, print, print, print, print, printClassModifiers, printInterfaceModifiers, setPos, visitAddExpression, visitArgs, visitArrayDimsAndInit, visitArrayInitializer, visitArrayLengthExpression, visitAssertStatement, visitAssignmentExpression, visitBlockStatement, visitBooleanLiteral, visitBreakStatement, visitByteLiteral, visitCatchClause, visitClassBlock, visitClassBody, visitClassDeclaration, visitClassExpression, visitClassOrGFImport, visitComment, visitComments, visitCompoundStatement, visitCompoundStatement, visitConditionalAndExpression, visitConditionalExpression, visitConditionalOrExpression, visitConstructorBlock, visitConstructorDeclaration, visitContinueStatement, visitDivideExpression, visitDoStatement, visitEmptyStatement, visitExplicitConstructorInvocation, visitExpressionListStatement, visitExpressionStatement, visitFieldDeclaration, visitForStatement, visitGenericFunctionDecl, visitIfStatement, visitInitializerDeclaration, visitInstanceofExpression, visitInterfaceBody, visitInterfaceDeclaration, visitIntLiteral, visitJavadoc, visitLabeledStatement, visitLocalVariableExpression, visitLongLiteral, visitMathModeExpression, visitMethodCallExpression, visitMethodDeclaration, visitMinusExpression, visitModuloExpression, visitMultExpression, visitNameExpression, visitNewAnonymousClassExpression, visitNullLiteral, visitPackageImport, visitPackageName, visitParenthesedExpression, visitRealLiteral, visitRelationalExpression, visitReturnStatement, visitShortLiteral, visitStringLiteral, visitSuperExpression, visitSwitchGroup, visitSwitchLabel, visitSwitchStatement, visitSynchronizedStatement, visitThisExpression, visitThrowStatement, visitTLMethodBody, visitTopLevelMethodDeclaration, visitTryCatchStatement, visitTryFinallyStatement, visitTypeDeclarationStatement, visitTypeNameExpression, 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.multijava.mjc.MjcVisitor
visitAddExpression, visitArrayDimsAndInit, visitArrayInitializer, visitArrayLengthExpression, visitAssertStatement, visitAssignmentExpression, visitBlockStatement, visitBooleanLiteral, visitBreakStatement, visitCatchClause, visitClassBlock, visitClassDeclaration, visitClassExpression, visitClassOrGFImport, visitCompoundStatement, visitConditionalAndExpression, visitConditionalExpression, visitConditionalOrExpression, visitConstructorBlock, visitConstructorDeclaration, visitContinueStatement, visitDivideExpression, visitDoStatement, visitEmptyStatement, visitExplicitConstructorInvocation, visitExpressionListStatement, visitExpressionStatement, visitFieldDeclaration, visitForStatement, visitGenericFunctionDecl, visitIfStatement, visitInitializerDeclaration, visitInstanceofExpression, visitInterfaceDeclaration, visitLabeledStatement, visitLocalVariableExpression, visitMathModeExpression, visitMethodCallExpression, visitMethodDeclaration, visitMinusExpression, visitModuloExpression, visitMultExpression, visitNameExpression, visitNewAnonymousClassExpression, visitNullLiteral, visitPackageImport, visitPackageName, visitParenthesedExpression, visitRealLiteral, visitRelationalExpression, visitReturnStatement, visitStringLiteral, visitSuperExpression, visitSwitchGroup, visitSwitchLabel, visitSwitchStatement, visitSynchronizedStatement, visitThisExpression, visitThrowStatement, visitTopLevelMethodDeclaration, visitTryCatchStatement, visitTryFinallyStatement, visitTypeDeclarationStatement, visitTypeNameExpression, visitVariableDefinition, visitWarnExpression, visitWhileStatement
 

Field Detail

NEW_LINE

public static final String NEW_LINE

offset

protected int offset
the space from '@' to the current print position for specification.

inAnnotation

private boolean inAnnotation
indicates if currently printing inside a JML annotation marker. 

 private invariant inAnnotation <==> annotationDepth > 0;

annotationDepth

private int annotationDepth
the depth of annotations. 

 private invariant annotationDepth >= 0;

atMarkerPos

private int atMarkerPos
the column number where annotation markers were written.

jmlModUtil

private JmlModifier jmlModUtil
Modifier utility to manipulating modifiers, e.g., to get string representations of modifiers from bit mask encoding. 

 private invariant jmlModUtil != null && jmlModUtil == modUtil &&
           inAnnotation <==> jmlModUtil.withoutMarkers();

Constructor Detail

RacPrettyPrinter

public RacPrettyPrinter(Writer writer,
                        JmlModifier modUtil)
Constructs a pretty printer object for JML specifications

Parameters:
writer - the object to which java code be written
modUtil - the modifier utility to print Java and JML modifiers

RacPrettyPrinter

public RacPrettyPrinter(String fileName,
                        JmlModifier modUtil)
Constructs a pretty printer object for JML specifications

Parameters:
fileName - the file into which the code is to be printed
modUtil - the modifier utility to print Java and JML modifiers

RacPrettyPrinter

public RacPrettyPrinter(File file,
                        JmlModifier modUtil)
Constructs a pretty printer object for JML specifications

Parameters:
file - the file into which the code is to be printed
modUtil - the modifier utility to print Java and JML modifiers

RacPrettyPrinter

public RacPrettyPrinter(TabbedPrintWriter writer)
Constructs a pretty printer object for JML specifications

Parameters:
writer - the file into which the code is to be printed
Method Detail

visitJmlCompilationUnit

public void visitJmlCompilationUnit(JmlCompilationUnit self)
Prints a JML compilation unit.

Specified by:
visitJmlCompilationUnit in interface JmlVisitor

visitCompilationUnit

public void visitCompilationUnit(JCompilationUnit self)
Prints a compilation unit. This method is overridden here to not print type declarations in self, the reason being that, due to refinement, combined type declarations should be printed and this can only be done at JML level.

Specified by:
visitCompilationUnit in interface MjcVisitor
Overrides:
visitCompilationUnit in class MjcPrettyPrinter

visitJmlClassDeclaration

public void visitJmlClassDeclaration(JmlClassDeclaration self)
Prints a JML class declaration.

Specified by:
visitJmlClassDeclaration in interface JmlVisitor

visitClassBody

protected void visitClassBody(JmlTypeDeclaration self)
Prints a JML type declaration.

visitJmlInterfaceDeclaration

public void visitJmlInterfaceDeclaration(JmlInterfaceDeclaration self)
Prints a JML interface declaration.

Specified by:
visitJmlInterfaceDeclaration in interface JmlVisitor

visitJmlMethodDeclaration

public void visitJmlMethodDeclaration(JmlMethodDeclaration self)
Prints a JML method declaration.

Specified by:
visitJmlMethodDeclaration in interface JmlVisitor

visitRacJmlMethodDeclaration

public void visitRacJmlMethodDeclaration(JmlMethodDeclaration self)
Prints a JML method declaration in Racc. As the Mjcvisitor can't deal with \bigint, this method is create.

See Also:
MjcPrettyPrinter#visitMethodDeclaration()

visitBigintLiteral

protected void visitBigintLiteral(long value)
Translates a \bigint literal.

applyBinaryExpression

protected void applyBinaryExpression(JExpression left,
                                     JExpression right,
                                     String oper)
prints a binary expression with the given operator and binary exps.

visitBinaryExpression

protected void visitBinaryExpression(JBinaryExpression self,
                                     String oper)
prints a binary expression with the given operator

Overrides:
visitBinaryExpression in class MjcPrettyPrinter

visitEqualityExpression

public void visitEqualityExpression(JEqualityExpression self)
prints an equality expression

Specified by:
visitEqualityExpression in interface MjcVisitor
Overrides:
visitEqualityExpression in class MjcPrettyPrinter

visitShiftExpression

public void visitShiftExpression(JShiftExpression self)
prints a shift expression

Specified by:
visitShiftExpression in interface MjcVisitor
Overrides:
visitShiftExpression in class MjcPrettyPrinter

visitBitwiseExpression

public void visitBitwiseExpression(JBitwiseExpression self)
prints a bitwise expression

Specified by:
visitBitwiseExpression in interface MjcVisitor
Overrides:
visitBitwiseExpression in class MjcPrettyPrinter

visitUnaryExpression

public void visitUnaryExpression(JUnaryExpression self)
prints an unary expression

Specified by:
visitUnaryExpression in interface MjcVisitor
Overrides:
visitUnaryExpression in class MjcPrettyPrinter

visitArrayAccessExpression

public void visitArrayAccessExpression(JArrayAccessExpression self)
prints an array length expression

Specified by:
visitArrayAccessExpression in interface MjcVisitor
Overrides:
visitArrayAccessExpression in class MjcPrettyPrinter

visitFieldExpression

public void visitFieldExpression(JClassFieldExpression self)
prints a field expression, if it's not a model field then invoke the method in super class

Specified by:
visitFieldExpression in interface MjcVisitor
Overrides:
visitFieldExpression in class MjcPrettyPrinter

visitCompoundAssignmentExpression

public void visitCompoundAssignmentExpression(JCompoundAssignmentExpression self)
prints a compound assignment expression

Specified by:
visitCompoundAssignmentExpression in interface MjcVisitor
Overrides:
visitCompoundAssignmentExpression in class MjcPrettyPrinter

visitPrefixExpression

public void visitPrefixExpression(JPrefixExpression self)
prints a prefix expression

Specified by:
visitPrefixExpression in interface MjcVisitor
Overrides:
visitPrefixExpression in class MjcPrettyPrinter

visitPostfixExpression

public void visitPostfixExpression(JPostfixExpression self)
prints a postfix expression

Specified by:
visitPostfixExpression in interface MjcVisitor
Overrides:
visitPostfixExpression in class MjcPrettyPrinter

printVariableDefinition

private void printVariableDefinition(JVariableDefinition self,
                                     boolean typeAndMod)
Prints the given variable definition, self. If the argument, typeAndMod is true, the type and modifiers are also printed; otherwise, they are not printed.

visitVariableDeclarationStatement

public void visitVariableDeclarationStatement(JVariableDeclarationStatement self)
prints a variable declaration statement

Specified by:
visitVariableDeclarationStatement in interface MjcVisitor
Overrides:
visitVariableDeclarationStatement in class MjcPrettyPrinter

visitFormalParameters

public void visitFormalParameters(JFormalParameter self)
Description copied from interface: MjcVisitor
visits a formal parameter

Specified by:
visitFormalParameters in interface MjcVisitor
Overrides:
visitFormalParameters in class MjcPrettyPrinter

visitJmlConstructorDeclaration

public void visitJmlConstructorDeclaration(JmlConstructorDeclaration self)
Prints a JML constructor declaration.

Specified by:
visitJmlConstructorDeclaration in interface JmlVisitor

visitJmlPredicate

public void visitJmlPredicate(JmlPredicate self)
Prints a JML predicate.

Specified by:
visitJmlPredicate in interface JmlVisitor

visitJmlPredicateKeyword

public void visitJmlPredicateKeyword(JmlPredicateKeyword self)
Specified by:
visitJmlPredicateKeyword in interface JmlVisitor

visitRacPredicate

public void visitRacPredicate(RacPredicate self)
Prints a RAC predicate.

Specified by:
visitRacPredicate in interface RacVisitor

visitJmlSpecExpression

public void visitJmlSpecExpression(JmlSpecExpression self)
Prints a JML specification expression.

Specified by:
visitJmlSpecExpression in interface JmlVisitor

visitRacNode

public void visitRacNode(RacNode self)
Prints a given RacNode. A RacNode is a special AST node for storing generated runtime assertion check code. It is a sequence of intermixed RacParser.END_OF_LINE, String, and AST nodes.

Specified by:
visitRacNode in interface RacVisitor
See Also:
RacNode

println

protected void println(String code)
Prints multi-lined code with proper line-breaking and indentation.

visitJmlAbruptSpecBody

public void visitJmlAbruptSpecBody(JmlAbruptSpecBody self)
Prints a JML abrupt spec body.

Specified by:
visitJmlAbruptSpecBody in interface JmlVisitor

visitJmlAbruptSpecCase

public void visitJmlAbruptSpecCase(JmlAbruptSpecCase self)
Prints a JML abrupt spec case.

Specified by:
visitJmlAbruptSpecCase in interface JmlVisitor

visitJmlAccessibleClause

public void visitJmlAccessibleClause(JmlAccessibleClause self)
Prints a JML accessible clause.

Specified by:
visitJmlAccessibleClause in interface JmlVisitor

visitJmlAssertStatement

public void visitJmlAssertStatement(JmlAssertStatement self)
Prints a JML assignable clause. If runtime assertion check code has been generated, it is also printed.

Specified by:
visitJmlAssertStatement in interface JmlVisitor

visitJmlAssignableClause

public void visitJmlAssignableClause(JmlAssignableClause self)
Prints a JML assignable clause.

Specified by:
visitJmlAssignableClause in interface JmlVisitor

visitJmlAssumeStatement

public void visitJmlAssumeStatement(JmlAssumeStatement self)
Prints a JML assume statement. If runtime assertion check code has been generated, it is also printed.

Specified by:
visitJmlAssumeStatement in interface JmlVisitor

visitJmlAxiom

public void visitJmlAxiom(JmlAxiom self)
Prints a JML axim.

Specified by:
visitJmlAxiom in interface JmlVisitor

visitJmlBehaviorSpec

public void visitJmlBehaviorSpec(JmlBehaviorSpec self)
Prints a JML behavior spec.

Specified by:
visitJmlBehaviorSpec in interface JmlVisitor

visitJmlBreaksClause

public void visitJmlBreaksClause(JmlBreaksClause self)
Prints a JML break clause.

Specified by:
visitJmlBreaksClause in interface JmlVisitor

visitJmlCallableClause

public void visitJmlCallableClause(JmlCallableClause self)
Prints a JML callable clause.

Specified by:
visitJmlCallableClause in interface JmlVisitor

visitJmlMethodNameList

public void visitJmlMethodNameList(JmlMethodNameList self)
Specified by:
visitJmlMethodNameList in interface JmlVisitor

visitJmlCapturesClause

public void visitJmlCapturesClause(JmlCapturesClause self)
Prints a JML captures clause.

Specified by:
visitJmlCapturesClause in interface JmlVisitor

visitJmlClassBlock

public void visitJmlClassBlock(JmlClassBlock self)
Prints static or instance initializer

Specified by:
visitJmlClassBlock in interface JmlVisitor

visitJmlClassOrGFImport

public void visitJmlClassOrGFImport(JmlClassOrGFImport self)
Prints a JML classOrGFImport clause.

Specified by:
visitJmlClassOrGFImport in interface JmlVisitor

visitJmlCodeContract

public void visitJmlCodeContract(JmlCodeContract self)
Prints a JML code contract.

Specified by:
visitJmlCodeContract in interface JmlVisitor

visitJmlConstraint

public void visitJmlConstraint(JmlConstraint self)
Prints a JML constraint clause.

Specified by:
visitJmlConstraint in interface JmlVisitor

visitJmlConstructorName

public void visitJmlConstructorName(JmlConstructorName self)
Prints a JML constructor name.

Specified by:
visitJmlConstructorName in interface JmlVisitor

visitJmlContinuesClause

public void visitJmlContinuesClause(JmlContinuesClause self)
Prints a JML continues statement.

Specified by:
visitJmlContinuesClause in interface JmlVisitor

visitJmlDebugStatement

public void visitJmlDebugStatement(JmlDebugStatement self)
Prints a JML debug statement.

Specified by:
visitJmlDebugStatement in interface JmlVisitor

visitJmlDivergesClause

public void visitJmlDivergesClause(JmlDivergesClause self)
Prints a JML diverges clause.

Specified by:
visitJmlDivergesClause in interface JmlVisitor

visitJmlElemTypeExpression

public void visitJmlElemTypeExpression(JmlElemTypeExpression self)
Prints a JML elemtype expression.

Specified by:
visitJmlElemTypeExpression in interface JmlVisitor

visitJmlEnsuresClause

public void visitJmlEnsuresClause(JmlEnsuresClause self)
Prints a JML ensures clause.

Specified by:
visitJmlEnsuresClause in interface JmlVisitor

visitJmlExample

public void visitJmlExample(JmlExample self)
Prints a JML example.

Specified by:
visitJmlExample in interface JmlVisitor

visitJmlExceptionalBehaviorSpec

public void visitJmlExceptionalBehaviorSpec(JmlExceptionalBehaviorSpec self)
Prints a JML exceptional behavior specification.

Specified by:
visitJmlExceptionalBehaviorSpec in interface JmlVisitor

visitJmlExceptionalExample

public void visitJmlExceptionalExample(JmlExceptionalExample self)
Prints a JML exceptional example.

Specified by:
visitJmlExceptionalExample in interface JmlVisitor

visitJmlExceptionalSpecBody

public void visitJmlExceptionalSpecBody(JmlExceptionalSpecBody self)
Prints a JML exceptional spec body.

Specified by:
visitJmlExceptionalSpecBody in interface JmlVisitor

visitJmlExceptionalSpecCase

public void visitJmlExceptionalSpecCase(JmlExceptionalSpecCase self)
Prints a JML exceptional spec case.

Specified by:
visitJmlExceptionalSpecCase in interface JmlVisitor

visitJmlExtendingSpecification

public void visitJmlExtendingSpecification(JmlExtendingSpecification self)
Prints a JML method extending specification.

Specified by:
visitJmlExtendingSpecification in interface JmlVisitor

visitMethodSpecification

private void visitMethodSpecification(JmlSpecification self)
Prints a JML method extending specification.

visitJmlFieldDeclaration

public void visitJmlFieldDeclaration(JmlFieldDeclaration self)
Prints the given JML field declaration. If this field declaration has a generated initialzer block (e.g., one for a ghost field), it is also printed.

Specified by:
visitJmlFieldDeclaration in interface JmlVisitor

visitJmlForAllVarDecl

public void visitJmlForAllVarDecl(JmlForAllVarDecl self)
Prints a JML forall variable declaration.

Specified by:
visitJmlForAllVarDecl in interface JmlVisitor

visitVarDecls

private void visitVarDecls(JVariableDefinition[] varDefs)
Prints a Java variable delcaration.

visitJmlFormalParameter

public void visitJmlFormalParameter(JmlFormalParameter self)
Prints a JML formal parameter.

Specified by:
visitJmlFormalParameter in interface JmlVisitor

visitJmlFreshExpression

public void visitJmlFreshExpression(JmlFreshExpression self)
Prints a JML fresh expression.

Specified by:
visitJmlFreshExpression in interface JmlVisitor

visitJmlGenericSpecBody

public void visitJmlGenericSpecBody(JmlGenericSpecBody self)
Prints a JML generic spec body.

Specified by:
visitJmlGenericSpecBody in interface JmlVisitor

visitJmlGenericSpecCase

public void visitJmlGenericSpecCase(JmlGenericSpecCase self)
Prints a JML generic spec case.

Specified by:
visitJmlGenericSpecCase in interface JmlVisitor

visitJmlGuardedStatement

public void visitJmlGuardedStatement(JmlGuardedStatement self)
Prints a JML guarded statement.

Specified by:
visitJmlGuardedStatement in interface JmlVisitor

visitJmlHenceByStatement

public void visitJmlHenceByStatement(JmlHenceByStatement self)
Prints a JML henceby statement.

Specified by:
visitJmlHenceByStatement in interface JmlVisitor

visitJmlInGroupClause

public void visitJmlInGroupClause(JmlInGroupClause self)
Prints a JML in data group clause.

Specified by:
visitJmlInGroupClause in interface JmlVisitor

visitJmlInformalExpression

public void visitJmlInformalExpression(JmlInformalExpression self)
Prints a JML informal expression.

Specified by:
visitJmlInformalExpression in interface JmlVisitor

visitJmlInformalStoreRef

public void visitJmlInformalStoreRef(JmlInformalStoreRef self)
Prints a JML informal store reference.

Specified by:
visitJmlInformalStoreRef in interface JmlVisitor

visitJmlInitiallyVarAssertion

public void visitJmlInitiallyVarAssertion(JmlInitiallyVarAssertion self)
Prints a JML initially variable assertion.

Specified by:
visitJmlInitiallyVarAssertion in interface JmlVisitor

visitJmlInvariant

public void visitJmlInvariant(JmlInvariant self)
Prints a JML invariant.

Specified by:
visitJmlInvariant in interface JmlVisitor

visitJmlInvariantForExpression

public void visitJmlInvariantForExpression(JmlInvariantForExpression self)
Prints a JML invariant for expression.

Specified by:
visitJmlInvariantForExpression in interface JmlVisitor

visitJmlInvariantStatement

public void visitJmlInvariantStatement(JmlInvariantStatement self)
Prints a JML invariant statement.

Specified by:
visitJmlInvariantStatement in interface JmlVisitor

visitJmlIsInitializedExpression

public void visitJmlIsInitializedExpression(JmlIsInitializedExpression self)
Prints a JML isinitialized expression.

Specified by:
visitJmlIsInitializedExpression in interface JmlVisitor

visitJmlLabelExpression

public void visitJmlLabelExpression(JmlLabelExpression self)
Prints a JML label expression.

Specified by:
visitJmlLabelExpression in interface JmlVisitor

visitJmlLetVarDecl

public void visitJmlLetVarDecl(JmlLetVarDecl self)
Prints a JML old variable declaration.

Specified by:
visitJmlLetVarDecl in interface JmlVisitor

visitJmlVariableDefinition

public void visitJmlVariableDefinition(JmlVariableDefinition self)
Prints a JML variable declaration.

Specified by:
visitJmlVariableDefinition in interface JmlVisitor

visitJmlLockSetExpression

public void visitJmlLockSetExpression(JmlLockSetExpression self)
Prints a JML lockset expression.

Specified by:
visitJmlLockSetExpression in interface JmlVisitor

visitJmlLoopInvariant

public void visitJmlLoopInvariant(JmlLoopInvariant self)
Prints a JML loop invariant.

Specified by:
visitJmlLoopInvariant in interface JmlVisitor

visitJmlLoopStatement

public void visitJmlLoopStatement(JmlLoopStatement self)
Prints a JML loop statement. A JML loop statement is a Java loop statement with optional loop invariants and variants.

Specified by:
visitJmlLoopStatement in interface JmlVisitor

visitJmlWorkingSpaceClause

public void visitJmlWorkingSpaceClause(JmlWorkingSpaceClause self)
Prints a JML working space clause.

Specified by:
visitJmlWorkingSpaceClause in interface JmlVisitor

visitJmlDurationClause

public void visitJmlDurationClause(JmlDurationClause self)
Prints a JML duration clause.

Specified by:
visitJmlDurationClause in interface JmlVisitor

visitJmlMapsIntoClause

public void visitJmlMapsIntoClause(JmlMapsIntoClause self)
Prints a JML maps into data group clause.

Specified by:
visitJmlMapsIntoClause in interface JmlVisitor

visitJmlMeasuredClause

public void visitJmlMeasuredClause(JmlMeasuredClause self)
Prints a JML measured clause.

Specified by:
visitJmlMeasuredClause in interface JmlVisitor

visitJmlMethodName

public void visitJmlMethodName(JmlMethodName self)
Prints a JML method name.

Specified by:
visitJmlMethodName in interface JmlVisitor

visitJmlModelProgram

public void visitJmlModelProgram(JmlModelProgram self)
Prints a JML model program.

Specified by:
visitJmlModelProgram in interface JmlVisitor

visitJmlMonitorsForVarAssertion

public void visitJmlMonitorsForVarAssertion(JmlMonitorsForVarAssertion self)
Prints a JML MonitorsFor variable assertion.

Specified by:
visitJmlMonitorsForVarAssertion in interface JmlVisitor

visitJmlName

public void visitJmlName(JmlName self)
Prints a JML name.

Specified by:
visitJmlName in interface JmlVisitor

visitJmlNonNullElementsExpression

public void visitJmlNonNullElementsExpression(JmlNonNullElementsExpression self)
Prints a JML \nonnullelements expression.

Specified by:
visitJmlNonNullElementsExpression in interface JmlVisitor

visitJmlAssignmentStatement

public void visitJmlAssignmentStatement(JmlAssignmentStatement self)
Specified by:
visitJmlAssignmentStatement in interface JmlVisitor

visitJmlNondetChoiceStatement

public void visitJmlNondetChoiceStatement(JmlNondetChoiceStatement self)
Prints a JML nondeterministic choice statement.

Specified by:
visitJmlNondetChoiceStatement in interface JmlVisitor

visitJmlNondetIfStatement

public void visitJmlNondetIfStatement(JmlNondetIfStatement self)
Prints a JML nondeterministic if statement.

Specified by:
visitJmlNondetIfStatement in interface JmlVisitor

visitJmlNormalBehaviorSpec

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

Specified by:
visitJmlNormalBehaviorSpec in interface JmlVisitor

visitJmlNormalExample

public void visitJmlNormalExample(JmlNormalExample self)
Prints a JML normal example.

Specified by:
visitJmlNormalExample in interface JmlVisitor

visitJmlNormalSpecBody

public void visitJmlNormalSpecBody(JmlNormalSpecBody self)
Prints a JML normal spec body.

Specified by:
visitJmlNormalSpecBody in interface JmlVisitor

visitJmlNormalSpecCase

public void visitJmlNormalSpecCase(JmlNormalSpecCase self)
Prints a JML normal spec case.

Specified by:
visitJmlNormalSpecCase in interface JmlVisitor

visitJmlNotModifiedExpression

public void visitJmlNotModifiedExpression(JmlNotModifiedExpression self)
Prints a JML \not_modified expression.

Specified by:
visitJmlNotModifiedExpression in interface JmlVisitor

visitJmlNotAssignedExpression

public void visitJmlNotAssignedExpression(JmlNotAssignedExpression self)
Prints a JML \not_assigned expression.

Specified by:
visitJmlNotAssignedExpression in interface JmlVisitor

visitJmlOnlyAccessedExpression

public void visitJmlOnlyAccessedExpression(JmlOnlyAccessedExpression self)
Prints a JML \only_accessed expression.

Specified by:
visitJmlOnlyAccessedExpression in interface JmlVisitor

visitJmlOnlyAssignedExpression

public void visitJmlOnlyAssignedExpression(JmlOnlyAssignedExpression self)
Prints a JML \only_assigned expression.

Specified by:
visitJmlOnlyAssignedExpression in interface JmlVisitor

visitJmlOnlyCalledExpression

public void visitJmlOnlyCalledExpression(JmlOnlyCalledExpression self)
Prints a JML \only_called expression.

Specified by:
visitJmlOnlyCalledExpression in interface JmlVisitor

visitJmlOnlyCapturedExpression

public void visitJmlOnlyCapturedExpression(JmlOnlyCapturedExpression self)
Prints a JML \only_captured expression.

Specified by:
visitJmlOnlyCapturedExpression in interface JmlVisitor

visitJmlStoreRefListWrapper

public void visitJmlStoreRefListWrapper(JmlStoreRefListWrapper self)

visitJmlOldExpression

public void visitJmlOldExpression(JmlOldExpression self)
Prints a JML \old expression.

Specified by:
visitJmlOldExpression in interface JmlVisitor

visitJmlPreExpression

public void visitJmlPreExpression(JmlPreExpression self)
Prints a JML \pre expression.

Specified by:
visitJmlPreExpression in interface JmlVisitor

visitJmlMaxExpression

public void visitJmlMaxExpression(JmlMaxExpression self)
Prints a JML \max expression.

Specified by:
visitJmlMaxExpression in interface JmlVisitor

visitJmlDurationExpression

public void visitJmlDurationExpression(JmlDurationExpression self)
Prints a JML \duration expression.

Specified by:
visitJmlDurationExpression in interface JmlVisitor

visitJmlWorkingSpaceExpression

public void visitJmlWorkingSpaceExpression(JmlWorkingSpaceExpression self)
Prints a JML \working_space expression.

Specified by:
visitJmlWorkingSpaceExpression in interface JmlVisitor

visitJmlSpaceExpression

public void visitJmlSpaceExpression(JmlSpaceExpression self)
Prints a JML \space expression.

Specified by:
visitJmlSpaceExpression in interface JmlVisitor

visitJmlPackageImport

public void visitJmlPackageImport(JmlPackageImport self)
Prints a JML package import statement.

Specified by:
visitJmlPackageImport in interface JmlVisitor

visitJmlReachExpression

public void visitJmlReachExpression(JmlReachExpression self)
Prints a JML reach expression.

Specified by:
visitJmlReachExpression in interface JmlVisitor

visitJmlReadableIfVarAssertion

public void visitJmlReadableIfVarAssertion(JmlReadableIfVarAssertion self)
Prints a JML readableif variable assertion.

Specified by:
visitJmlReadableIfVarAssertion in interface JmlVisitor

visitJmlWritableIfVarAssertion

public void visitJmlWritableIfVarAssertion(JmlWritableIfVarAssertion self)
Specified by:
visitJmlWritableIfVarAssertion in interface JmlVisitor

visitJmlRedundantSpec

public void visitJmlRedundantSpec(JmlRedundantSpec self)
Prints a JML redundant specifications including implies_that and for_example.

Specified by:
visitJmlRedundantSpec in interface JmlVisitor

visitJmlRefinePrefix

public void visitJmlRefinePrefix(JmlRefinePrefix self)
Prints a JML refine prefix.

Specified by:
visitJmlRefinePrefix in interface JmlVisitor

visitJmlRelationalExpression

public void visitJmlRelationalExpression(JmlRelationalExpression self)
Prints a JML relational expression.

Specified by:
visitJmlRelationalExpression in interface JmlVisitor

visitJmlRepresentsDecl

public void visitJmlRepresentsDecl(JmlRepresentsDecl self)
Prints a JML represents declaration.

Specified by:
visitJmlRepresentsDecl in interface JmlVisitor

visitJmlRequiresClause

public void visitJmlRequiresClause(JmlRequiresClause self)
Prints a JML requires clause.

Specified by:
visitJmlRequiresClause in interface JmlVisitor

visitJmlResultExpression

public void visitJmlResultExpression(JmlResultExpression self)
Prints a JML \result expression.

Specified by:
visitJmlResultExpression in interface JmlVisitor

visitJmlReturnsClause

public void visitJmlReturnsClause(JmlReturnsClause self)
Prints a JML return clause.

Specified by:
visitJmlReturnsClause in interface JmlVisitor

visitJmlSetComprehension

public void visitJmlSetComprehension(JmlSetComprehension self)
Prints a JML set comprehension expression.

Specified by:
visitJmlSetComprehension in interface JmlVisitor

visitJmlSetStatement

public void visitJmlSetStatement(JmlSetStatement self)
Prints the given JML set statement.

Specified by:
visitJmlSetStatement in interface JmlVisitor

visitJmlSignalsOnlyClause

public void visitJmlSignalsOnlyClause(JmlSignalsOnlyClause self)
Prints a JML signals_only clause

Specified by:
visitJmlSignalsOnlyClause in interface JmlVisitor

visitJmlSignalsClause

public void visitJmlSignalsClause(JmlSignalsClause self)
Prints a JML signals clause

Specified by:
visitJmlSignalsClause in interface JmlVisitor

visitJmlSpecQuantifiedExpression

public void visitJmlSpecQuantifiedExpression(JmlSpecQuantifiedExpression self)
Prints a JML specification quantified expression.

Specified by:
visitJmlSpecQuantifiedExpression in interface JmlVisitor

visitJmlSpecStatement

public void visitJmlSpecStatement(JmlSpecStatement self)
Prints a JML specification statement.

Specified by:
visitJmlSpecStatement in interface JmlVisitor

visitJmlSpecification

public void visitJmlSpecification(JmlSpecification self)
Prints a JML specification.

Specified by:
visitJmlSpecification in interface JmlVisitor

visitJmlStoreRefExpression

public void visitJmlStoreRefExpression(JmlStoreRefExpression self)
Prints a JML store reference expression.

Specified by:
visitJmlStoreRefExpression in interface JmlVisitor

visitJmlStoreRefKeyword

public void visitJmlStoreRefKeyword(JmlStoreRefKeyword self)
Prints a JML store reference keywords such as \everything, \nothing, and \not_specified.

Specified by:
visitJmlStoreRefKeyword in interface JmlVisitor

visitJmlTypeExpression

public void visitJmlTypeExpression(JmlTypeExpression self)
Prints a JML \type expression.

Specified by:
visitJmlTypeExpression in interface JmlVisitor

visitJmlTypeOfExpression

public void visitJmlTypeOfExpression(JmlTypeOfExpression self)
Prints a JML \typeof expression.

Specified by:
visitJmlTypeOfExpression in interface JmlVisitor

visitJmlUnreachableStatement

public void visitJmlUnreachableStatement(JmlUnreachableStatement self)
Prints a JML unreachable statement.

Specified by:
visitJmlUnreachableStatement in interface JmlVisitor

visitJmlVariantFunction

public void visitJmlVariantFunction(JmlVariantFunction self)
Prints a JML variant function.

Specified by:
visitJmlVariantFunction in interface JmlVisitor

visitJmlWhenClause

public void visitJmlWhenClause(JmlWhenClause self)
Prints a JML when clause.

Specified by:
visitJmlWhenClause in interface JmlVisitor

visitCastExpression

public void visitCastExpression(JCastExpression self)
Prints a cast expression.

Specified by:
visitCastExpression in interface MjcVisitor
Overrides:
visitCastExpression in class MjcPrettyPrinter

visitUnaryPromoteExpression

public void visitUnaryPromoteExpression(JUnaryPromote self)
prints a unaryPrompte expression

Specified by:
visitUnaryPromoteExpression in interface MjcVisitor
Overrides:
visitUnaryPromoteExpression in class MjcPrettyPrinter

visitNewObjectExpression

public void visitNewObjectExpression(JNewObjectExpression self)
Prints an object allocator expression.

Specified by:
visitNewObjectExpression in interface MjcVisitor
Overrides:
visitNewObjectExpression in class MjcPrettyPrinter

visitNewArrayExpression

public void visitNewArrayExpression(JNewArrayExpression self)
Prints an array allocator expression.

Specified by:
visitNewArrayExpression in interface MjcVisitor
Overrides:
visitNewArrayExpression in class MjcPrettyPrinter

visitOrdinalLiteral

public void visitOrdinalLiteral(JOrdinalLiteral self)
Prints an ordinal literal.

Specified by:
visitOrdinalLiteral in interface MjcVisitor
Overrides:
visitOrdinalLiteral in class MjcPrettyPrinter

visitCharLiteral

public void visitCharLiteral(JCharLiteral self)
Prints a character literal. This method is overridden here to specially handle non-printable characters such as unicode chars.

Specified by:
visitCharLiteral in interface MjcVisitor
Overrides:
visitCharLiteral in class MjcPrettyPrinter

visitDoubleLiteral

protected void visitDoubleLiteral(double value)
Prints a double literal. This method is overridden here to take care of special values such as INFINITY, NaN, MIN_VALUE, and MAX_VALUE.

Overrides:
visitDoubleLiteral in class MjcPrettyPrinter

visitFloatLiteral

protected void visitFloatLiteral(float value)
Prints a float literal. This method is overridden here to take care of special values such as Float.POSTIVE_INFINITY, Float.NaN, etc.

Overrides:
visitFloatLiteral in class MjcPrettyPrinter

toString

protected String toString(CType type)
Description copied from class: MjcPrettyPrinter
Returns the string for the given type. E.g., if the type represents a local local class such as n1.n2.1.n3, then returned is the string "n3".

Overrides:
toString in class MjcPrettyPrinter

visitGeneralSpecCase

public void visitGeneralSpecCase(JmlGeneralSpecCase self)
Prints the given general spec case.

visitSpecCases

protected void visitSpecCases(JmlSpecCase[] specCases)
Prints spec cases.

visitExample

protected void visitExample(JmlExample self)
Prints example specifications.

visitSpecBody

protected void visitSpecBody(JmlSpecBody self)
Prints specification body.

visitSpecBodyClause

public void visitSpecBodyClause(JmlPredicateClause self,
                                String keyword)
Prints specfication body clause.

mayStartAnnotation

protected void mayStartAnnotation()
Starts the annotation printing mode if not already in; also prints the opening annotation marker /*@. 

 modifies annotationDepth, inAnnotation, jmlModUtil, atMarkerPos;
 ensures annotationDepth == \old(annotationDepth) + 1;
 ensures_redundantly inAnnotation && jmlModUtil.withoutMarkers();

See Also:
mayEndAnnotation(), mayStartAnnotation(boolean)

mayEndAnnotation

protected void mayEndAnnotation()
Stops the annotation printing mode if currently in that mode; also prints the closing annotation marker @*/. 

 modifies annotationDepth, inAnnotation, jmlModUtil;
 ensures annotationDepth == \old(annotationDepth) - 1;

See Also:
mayStartAnnotation(), mayEndAnnotation(boolean)

mayStartAnnotation

protected void mayStartAnnotation(boolean flag)
Starts the annotation printing mode if flag is true and not already in the annotation mode; also prints the opening annotation marker /*@. 

 modifies annotationDepth, inAnnotation, jmlModUtil, atMarkerPos;
 ensures flag ==> (annotationDepth == \old(annotationDepth) + 1);
 ensures_redundantly flag ==> 
   (inAnnotation && jmlModUtil.withoutMarkers());

See Also:
mayEndAnnotation(boolean)

mayEndAnnotation

protected void mayEndAnnotation(boolean flag)
Stops the annotation printing mode if the flag is true and currently in the annotation mode; also prints the closing annotation marker @*/. 

 modifies annotationDepth, inAnnotation, jmlModUtil;
 ensures flag ==> (annotationDepth == \old(annotationDepth) - 1);

See Also:
mayStartAnnotation(boolean)

newLine

protected void newLine()
Prints a new line marker. If in the annotation mode, also print the annotation marker at the appropriate position.

Overrides:
newLine in class MjcPrettyPrinter

newLineOffset

protected void newLineOffset()
Prints a new line marker. If in the annotation mode, also print the annotation marker at the appropriate position and advance to the distance of the current offset.

print

protected void print(String s)
Prints a string.

Overrides:
print in class MjcPrettyPrinter

print

protected void print(CType t)
Prints a type.

Overrides:
print in class MjcPrettyPrinter

printJml

protected void printJml(String s)
Prints a string enclosed in the JML annotation markers. I.e., prints /*@ ... @*/.

acceptAll

protected void acceptAll(JPhylum[] all)
Visits each element of the argument.

close

public void close()
Description copied from class: MjcPrettyPrinter
Close the stream at the end

Overrides:
close in class MjcPrettyPrinter

visitJmlDeclaration

public void visitJmlDeclaration(JmlDeclaration self)
Specified by:
visitJmlDeclaration in interface JmlVisitor

visitJmlExpression

public void visitJmlExpression(JmlExpression self)
Specified by:
visitJmlExpression in interface JmlVisitor

visitJmlGeneralSpecCase

public void visitJmlGeneralSpecCase(JmlGeneralSpecCase self)
Specified by:
visitJmlGeneralSpecCase in interface JmlVisitor

visitJmlMethodSpecification

public void visitJmlMethodSpecification(JmlMethodSpecification self)
Specified by:
visitJmlMethodSpecification in interface JmlVisitor

visitJmlNode

public void visitJmlNode(JmlNode self)
Specified by:
visitJmlNode in interface JmlVisitor

visitJmlSpecBody

public void visitJmlSpecBody(JmlSpecBody self)
Specified by:
visitJmlSpecBody in interface JmlVisitor

visitJmlSpecVarDecl

public void visitJmlSpecVarDecl(JmlSpecVarDecl self)
Specified by:
visitJmlSpecVarDecl in interface JmlVisitor

visitJmlStoreRef

public void visitJmlStoreRef(JmlStoreRef self)
Specified by:
visitJmlStoreRef in interface JmlVisitor
Overview  Package   Class  Use  Tree  Deprecated  Index  Help 
JML
 PREV CLASS   NEXT CLASS FRAMES    NO FRAMES    
SUMMARY: NESTED | FIELD | CONSTR | METHOD DETAIL: FIELD | CONSTR | METHOD
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.