JML

org.jmlspecs.jmldoc.jmldoc_142
Class SpecWriter

java.lang.Object
  extended byorg.jmlspecs.checker.JmlVisitorNI
      extended byorg.jmlspecs.jmldoc.jmldoc_142.SpecWriter
All Implemented Interfaces:
Constants, Constants, Constants, JmlVisitor, MjcVisitor

public class SpecWriter
extends JmlVisitorNI
implements Constants

This class is a Visitor class that generates appropriate portions of the javadoc documentation by walking the parse tree.


Field Summary
static String BREOL
           
static int BREOLlength
           
private static String eol
          The string that terminates lines on this platform.
private  int lastLineNumber
           
(package private) static JmldocOptions options
          The command-line options, set here by JmlHTML.
private  boolean printAlso
          This field is simply used to communicate the need to print 'also' from one method to another.
protected  StringBuffer sb
          This buffer accumulates text that later is written out as a file or turned into a String.
 
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
protected SpecWriter()
          Constructs a SpecWriter with an empty text buffer.
  SpecWriter(StringBuffer s)
          Constructs a SpecWriter with the given StringBuffer.
  SpecWriter(StringBuffer s, JPhylum p)
          Constructs a SpecWriter with the given StringBuffer and then walks the AST with the SpecWriter, appending text as it goes.
  SpecWriter(JPhylum p)
          Constructs a SpecWriter with an empty text buffer and then walks the AST with the SpecWriter, accumulating text as it goes.
 
Method Summary
 void append(String s)
          Appends the given string to the SpecWriter's buffer.
 void checkLine(JPhylum self)
           
 String convertToHtml(String s)
          Copies the input string to the output, replacing instances of special html characters by html representations (less than symbols, greater than symbols, ampersands).
 String htmlop(int op, JRelationalExpression s)
           
static String jmlModifiers(long mods)
           
static void removeBR(StringBuffer classspec)
          This method removes a "
"+eol combination from the end of the given StringBuffer, if it is present.
private  String replace(String s, char c, String rep)
           
 void setLine(JPhylum self)
           
 String toString()
          Returns the accumulated text.
 void visitAddExpression(JAddExpression self)
          visits an add expression
 void visitArrayAccessExpression(JArrayAccessExpression self)
          visits an array access expression
 void visitArrayDimsAndInit(JArrayDimsAndInits self)
          visits an array dimension and initialization expression
 void visitArrayInitializer(JArrayInitializer self)
          visits an array initializer expression
 void visitArrayLengthExpression(JArrayLengthExpression self)
          visits an array length expression
 void visitAssignmentExpression(JAssignmentExpression self)
          visits an assignment expression
 void visitBitwiseExpression(JBitwiseExpression self)
          visits a bit operator expression
 void visitBlockStatement(JBlock self)
          visits an expression statement
 void visitBooleanLiteral(JBooleanLiteral self)
          visits a boolean literal
 void visitBreakStatement(JBreakStatement self)
          visits a break statement
 void visitCastExpression(JCastExpression self)
          visits a cast expression
 void visitCatchClause(JCatchClause self)
          visits a catch clause
 void visitCharLiteral(JCharLiteral self)
          visits a character literal
 void visitClassBlock(JClassBlock self)
          visits a class block (initializer)
 void visitClassDeclaration(JClassDeclarationType self)
          visits a class declaration
 void visitClassExpression(JClassExpression self)
          visits a class expression
 void visitClassOrGFImport(JClassOrGFImportType self)
          visits a class import declaration
 void visitCompilationUnit(JCompilationUnitType self)
          visits a compilation unit
 void visitCompoundAssignmentExpression(JCompoundAssignmentExpression self)
          visits a compound expression
 void visitCompoundStatement(JCompoundStatement self)
          visits a compound statement
 void visitConditionalAndExpression(JConditionalAndExpression self)
          visits a boolean AND expression
 void visitConditionalExpression(JConditionalExpression self)
          visits a conditional expression
 void visitConditionalOrExpression(JConditionalOrExpression self)
          visits a boolean OR expression
 void visitConstructorBlock(JConstructorBlock self)
          visits a constructor block
 void visitConstructorDeclaration(JConstructorDeclarationType self)
          visits a constructor declaration
 void visitContinueStatement(JContinueStatement self)
          visits a continue statement
 void visitDivideExpression(JDivideExpression self)
          visits a divide expression
 void visitDoStatement(JDoStatement self)
          visits a do statement
 void visitEmptyStatement(JEmptyStatement self)
          visits a empty statement
 void visitEqualityExpression(JEqualityExpression self)
          visits an equality expression
 void visitExplicitConstructorInvocation(JExplicitConstructorInvocation self)
          visits an explicit constructor invocation
 void visitExpressionListStatement(JExpressionListStatement self)
          visits an expression list statement
 void visitExpressionStatement(JExpressionStatement self)
          visits an expression statement
 void visitFieldDeclaration(JFieldDeclaration self)
          visits a field declaration
 void visitFieldDeclaration(JFieldDeclarationType self)
          visits a field declaration
 void visitFieldExpression(JClassFieldExpression self)
          visits a field expression
 void visitFormalParameters(JFormalParameter self)
          visits a formal parameter
 void visitForStatement(JForStatement self)
          visits a for statement
 void visitGenericFunctionDecl(MJGenericFunctionDecl self)
          visits a generic function anchor
 void visitIfStatement(JIfStatement self)
          visits a if statement
 void visitInitializerDeclaration(JInitializerDeclaration self)
          visits an initializer declaration
 void visitInstanceofExpression(JInstanceofExpression self)
          visits an instanceof expression
 void visitInterfaceDeclaration(JInterfaceDeclarationType self)
          visits an interface declaration
 void visitJmlAccessibleClause(JmlAccessibleClause self)
           
 void visitJmlAssignableClause(JmlAssignableClause self)
           
 void visitJmlAssignmentStatement(JmlAssignmentStatement self)
           
 void visitJmlAxiom(JmlAxiom self)
           
 void visitJmlBehaviorSpec(JmlBehaviorSpec self)
           
 void visitJmlBehaviorSpecHelper(JmlHeavyweightSpec self, String s)
           
 void visitJmlCallableClause(JmlCallableClause self)
           
 void visitJmlCapturesClause(JmlCapturesClause self)
           
 void visitJmlCodeContract(JmlCodeContract self)
          Prints a JML code contract.
 void visitJmlConstraint(JmlConstraint self)
           
 void visitJmlConstructorName(JmlConstructorName self)
           
 void visitJmlDeclaration(JmlDeclaration self)
          This method gets called only if a derived class does not implement accept.
 void visitJmlDivergesClause(JmlDivergesClause self)
           
 void visitJmlDurationClause(JmlDurationClause self)
           
 void visitJmlDurationExpression(JmlDurationExpression self)
           
 void visitJmlElemTypeExpression(JmlElemTypeExpression self)
           
 void visitJmlEnsuresClause(JmlEnsuresClause self)
           
 void visitJmlExample(JmlExample self)
           
 void visitJmlExampleHelper(JmlExample self, String title)
           
 void visitJmlExceptionalBehaviorSpec(JmlExceptionalBehaviorSpec self)
           
 void visitJmlExceptionalExample(JmlExceptionalExample self)
           
 void visitJmlExceptionalSpecBody(JmlExceptionalSpecBody self)
           
 void visitJmlExceptionalSpecCase(JmlGenericSpecCase self)
           
 void visitJmlExpression(JmlExpression self)
           
 void visitJmlExtendingSpecification(JmlExtendingSpecification self)
           
 void visitJmlFieldDeclaration(JmlFieldDeclaration self)
           
 void visitJmlForAllVarDecl(JmlForAllVarDecl self)
           
 void visitJmlFreshExpression(JmlFreshExpression self)
           
 void visitJmlGeneralSpecCase(JmlGeneralSpecCase self)
           
 void visitJmlGeneralSpecCaseHelper(JmlGeneralSpecCase self, boolean indent)
           
 void visitJmlGenericSpecBody(JmlGenericSpecBody self)
           
 void visitJmlGenericSpecCase(JmlGenericSpecCase self)
           
 void visitJmlGuardedStatement(JmlGuardedStatement self)
           
 void visitJmlInformalExpression(JmlInformalExpression self)
           
 void visitJmlInformalStoreRef(JmlInformalStoreRef self)
           
 void visitJmlInitiallyVarAssertion(JmlInitiallyVarAssertion self)
           
 void visitJmlInvariant(JmlInvariant self)
           
 void visitJmlInvariantForExpression(JmlInvariantForExpression self)
           
 void visitJmlIsInitializedExpression(JmlIsInitializedExpression self)
           
 void visitJmlLabelExpression(JmlLabelExpression self)
           
 void visitJmlLetVarDecl(JmlLetVarDecl self)
           
 void visitJmlLockSetExpression(JmlLockSetExpression self)
           
 void visitJmlMaxExpression(JmlMaxExpression self)
           
 void visitJmlMeasuredClause(JmlMeasuredClause self)
           
 void visitJmlMethodName(JmlMethodName self)
           
 void visitJmlMethodNameList(JmlMethodNameList self)
           
 void visitJmlModelProgram(JmlModelProgram self)
           
 void visitJmlMonitorsForVarAssertion(JmlMonitorsForVarAssertion self)
           
 void visitJmlName(JmlName self)
           
 void visitJmlNameHelper(JmlName self, boolean addDot)
           
 void visitJmlNode(JmlNode self)
           
 void visitJmlNondetChoiceStatement(JmlNondetChoiceStatement self)
           
 void visitJmlNondetIfStatement(JmlNondetIfStatement self)
           
 void visitJmlNonNullElementsExpression(JmlNonNullElementsExpression self)
           
 void visitJmlNormalBehaviorSpec(JmlNormalBehaviorSpec self)
           
 void visitJmlNormalExample(JmlNormalExample self)
           
 void visitJmlNormalSpecBody(JmlNormalSpecBody self)
           
 void visitJmlNormalSpecCase(JmlGenericSpecCase self)
           
 void visitJmlNotAssignedExpression(JmlNotAssignedExpression self)
           
 void visitJmlNotModifiedExpression(JmlNotModifiedExpression self)
           
 void visitJmlOldExpression(JmlOldExpression self)
           
 void visitJmlOnlyAssignedExpression(JmlOnlyAssignedExpression self)
           
 void visitJmlPredicate(JmlPredicate self)
           
 void visitJmlPredicateClause(JmlPredicateClause self)
           
 void visitJmlPredicateKeyword(JmlPredicateKeyword self)
           
 void visitJmlPreExpression(JmlPreExpression self)
           
 void visitJmlReachExpression(JmlReachExpression self)
           
 void visitJmlReadableIfVarAssertion(JmlReadableIfVarAssertion self)
           
 void visitJmlRedundantSpec(JmlRedundantSpec self)
           
 void visitJmlRelationalExpression(JmlRelationalExpression self)
           
 void visitJmlRepresentsDecl(JmlRepresentsDecl self)
           
 void visitJmlRequiresClause(JmlRequiresClause self)
           
 void visitJmlResultExpression(JmlResultExpression self)
           
 void visitJmlSetComprehension(JmlSetComprehension self)
           
 void visitJmlSignalsClause(JmlSignalsClause self)
           
 void visitJmlSignalsOnlyClause(JmlSignalsOnlyClause self)
           
 void visitJmlSpaceExpression(JmlSpaceExpression self)
           
 void visitJmlSpecBody(JmlSpecBody self)
           
 void visitJmlSpecBodyClause(JmlSpecBodyClause self)
           
 void visitJmlSpecExpression(JmlSpecExpression self)
           
 void visitJmlSpecification(JmlSpecification self)
           
 void visitJmlSpecificationHelper(JmlSpecCase[] scases, boolean initialAlso)
           
 void visitJmlSpecQuantifiedExpression(JmlSpecQuantifiedExpression self)
           
 void visitJmlSpecVarDecl(JmlSpecVarDecl self)
           
 void visitJmlStoreRef(JmlStoreRef self)
           
 void visitJmlStoreRefExpression(JmlStoreRefExpression self)
           
 void visitJmlStoreRefKeyword(JmlStoreRefKeyword self)
           
 void visitJmlTypeExpression(JmlTypeExpression self)
           
 void visitJmlTypeOfExpression(JmlTypeOfExpression self)
           
 void visitJmlVariableDefinition(JmlVariableDefinition self)
          visits a variable declaration statement
 void visitJmlWhenClause(JmlWhenClause self)
           
 void visitJmlWorkingSpaceClause(JmlWorkingSpaceClause self)
           
 void visitJmlWorkingSpaceExpression(JmlWorkingSpaceExpression self)
           
 void visitJmlWritableIfVarAssertion(JmlWritableIfVarAssertion self)
           
 void visitLabeledStatement(JLabeledStatement self)
          visits a labeled statement
 void visitLocalVariableExpression(JLocalVariableExpression self)
          visits a local variable expression
 void visitMathModeExpression(MJMathModeExpression self)
          visits a math mode expression
 void visitMethodCallExpression(JMethodCallExpression self)
          visits a method call expression
 void visitMethodDeclaration(JMethodDeclarationType self)
          visits a method declaration
 void visitMinusExpression(JMinusExpression self)
          visits a minus expression
 void visitModuloExpression(JModuloExpression self)
          visits a modulo division expression
 void visitMultExpression(JMultExpression self)
          visits a multiplication expression
 void visitNameExpression(JNameExpression self)
          visits a name expression
 void visitNewAnonymousClassExpression(JNewAnonymousClassExpression self)
          visits an object allocator expression for an anonymous class
 void visitNewArrayExpression(JNewArrayExpression self)
          visits an array allocator expression
 void visitNewObjectExpression(JNewObjectExpression self)
          visits an object allocator expression
 void visitNullLiteral(JNullLiteral self)
          visits a null literal
 void visitOrdinalLiteral(JOrdinalLiteral self)
          prints an ordinal literal
 void visitPackageImport(JPackageImportType self)
          visits a package import declaration
 void visitPackageName(JPackageName self)
          visits a package name declaration
 void visitParenthesedExpression(JParenthesedExpression self)
          visits a parenthesed expression
 void visitPostfixExpression(JPostfixExpression self)
          visits a postfix expression
 void visitPrefixExpression(JPrefixExpression self)
          visits a prefix expression
 void visitRealLiteral(JRealLiteral self)
          prints a real literal
 void visitRelationalExpression(JRelationalExpression self)
          visits a relational expression
 void visitReturnStatement(JReturnStatement self)
          visits a return statement
 void visitShiftExpression(JShiftExpression self)
          visits a shift expression
 void visitStringLiteral(JStringLiteral self)
          visits a string literal
 void visitSuperExpression(JSuperExpression self)
          visits a super expression
 void visitSwitchGroup(JSwitchGroup self)
          visits a switch group
 void visitSwitchLabel(JSwitchLabel self)
          visits a switch label
 void visitSwitchStatement(JSwitchStatement self)
          visits a switch statement
 void visitSynchronizedStatement(JSynchronizedStatement self)
          visits a synchronized statement
 void visitThisExpression(JThisExpression self)
          visits a this expression
 void visitThrowStatement(JThrowStatement self)
          visits a throw statement
 void visitTopLevelMethodDeclaration(MJTopLevelMethodDeclaration self)
          visits an external method declaration
 void visitTryCatchStatement(JTryCatchStatement self)
          visits a try-catch statement
 void visitTryFinallyStatement(JTryFinallyStatement self)
          visits a try-finally statement
 void visitTypeDeclarationStatement(JTypeDeclarationStatement self)
          visits a type declaration statement
 void visitTypeNameExpression(JTypeNameExpression self)
          visits a type name expression
 void visitUnaryExpression(JUnaryExpression self)
          visits an unary expression
 void visitUnaryPromoteExpression(JUnaryPromote self)
          visits a cast expression
 void visitVariableDeclarationStatement(JVariableDeclarationStatement self)
          visits a variable declaration statement
 void visitVariableDefinition(JVariableDefinition self)
          visits a variable declaration statement
 void visitWarnExpression(MJWarnExpression self)
          visits a warn expression
 void visitWhileStatement(JWhileStatement self)
          visits a while statement
(package private) static void writeModifiers(StringBuffer sb, long p)
           
(package private) static void writePrivacy(StringBuffer sb, long p)
           
 
Methods inherited from class org.jmlspecs.checker.JmlVisitorNI
imp, visitAssertStatement, visitClassDeclaration, visitClassOrGFImport, visitCompilationUnit, visitConstructorDeclaration, visitInterfaceDeclaration, visitJmlAbruptSpecBody, visitJmlAbruptSpecCase, visitJmlAssertStatement, visitJmlAssumeStatement, visitJmlBreaksClause, visitJmlClassBlock, visitJmlClassDeclaration, visitJmlClassOrGFImport, visitJmlCompilationUnit, visitJmlConstructorDeclaration, visitJmlContinuesClause, visitJmlDebugStatement, visitJmlExceptionalSpecCase, visitJmlFormalParameter, visitJmlHenceByStatement, visitJmlInGroupClause, visitJmlInterfaceDeclaration, visitJmlInvariantStatement, visitJmlLoopInvariant, visitJmlLoopStatement, visitJmlMapsIntoClause, visitJmlMethodDeclaration, visitJmlMethodSpecification, visitJmlNormalSpecCase, visitJmlOnlyAccessedExpression, visitJmlOnlyCalledExpression, visitJmlOnlyCapturedExpression, visitJmlPackageImport, visitJmlRefinePrefix, visitJmlReturnsClause, visitJmlSetStatement, visitJmlSpecStatement, visitJmlUnreachableStatement, visitJmlVariantFunction, visitMethodDeclaration, visitPackageImport
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
 

Field Detail

lastLineNumber

private int lastLineNumber

options

static JmldocOptions options
The command-line options, set here by JmlHTML.


eol

private static final String eol
The string that terminates lines on this platform.


printAlso

private boolean printAlso
This field is simply used to communicate the need to print 'also' from one method to another.


sb

protected StringBuffer sb
This buffer accumulates text that later is written out as a file or turned into a String.


BREOL

public static final String BREOL

BREOLlength

public static final int BREOLlength
Constructor Detail

SpecWriter

public SpecWriter(StringBuffer s)
Constructs a SpecWriter with the given StringBuffer.


SpecWriter

protected SpecWriter()
Constructs a SpecWriter with an empty text buffer.


SpecWriter

public SpecWriter(JPhylum p)
Constructs a SpecWriter with an empty text buffer and then walks the AST with the SpecWriter, accumulating text as it goes.


SpecWriter

public SpecWriter(StringBuffer s,
                  JPhylum p)
Constructs a SpecWriter with the given StringBuffer and then walks the AST with the SpecWriter, appending text as it goes.

Method Detail

checkLine

public void checkLine(JPhylum self)

setLine

public void setLine(JPhylum self)

toString

public String toString()
Returns the accumulated text.

Overrides:
toString in class Object

append

public void append(String s)
Appends the given string to the SpecWriter's buffer.


visitCompilationUnit

public void visitCompilationUnit(JCompilationUnitType self)
visits a compilation unit


visitClassDeclaration

public void visitClassDeclaration(JClassDeclarationType self)
visits a class declaration


visitInterfaceDeclaration

public void visitInterfaceDeclaration(JInterfaceDeclarationType self)
visits an interface declaration


visitGenericFunctionDecl

public void visitGenericFunctionDecl(MJGenericFunctionDecl self)
visits a generic function anchor

Specified by:
visitGenericFunctionDecl in interface MjcVisitor
Overrides:
visitGenericFunctionDecl in class JmlVisitorNI

visitFieldDeclaration

public void visitFieldDeclaration(JFieldDeclarationType self)
visits a field declaration


visitMethodDeclaration

public void visitMethodDeclaration(JMethodDeclarationType self)
visits a method declaration


visitInitializerDeclaration

public void visitInitializerDeclaration(JInitializerDeclaration self)
visits an initializer declaration

Specified by:
visitInitializerDeclaration in interface MjcVisitor
Overrides:
visitInitializerDeclaration in class JmlVisitorNI

visitTopLevelMethodDeclaration

public void visitTopLevelMethodDeclaration(MJTopLevelMethodDeclaration self)
visits an external method declaration

Specified by:
visitTopLevelMethodDeclaration in interface MjcVisitor
Overrides:
visitTopLevelMethodDeclaration in class JmlVisitorNI

visitConstructorDeclaration

public void visitConstructorDeclaration(JConstructorDeclarationType self)
visits a constructor declaration


visitWhileStatement

public void visitWhileStatement(JWhileStatement self)
visits a while statement

Specified by:
visitWhileStatement in interface MjcVisitor
Overrides:
visitWhileStatement in class JmlVisitorNI

visitVariableDeclarationStatement

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

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

visitVariableDefinition

public void visitVariableDefinition(JVariableDefinition self)
visits a variable declaration statement

Specified by:
visitVariableDefinition in interface MjcVisitor
Overrides:
visitVariableDefinition in class JmlVisitorNI

visitJmlVariableDefinition

public void visitJmlVariableDefinition(JmlVariableDefinition self)
visits a variable declaration statement

Specified by:
visitJmlVariableDefinition in interface JmlVisitor
Overrides:
visitJmlVariableDefinition in class JmlVisitorNI

visitTryCatchStatement

public void visitTryCatchStatement(JTryCatchStatement self)
visits a try-catch statement

Specified by:
visitTryCatchStatement in interface MjcVisitor
Overrides:
visitTryCatchStatement in class JmlVisitorNI

visitTryFinallyStatement

public void visitTryFinallyStatement(JTryFinallyStatement self)
visits a try-finally statement

Specified by:
visitTryFinallyStatement in interface MjcVisitor
Overrides:
visitTryFinallyStatement in class JmlVisitorNI

visitThrowStatement

public void visitThrowStatement(JThrowStatement self)
visits a throw statement

Specified by:
visitThrowStatement in interface MjcVisitor
Overrides:
visitThrowStatement in class JmlVisitorNI

visitSynchronizedStatement

public void visitSynchronizedStatement(JSynchronizedStatement self)
visits a synchronized statement

Specified by:
visitSynchronizedStatement in interface MjcVisitor
Overrides:
visitSynchronizedStatement in class JmlVisitorNI

visitSwitchStatement

public void visitSwitchStatement(JSwitchStatement self)
visits a switch statement

Specified by:
visitSwitchStatement in interface MjcVisitor
Overrides:
visitSwitchStatement in class JmlVisitorNI

visitReturnStatement

public void visitReturnStatement(JReturnStatement self)
visits a return statement

Specified by:
visitReturnStatement in interface MjcVisitor
Overrides:
visitReturnStatement in class JmlVisitorNI

visitLabeledStatement

public void visitLabeledStatement(JLabeledStatement self)
visits a labeled statement

Specified by:
visitLabeledStatement in interface MjcVisitor
Overrides:
visitLabeledStatement in class JmlVisitorNI

visitIfStatement

public void visitIfStatement(JIfStatement self)
visits a if statement

Specified by:
visitIfStatement in interface MjcVisitor
Overrides:
visitIfStatement in class JmlVisitorNI

visitForStatement

public void visitForStatement(JForStatement self)
visits a for statement

Specified by:
visitForStatement in interface MjcVisitor
Overrides:
visitForStatement in class JmlVisitorNI

visitCompoundStatement

public void visitCompoundStatement(JCompoundStatement self)
visits a compound statement

Specified by:
visitCompoundStatement in interface MjcVisitor
Overrides:
visitCompoundStatement in class JmlVisitorNI

visitExpressionStatement

public void visitExpressionStatement(JExpressionStatement self)
visits an expression statement

Specified by:
visitExpressionStatement in interface MjcVisitor
Overrides:
visitExpressionStatement in class JmlVisitorNI

visitExpressionListStatement

public void visitExpressionListStatement(JExpressionListStatement self)
visits an expression list statement

Specified by:
visitExpressionListStatement in interface MjcVisitor
Overrides:
visitExpressionListStatement in class JmlVisitorNI

visitEmptyStatement

public void visitEmptyStatement(JEmptyStatement self)
visits a empty statement

Specified by:
visitEmptyStatement in interface MjcVisitor
Overrides:
visitEmptyStatement in class JmlVisitorNI

visitDoStatement

public void visitDoStatement(JDoStatement self)
visits a do statement

Specified by:
visitDoStatement in interface MjcVisitor
Overrides:
visitDoStatement in class JmlVisitorNI

visitContinueStatement

public void visitContinueStatement(JContinueStatement self)
visits a continue statement

Specified by:
visitContinueStatement in interface MjcVisitor
Overrides:
visitContinueStatement in class JmlVisitorNI

visitBreakStatement

public void visitBreakStatement(JBreakStatement self)
visits a break statement

Specified by:
visitBreakStatement in interface MjcVisitor
Overrides:
visitBreakStatement in class JmlVisitorNI

visitBlockStatement

public void visitBlockStatement(JBlock self)
visits an expression statement

Specified by:
visitBlockStatement in interface MjcVisitor
Overrides:
visitBlockStatement in class JmlVisitorNI

visitConstructorBlock

public void visitConstructorBlock(JConstructorBlock self)
visits a constructor block

Specified by:
visitConstructorBlock in interface MjcVisitor
Overrides:
visitConstructorBlock in class JmlVisitorNI

visitClassBlock

public void visitClassBlock(JClassBlock self)
visits a class block (initializer)

Specified by:
visitClassBlock in interface MjcVisitor
Overrides:
visitClassBlock in class JmlVisitorNI

visitTypeDeclarationStatement

public void visitTypeDeclarationStatement(JTypeDeclarationStatement self)
visits a type declaration statement

Specified by:
visitTypeDeclarationStatement in interface MjcVisitor
Overrides:
visitTypeDeclarationStatement in class JmlVisitorNI

visitUnaryExpression

public void visitUnaryExpression(JUnaryExpression self)
visits an unary expression

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

visitTypeNameExpression

public void visitTypeNameExpression(JTypeNameExpression self)
visits a type name expression

Specified by:
visitTypeNameExpression in interface MjcVisitor
Overrides:
visitTypeNameExpression in class JmlVisitorNI

visitThisExpression

public void visitThisExpression(JThisExpression self)
visits a this expression

Specified by:
visitThisExpression in interface MjcVisitor
Overrides:
visitThisExpression in class JmlVisitorNI

visitSuperExpression

public void visitSuperExpression(JSuperExpression self)
visits a super expression

Specified by:
visitSuperExpression in interface MjcVisitor
Overrides:
visitSuperExpression in class JmlVisitorNI

visitShiftExpression

public void visitShiftExpression(JShiftExpression self)
visits a shift expression

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

visitRelationalExpression

public void visitRelationalExpression(JRelationalExpression self)
visits a relational expression

Specified by:
visitRelationalExpression in interface MjcVisitor
Overrides:
visitRelationalExpression in class JmlVisitorNI

visitPrefixExpression

public void visitPrefixExpression(JPrefixExpression self)
visits a prefix expression

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

visitPostfixExpression

public void visitPostfixExpression(JPostfixExpression self)
visits a postfix expression

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

visitParenthesedExpression

public void visitParenthesedExpression(JParenthesedExpression self)
visits a parenthesed expression

Specified by:
visitParenthesedExpression in interface MjcVisitor
Overrides:
visitParenthesedExpression in class JmlVisitorNI

visitNewObjectExpression

public void visitNewObjectExpression(JNewObjectExpression self)
visits an object allocator expression

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

visitNewAnonymousClassExpression

public void visitNewAnonymousClassExpression(JNewAnonymousClassExpression self)
visits an object allocator expression for an anonymous class

Specified by:
visitNewAnonymousClassExpression in interface MjcVisitor
Overrides:
visitNewAnonymousClassExpression in class JmlVisitorNI

visitNewArrayExpression

public void visitNewArrayExpression(JNewArrayExpression self)
visits an array allocator expression

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

visitNameExpression

public void visitNameExpression(JNameExpression self)
visits a name expression

Specified by:
visitNameExpression in interface MjcVisitor
Overrides:
visitNameExpression in class JmlVisitorNI

visitAddExpression

public void visitAddExpression(JAddExpression self)
visits an add expression

Specified by:
visitAddExpression in interface MjcVisitor
Overrides:
visitAddExpression in class JmlVisitorNI

visitConditionalAndExpression

public void visitConditionalAndExpression(JConditionalAndExpression self)
visits a boolean AND expression

Specified by:
visitConditionalAndExpression in interface MjcVisitor
Overrides:
visitConditionalAndExpression in class JmlVisitorNI

visitConditionalOrExpression

public void visitConditionalOrExpression(JConditionalOrExpression self)
visits a boolean OR expression

Specified by:
visitConditionalOrExpression in interface MjcVisitor
Overrides:
visitConditionalOrExpression in class JmlVisitorNI

visitDivideExpression

public void visitDivideExpression(JDivideExpression self)
visits a divide expression

Specified by:
visitDivideExpression in interface MjcVisitor
Overrides:
visitDivideExpression in class JmlVisitorNI

visitMinusExpression

public void visitMinusExpression(JMinusExpression self)
visits a minus expression

Specified by:
visitMinusExpression in interface MjcVisitor
Overrides:
visitMinusExpression in class JmlVisitorNI

visitModuloExpression

public void visitModuloExpression(JModuloExpression self)
visits a modulo division expression

Specified by:
visitModuloExpression in interface MjcVisitor
Overrides:
visitModuloExpression in class JmlVisitorNI

visitMultExpression

public void visitMultExpression(JMultExpression self)
visits a multiplication expression

Specified by:
visitMultExpression in interface MjcVisitor
Overrides:
visitMultExpression in class JmlVisitorNI

visitMethodCallExpression

public void visitMethodCallExpression(JMethodCallExpression self)
visits a method call expression

Specified by:
visitMethodCallExpression in interface MjcVisitor
Overrides:
visitMethodCallExpression in class JmlVisitorNI

visitLocalVariableExpression

public void visitLocalVariableExpression(JLocalVariableExpression self)
visits a local variable expression

Specified by:
visitLocalVariableExpression in interface MjcVisitor
Overrides:
visitLocalVariableExpression in class JmlVisitorNI

visitInstanceofExpression

public void visitInstanceofExpression(JInstanceofExpression self)
visits an instanceof expression

Specified by:
visitInstanceofExpression in interface MjcVisitor
Overrides:
visitInstanceofExpression in class JmlVisitorNI

visitEqualityExpression

public void visitEqualityExpression(JEqualityExpression self)
visits an equality expression

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

visitConditionalExpression

public void visitConditionalExpression(JConditionalExpression self)
visits a conditional expression

Specified by:
visitConditionalExpression in interface MjcVisitor
Overrides:
visitConditionalExpression in class JmlVisitorNI

visitCompoundAssignmentExpression

public void visitCompoundAssignmentExpression(JCompoundAssignmentExpression self)
visits a compound expression

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

visitFieldExpression

public void visitFieldExpression(JClassFieldExpression self)
visits a field expression

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

visitClassExpression

public void visitClassExpression(JClassExpression self)
visits a class expression

Specified by:
visitClassExpression in interface MjcVisitor
Overrides:
visitClassExpression in class JmlVisitorNI

visitCastExpression

public void visitCastExpression(JCastExpression self)
visits a cast expression

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

visitUnaryPromoteExpression

public void visitUnaryPromoteExpression(JUnaryPromote self)
visits a cast expression

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

visitBitwiseExpression

public void visitBitwiseExpression(JBitwiseExpression self)
visits a bit operator expression

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

visitAssignmentExpression

public void visitAssignmentExpression(JAssignmentExpression self)
visits an assignment expression

Specified by:
visitAssignmentExpression in interface MjcVisitor
Overrides:
visitAssignmentExpression in class JmlVisitorNI

visitArrayLengthExpression

public void visitArrayLengthExpression(JArrayLengthExpression self)
visits an array length expression

Specified by:
visitArrayLengthExpression in interface MjcVisitor
Overrides:
visitArrayLengthExpression in class JmlVisitorNI

visitArrayAccessExpression

public void visitArrayAccessExpression(JArrayAccessExpression self)
visits an array access expression

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

visitWarnExpression

public void visitWarnExpression(MJWarnExpression self)
visits a warn expression

Specified by:
visitWarnExpression in interface MjcVisitor
Overrides:
visitWarnExpression in class JmlVisitorNI

visitMathModeExpression

public void visitMathModeExpression(MJMathModeExpression self)
visits a math mode expression

Specified by:
visitMathModeExpression in interface MjcVisitor
Overrides:
visitMathModeExpression in class JmlVisitorNI

visitSwitchLabel

public void visitSwitchLabel(JSwitchLabel self)
visits a switch label

Specified by:
visitSwitchLabel in interface MjcVisitor
Overrides:
visitSwitchLabel in class JmlVisitorNI

visitSwitchGroup

public void visitSwitchGroup(JSwitchGroup self)
visits a switch group

Specified by:
visitSwitchGroup in interface MjcVisitor
Overrides:
visitSwitchGroup in class JmlVisitorNI

visitCatchClause

public void visitCatchClause(JCatchClause self)
visits a catch clause

Specified by:
visitCatchClause in interface MjcVisitor
Overrides:
visitCatchClause in class JmlVisitorNI

visitBooleanLiteral

public void visitBooleanLiteral(JBooleanLiteral self)
visits a boolean literal

Specified by:
visitBooleanLiteral in interface MjcVisitor
Overrides:
visitBooleanLiteral in class JmlVisitorNI

visitCharLiteral

public void visitCharLiteral(JCharLiteral self)
visits a character literal

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

visitOrdinalLiteral

public void visitOrdinalLiteral(JOrdinalLiteral self)
prints an ordinal literal

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

visitRealLiteral

public void visitRealLiteral(JRealLiteral self)
prints a real literal

Specified by:
visitRealLiteral in interface MjcVisitor
Overrides:
visitRealLiteral in class JmlVisitorNI

visitStringLiteral

public void visitStringLiteral(JStringLiteral self)
visits a string literal

Specified by:
visitStringLiteral in interface MjcVisitor
Overrides:
visitStringLiteral in class JmlVisitorNI

visitNullLiteral

public void visitNullLiteral(JNullLiteral self)
visits a null literal

Specified by:
visitNullLiteral in interface MjcVisitor
Overrides:
visitNullLiteral in class JmlVisitorNI

visitPackageName

public void visitPackageName(JPackageName self)
visits a package name declaration

Specified by:
visitPackageName in interface MjcVisitor
Overrides:
visitPackageName in class JmlVisitorNI

visitPackageImport

public void visitPackageImport(JPackageImportType self)
visits a package import declaration


visitClassOrGFImport

public void visitClassOrGFImport(JClassOrGFImportType self)
visits a class import declaration


visitFormalParameters

public void visitFormalParameters(JFormalParameter self)
visits a formal parameter

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

visitExplicitConstructorInvocation

public void visitExplicitConstructorInvocation(JExplicitConstructorInvocation self)
visits an explicit constructor invocation

Specified by:
visitExplicitConstructorInvocation in interface MjcVisitor
Overrides:
visitExplicitConstructorInvocation in class JmlVisitorNI

visitArrayInitializer

public void visitArrayInitializer(JArrayInitializer self)
visits an array initializer expression

Specified by:
visitArrayInitializer in interface MjcVisitor
Overrides:
visitArrayInitializer in class JmlVisitorNI

visitArrayDimsAndInit

public void visitArrayDimsAndInit(JArrayDimsAndInits self)
visits an array dimension and initialization expression

Specified by:
visitArrayDimsAndInit in interface MjcVisitor
Overrides:
visitArrayDimsAndInit in class JmlVisitorNI

visitJmlExtendingSpecification

public void visitJmlExtendingSpecification(JmlExtendingSpecification self)
Specified by:
visitJmlExtendingSpecification in interface JmlVisitor
Overrides:
visitJmlExtendingSpecification in class JmlVisitorNI

visitJmlSpecification

public void visitJmlSpecification(JmlSpecification self)
Specified by:
visitJmlSpecification in interface JmlVisitor
Overrides:
visitJmlSpecification in class JmlVisitorNI

visitJmlSpecificationHelper

public void visitJmlSpecificationHelper(JmlSpecCase[] scases,
                                        boolean initialAlso)

visitJmlCodeContract

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

Specified by:
visitJmlCodeContract in interface JmlVisitor
Overrides:
visitJmlCodeContract in class JmlVisitorNI

visitJmlRedundantSpec

public void visitJmlRedundantSpec(JmlRedundantSpec self)
Specified by:
visitJmlRedundantSpec in interface JmlVisitor
Overrides:
visitJmlRedundantSpec in class JmlVisitorNI

visitJmlNode

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

visitJmlSpecExpression

public void visitJmlSpecExpression(JmlSpecExpression self)
Specified by:
visitJmlSpecExpression in interface JmlVisitor
Overrides:
visitJmlSpecExpression in class JmlVisitorNI

visitJmlExpression

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

visitJmlGenericSpecCase

public void visitJmlGenericSpecCase(JmlGenericSpecCase self)
Specified by:
visitJmlGenericSpecCase in interface JmlVisitor
Overrides:
visitJmlGenericSpecCase in class JmlVisitorNI

visitJmlNormalSpecCase

public void visitJmlNormalSpecCase(JmlGenericSpecCase self)

visitJmlExceptionalSpecCase

public void visitJmlExceptionalSpecCase(JmlGenericSpecCase self)

visitJmlRequiresClause

public void visitJmlRequiresClause(JmlRequiresClause self)
Specified by:
visitJmlRequiresClause in interface JmlVisitor
Overrides:
visitJmlRequiresClause in class JmlVisitorNI

visitJmlAssignableClause

public void visitJmlAssignableClause(JmlAssignableClause self)
Specified by:
visitJmlAssignableClause in interface JmlVisitor
Overrides:
visitJmlAssignableClause in class JmlVisitorNI

visitJmlWorkingSpaceClause

public void visitJmlWorkingSpaceClause(JmlWorkingSpaceClause self)
Specified by:
visitJmlWorkingSpaceClause in interface JmlVisitor
Overrides:
visitJmlWorkingSpaceClause in class JmlVisitorNI

visitJmlDurationClause

public void visitJmlDurationClause(JmlDurationClause self)
Specified by:
visitJmlDurationClause in interface JmlVisitor
Overrides:
visitJmlDurationClause in class JmlVisitorNI

visitJmlMeasuredClause

public void visitJmlMeasuredClause(JmlMeasuredClause self)
Specified by:
visitJmlMeasuredClause in interface JmlVisitor
Overrides:
visitJmlMeasuredClause in class JmlVisitorNI

visitJmlWhenClause

public void visitJmlWhenClause(JmlWhenClause self)
Specified by:
visitJmlWhenClause in interface JmlVisitor
Overrides:
visitJmlWhenClause in class JmlVisitorNI

visitJmlEnsuresClause

public void visitJmlEnsuresClause(JmlEnsuresClause self)
Specified by:
visitJmlEnsuresClause in interface JmlVisitor
Overrides:
visitJmlEnsuresClause in class JmlVisitorNI

visitJmlSignalsOnlyClause

public void visitJmlSignalsOnlyClause(JmlSignalsOnlyClause self)
Specified by:
visitJmlSignalsOnlyClause in interface JmlVisitor
Overrides:
visitJmlSignalsOnlyClause in class JmlVisitorNI

visitJmlSignalsClause

public void visitJmlSignalsClause(JmlSignalsClause self)
Specified by:
visitJmlSignalsClause in interface JmlVisitor
Overrides:
visitJmlSignalsClause in class JmlVisitorNI

visitJmlDivergesClause

public void visitJmlDivergesClause(JmlDivergesClause self)
Specified by:
visitJmlDivergesClause in interface JmlVisitor
Overrides:
visitJmlDivergesClause in class JmlVisitorNI

visitJmlAccessibleClause

public void visitJmlAccessibleClause(JmlAccessibleClause self)
Specified by:
visitJmlAccessibleClause in interface JmlVisitor
Overrides:
visitJmlAccessibleClause in class JmlVisitorNI

visitJmlCallableClause

public void visitJmlCallableClause(JmlCallableClause self)
Specified by:
visitJmlCallableClause in interface JmlVisitor
Overrides:
visitJmlCallableClause in class JmlVisitorNI

visitJmlCapturesClause

public void visitJmlCapturesClause(JmlCapturesClause self)
Specified by:
visitJmlCapturesClause in interface JmlVisitor
Overrides:
visitJmlCapturesClause in class JmlVisitorNI

visitJmlGeneralSpecCase

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

visitJmlGeneralSpecCaseHelper

public void visitJmlGeneralSpecCaseHelper(JmlGeneralSpecCase self,
                                          boolean indent)

visitJmlPredicate

public void visitJmlPredicate(JmlPredicate self)
Specified by:
visitJmlPredicate in interface JmlVisitor
Overrides:
visitJmlPredicate in class JmlVisitorNI

visitJmlPredicateKeyword

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

visitJmlPredicateClause

public void visitJmlPredicateClause(JmlPredicateClause self)

visitJmlSpecBody

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

visitJmlSpecBodyClause

public void visitJmlSpecBodyClause(JmlSpecBodyClause self)

visitJmlGenericSpecBody

public void visitJmlGenericSpecBody(JmlGenericSpecBody self)
Specified by:
visitJmlGenericSpecBody in interface JmlVisitor
Overrides:
visitJmlGenericSpecBody in class JmlVisitorNI

visitJmlNormalSpecBody

public void visitJmlNormalSpecBody(JmlNormalSpecBody self)
Specified by:
visitJmlNormalSpecBody in interface JmlVisitor
Overrides:
visitJmlNormalSpecBody in class JmlVisitorNI

visitJmlExceptionalSpecBody

public void visitJmlExceptionalSpecBody(JmlExceptionalSpecBody self)
Specified by:
visitJmlExceptionalSpecBody in interface JmlVisitor
Overrides:
visitJmlExceptionalSpecBody in class JmlVisitorNI

visitJmlResultExpression

public void visitJmlResultExpression(JmlResultExpression self)
Specified by:
visitJmlResultExpression in interface JmlVisitor
Overrides:
visitJmlResultExpression in class JmlVisitorNI

htmlop

public String htmlop(int op,
                     JRelationalExpression s)

visitJmlRelationalExpression

public void visitJmlRelationalExpression(JmlRelationalExpression self)
Specified by:
visitJmlRelationalExpression in interface JmlVisitor
Overrides:
visitJmlRelationalExpression in class JmlVisitorNI

visitJmlFreshExpression

public void visitJmlFreshExpression(JmlFreshExpression self)
Specified by:
visitJmlFreshExpression in interface JmlVisitor
Overrides:
visitJmlFreshExpression in class JmlVisitorNI

visitJmlIsInitializedExpression

public void visitJmlIsInitializedExpression(JmlIsInitializedExpression self)
Specified by:
visitJmlIsInitializedExpression in interface JmlVisitor
Overrides:
visitJmlIsInitializedExpression in class JmlVisitorNI

visitJmlLabelExpression

public void visitJmlLabelExpression(JmlLabelExpression self)
Specified by:
visitJmlLabelExpression in interface JmlVisitor
Overrides:
visitJmlLabelExpression in class JmlVisitorNI

visitJmlLockSetExpression

public void visitJmlLockSetExpression(JmlLockSetExpression self)
Specified by:
visitJmlLockSetExpression in interface JmlVisitor
Overrides:
visitJmlLockSetExpression in class JmlVisitorNI

visitJmlReachExpression

public void visitJmlReachExpression(JmlReachExpression self)
Specified by:
visitJmlReachExpression in interface JmlVisitor
Overrides:
visitJmlReachExpression in class JmlVisitorNI

visitJmlSpecQuantifiedExpression

public void visitJmlSpecQuantifiedExpression(JmlSpecQuantifiedExpression self)
Specified by:
visitJmlSpecQuantifiedExpression in interface JmlVisitor
Overrides:
visitJmlSpecQuantifiedExpression in class JmlVisitorNI

visitJmlTypeExpression

public void visitJmlTypeExpression(JmlTypeExpression self)
Specified by:
visitJmlTypeExpression in interface JmlVisitor
Overrides:
visitJmlTypeExpression in class JmlVisitorNI

visitJmlOldExpression

public void visitJmlOldExpression(JmlOldExpression self)
Specified by:
visitJmlOldExpression in interface JmlVisitor
Overrides:
visitJmlOldExpression in class JmlVisitorNI

visitJmlPreExpression

public void visitJmlPreExpression(JmlPreExpression self)
Specified by:
visitJmlPreExpression in interface JmlVisitor
Overrides:
visitJmlPreExpression in class JmlVisitorNI

visitJmlMaxExpression

public void visitJmlMaxExpression(JmlMaxExpression self)
Specified by:
visitJmlMaxExpression in interface JmlVisitor
Overrides:
visitJmlMaxExpression in class JmlVisitorNI

visitJmlDurationExpression

public void visitJmlDurationExpression(JmlDurationExpression self)
Specified by:
visitJmlDurationExpression in interface JmlVisitor
Overrides:
visitJmlDurationExpression in class JmlVisitorNI

visitJmlSpaceExpression

public void visitJmlSpaceExpression(JmlSpaceExpression self)
Specified by:
visitJmlSpaceExpression in interface JmlVisitor
Overrides:
visitJmlSpaceExpression in class JmlVisitorNI

visitJmlWorkingSpaceExpression

public void visitJmlWorkingSpaceExpression(JmlWorkingSpaceExpression self)
Specified by:
visitJmlWorkingSpaceExpression in interface JmlVisitor
Overrides:
visitJmlWorkingSpaceExpression in class JmlVisitorNI

visitJmlNotModifiedExpression

public void visitJmlNotModifiedExpression(JmlNotModifiedExpression self)
Specified by:
visitJmlNotModifiedExpression in interface JmlVisitor
Overrides:
visitJmlNotModifiedExpression in class JmlVisitorNI

visitJmlNotAssignedExpression

public void visitJmlNotAssignedExpression(JmlNotAssignedExpression self)
Specified by:
visitJmlNotAssignedExpression in interface JmlVisitor
Overrides:
visitJmlNotAssignedExpression in class JmlVisitorNI

visitJmlOnlyAssignedExpression

public void visitJmlOnlyAssignedExpression(JmlOnlyAssignedExpression self)
Specified by:
visitJmlOnlyAssignedExpression in interface JmlVisitor
Overrides:
visitJmlOnlyAssignedExpression in class JmlVisitorNI

visitJmlNonNullElementsExpression

public void visitJmlNonNullElementsExpression(JmlNonNullElementsExpression self)
Specified by:
visitJmlNonNullElementsExpression in interface JmlVisitor
Overrides:
visitJmlNonNullElementsExpression in class JmlVisitorNI

visitJmlTypeOfExpression

public void visitJmlTypeOfExpression(JmlTypeOfExpression self)
Specified by:
visitJmlTypeOfExpression in interface JmlVisitor
Overrides:
visitJmlTypeOfExpression in class JmlVisitorNI

visitJmlElemTypeExpression

public void visitJmlElemTypeExpression(JmlElemTypeExpression self)
Specified by:
visitJmlElemTypeExpression in interface JmlVisitor
Overrides:
visitJmlElemTypeExpression in class JmlVisitorNI

visitJmlInvariantForExpression

public void visitJmlInvariantForExpression(JmlInvariantForExpression self)
Specified by:
visitJmlInvariantForExpression in interface JmlVisitor
Overrides:
visitJmlInvariantForExpression in class JmlVisitorNI

visitJmlStoreRef

public void visitJmlStoreRef(JmlStoreRef self)
Specified by:
visitJmlStoreRef in interface JmlVisitor
Overrides:
visitJmlStoreRef in class JmlVisitorNI

visitJmlStoreRefExpression

public void visitJmlStoreRefExpression(JmlStoreRefExpression self)
Specified by:
visitJmlStoreRefExpression in interface JmlVisitor
Overrides:
visitJmlStoreRefExpression in class JmlVisitorNI

visitJmlInformalStoreRef

public void visitJmlInformalStoreRef(JmlInformalStoreRef self)
Specified by:
visitJmlInformalStoreRef in interface JmlVisitor
Overrides:
visitJmlInformalStoreRef in class JmlVisitorNI

visitJmlName

public void visitJmlName(JmlName self)
Specified by:
visitJmlName in interface JmlVisitor
Overrides:
visitJmlName in class JmlVisitorNI

visitJmlNameHelper

public void visitJmlNameHelper(JmlName self,
                               boolean addDot)

visitJmlStoreRefKeyword

public void visitJmlStoreRefKeyword(JmlStoreRefKeyword self)
Specified by:
visitJmlStoreRefKeyword in interface JmlVisitor
Overrides:
visitJmlStoreRefKeyword in class JmlVisitorNI

writePrivacy

static void writePrivacy(StringBuffer sb,
                         long p)

writeModifiers

static void writeModifiers(StringBuffer sb,
                           long p)

visitJmlBehaviorSpecHelper

public void visitJmlBehaviorSpecHelper(JmlHeavyweightSpec self,
                                       String s)

visitJmlBehaviorSpec

public void visitJmlBehaviorSpec(JmlBehaviorSpec self)
Specified by:
visitJmlBehaviorSpec in interface JmlVisitor
Overrides:
visitJmlBehaviorSpec in class JmlVisitorNI

visitJmlNormalBehaviorSpec

public void visitJmlNormalBehaviorSpec(JmlNormalBehaviorSpec self)
Specified by:
visitJmlNormalBehaviorSpec in interface JmlVisitor
Overrides:
visitJmlNormalBehaviorSpec in class JmlVisitorNI

visitJmlExceptionalBehaviorSpec

public void visitJmlExceptionalBehaviorSpec(JmlExceptionalBehaviorSpec self)
Specified by:
visitJmlExceptionalBehaviorSpec in interface JmlVisitor
Overrides:
visitJmlExceptionalBehaviorSpec in class JmlVisitorNI

visitJmlModelProgram

public void visitJmlModelProgram(JmlModelProgram self)
Specified by:
visitJmlModelProgram in interface JmlVisitor
Overrides:
visitJmlModelProgram in class JmlVisitorNI

visitJmlAssignmentStatement

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

visitJmlNondetChoiceStatement

public void visitJmlNondetChoiceStatement(JmlNondetChoiceStatement self)
Specified by:
visitJmlNondetChoiceStatement in interface JmlVisitor
Overrides:
visitJmlNondetChoiceStatement in class JmlVisitorNI

visitJmlNondetIfStatement

public void visitJmlNondetIfStatement(JmlNondetIfStatement self)
Specified by:
visitJmlNondetIfStatement in interface JmlVisitor
Overrides:
visitJmlNondetIfStatement in class JmlVisitorNI

visitJmlGuardedStatement

public void visitJmlGuardedStatement(JmlGuardedStatement self)
Specified by:
visitJmlGuardedStatement in interface JmlVisitor
Overrides:
visitJmlGuardedStatement in class JmlVisitorNI

visitJmlSpecVarDecl

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

visitJmlForAllVarDecl

public void visitJmlForAllVarDecl(JmlForAllVarDecl self)
Specified by:
visitJmlForAllVarDecl in interface JmlVisitor
Overrides:
visitJmlForAllVarDecl in class JmlVisitorNI

visitJmlLetVarDecl

public void visitJmlLetVarDecl(JmlLetVarDecl self)
Specified by:
visitJmlLetVarDecl in interface JmlVisitor
Overrides:
visitJmlLetVarDecl in class JmlVisitorNI

visitFieldDeclaration

public void visitFieldDeclaration(JFieldDeclaration self)
Description copied from class: JmlVisitorNI
visits a field declaration

Specified by:
visitFieldDeclaration in interface MjcVisitor
Overrides:
visitFieldDeclaration in class JmlVisitorNI

visitJmlFieldDeclaration

public void visitJmlFieldDeclaration(JmlFieldDeclaration self)
Specified by:
visitJmlFieldDeclaration in interface JmlVisitor
Overrides:
visitJmlFieldDeclaration in class JmlVisitorNI

visitJmlInitiallyVarAssertion

public void visitJmlInitiallyVarAssertion(JmlInitiallyVarAssertion self)
Specified by:
visitJmlInitiallyVarAssertion in interface JmlVisitor
Overrides:
visitJmlInitiallyVarAssertion in class JmlVisitorNI

visitJmlReadableIfVarAssertion

public void visitJmlReadableIfVarAssertion(JmlReadableIfVarAssertion self)
Specified by:
visitJmlReadableIfVarAssertion in interface JmlVisitor
Overrides:
visitJmlReadableIfVarAssertion in class JmlVisitorNI

visitJmlWritableIfVarAssertion

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

visitJmlMonitorsForVarAssertion

public void visitJmlMonitorsForVarAssertion(JmlMonitorsForVarAssertion self)
Specified by:
visitJmlMonitorsForVarAssertion in interface JmlVisitor
Overrides:
visitJmlMonitorsForVarAssertion in class JmlVisitorNI

visitJmlInformalExpression

public void visitJmlInformalExpression(JmlInformalExpression self)
Specified by:
visitJmlInformalExpression in interface JmlVisitor
Overrides:
visitJmlInformalExpression in class JmlVisitorNI

visitJmlAxiom

public void visitJmlAxiom(JmlAxiom self)
Specified by:
visitJmlAxiom in interface JmlVisitor
Overrides:
visitJmlAxiom in class JmlVisitorNI

visitJmlDeclaration

public void visitJmlDeclaration(JmlDeclaration self)
This method gets called only if a derived class does not implement accept.

Specified by:
visitJmlDeclaration in interface JmlVisitor
Overrides:
visitJmlDeclaration in class JmlVisitorNI

visitJmlInvariant

public void visitJmlInvariant(JmlInvariant self)
Specified by:
visitJmlInvariant in interface JmlVisitor
Overrides:
visitJmlInvariant in class JmlVisitorNI

visitJmlConstraint

public void visitJmlConstraint(JmlConstraint self)
Specified by:
visitJmlConstraint in interface JmlVisitor
Overrides:
visitJmlConstraint in class JmlVisitorNI

visitJmlRepresentsDecl

public void visitJmlRepresentsDecl(JmlRepresentsDecl self)
Specified by:
visitJmlRepresentsDecl in interface JmlVisitor
Overrides:
visitJmlRepresentsDecl in class JmlVisitorNI

visitJmlMethodNameList

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

visitJmlMethodName

public void visitJmlMethodName(JmlMethodName self)
Specified by:
visitJmlMethodName in interface JmlVisitor
Overrides:
visitJmlMethodName in class JmlVisitorNI

visitJmlConstructorName

public void visitJmlConstructorName(JmlConstructorName self)
Specified by:
visitJmlConstructorName in interface JmlVisitor
Overrides:
visitJmlConstructorName in class JmlVisitorNI

visitJmlSetComprehension

public void visitJmlSetComprehension(JmlSetComprehension self)
Specified by:
visitJmlSetComprehension in interface JmlVisitor
Overrides:
visitJmlSetComprehension in class JmlVisitorNI

visitJmlExample

public void visitJmlExample(JmlExample self)
Specified by:
visitJmlExample in interface JmlVisitor
Overrides:
visitJmlExample in class JmlVisitorNI

visitJmlNormalExample

public void visitJmlNormalExample(JmlNormalExample self)
Specified by:
visitJmlNormalExample in interface JmlVisitor
Overrides:
visitJmlNormalExample in class JmlVisitorNI

visitJmlExceptionalExample

public void visitJmlExceptionalExample(JmlExceptionalExample self)
Specified by:
visitJmlExceptionalExample in interface JmlVisitor
Overrides:
visitJmlExceptionalExample in class JmlVisitorNI

visitJmlExampleHelper

public void visitJmlExampleHelper(JmlExample self,
                                  String title)

jmlModifiers

public static String jmlModifiers(long mods)

removeBR

public static void removeBR(StringBuffer classspec)
This method removes a "
"+eol combination from the end of the given StringBuffer, if it is present.


convertToHtml

public String convertToHtml(String s)
Copies the input string to the output, replacing instances of special html characters by html representations (less than symbols, greater than symbols, ampersands).


replace

private String replace(String s,
                       char c,
                       String rep)

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.