org.jmlspecs.jmldoc.jmldoc_142
Class SpecWriter

java.lang.Object
  org.jmlspecs.checker.JmlVisitorNI
      org.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_NON_NULL, ACC_NON_NULL_BY_DEFAULT, ACC_NULLABLE, ACC_NULLABLE_BY_DEFAULT, ACC_QUERY, ACC_SECRET, ACC_SPEC_BIGINT_MATH, ACC_SPEC_JAVA_MATH, ACC_SPEC_PROTECTED, ACC_SPEC_PUBLIC, ACC_SPEC_SAFE_MATH, ACC_UNINITIALIZED, ACCESS_FLAG_ARRAY, ACCESS_FLAG_NAMES, AMID_BIGINT_MATH, EVERYTHING, JML_JMLObjectSet, NOT_SPECIFIED, NOTHING, OPE_BACKWARD_IMPLIES, OPE_EQUIV, OPE_EXISTS, OPE_FORALL, OPE_IMPLIES, OPE_L_ARROW, OPE_MAX, OPE_MIN, OPE_NOT_EQUIV, OPE_NUM_OF, OPE_PRODUCT, OPE_R_ARROW, OPE_SUBTYPE, OPE_SUM, SAME, TID_BIGINT, TID_REAL, TID_TYPE, TN_JMLOBJECTSET, TN_JMLTYPE, TN_JMLVALUESET

 

Fields inherited from interface org.multijava.mjc.Constants

ACC_PURE, AMID_JAVA_MATH, AMID_MAX, AMID_SAFE_MATH, CMP_VERSION, JAV_ASSERTION_ERROR, JAV_CLASS, JAV_CLASSLOADER, JAV_CLASSNOTFOUND_EXCEPTION, JAV_CLONE, JAV_CLONEABLE, JAV_CONSTRUCTOR, JAV_ERROR, JAV_EXCEPTION, JAV_INIT, JAV_LENGTH, JAV_NAME_SEPARATOR, JAV_NOCLASSDEFFOUND_ERROR, JAV_OBJECT, JAV_OUTER_THIS, JAV_RMJ_RUNTIME_EXCEPTION, JAV_RUNTIME, JAV_RUNTIME_EXCEPTION, JAV_SERIALIZABLE, JAV_STATIC_INIT, JAV_STRING, JAV_STRINGBUFFER, JAV_SUPER, JAV_THIS, JAV_THROWABLE, MJ_ANCHOR, OPE_BAND, OPE_BNOT, OPE_BOR, OPE_BSR, OPE_BXOR, OPE_EQ, OPE_GE, OPE_GT, OPE_LAND, OPE_LE, OPE_LNOT, OPE_LOR, OPE_LT, OPE_MINUS, OPE_NE, OPE_PERCENT, OPE_PLUS, OPE_POSTDEC, OPE_POSTINC, OPE_PREDEC, OPE_PREINC, OPE_SIMPLE, OPE_SL, OPE_SLASH, OPE_SR, OPE_STAR, TID_ARRAY, TID_BOOLEAN, TID_BYTE, TID_CHAR, TID_CLASS, TID_DOUBLE, TID_FLOAT, TID_INT, TID_LONG, TID_MAX, TID_SHORT, TID_VOID, UNIV_ARRAY_TMP, UNIV_TMP

 

Fields inherited from interface org.multijava.util.classfile.Constants

ACC_ABSTRACT, ACC_FINAL, ACC_INTERFACE, ACC_NATIVE, ACC_PRIVATE, ACC_PROTECTED, ACC_PUBLIC, ACC_STATIC, ACC_STRICT, ACC_SUPER, ACC_SYNCHRONIZED, ACC_TRANSIENT, ACC_VOLATILE, ATT_ANCHOR, ATT_BRIDGE, ATT_CODE, ATT_CONSTANTVALUE, ATT_DEPRECATED, ATT_DISPATCHER, ATT_EXCEPTIONS, ATT_GENERIC, ATT_GENERIC_FUNCTIONS, ATT_INNERCLASSES, ATT_LINENUMBERTABLE, ATT_LOCALVARIABLETABLE, ATT_MM_BODY, ATT_REDIRECTOR, ATT_RMJ_GLUE, ATT_RMJ_SIGNATURE, ATT_RUNTIME_VISIBLE_ANNOTATIONS, ATT_RUNTIME_VISIBLE_PARAMETER_ANNOTATIONS, ATT_SIGNATURE, ATT_SOURCEFILE, ATT_SYNTHETIC, ATT_UNIVERSE_FIELD, ATT_UNIVERSE_METHOD, ATT_UNIVERSE_VERSION, CST_CLASS, CST_DOUBLE, CST_FIELD, CST_FLOAT, CST_INTEGER, CST_INTERFACEMETHOD, CST_LONG, CST_METHOD, CST_NAMEANDTYPE, CST_STRING, CST_UTF8, ENV_DEBUG_MODE, ENV_USE_CACHE, JAVA_MAGIC, JAVA_MAJOR, JAVA_MINOR, MAX_CODE_PER_METHOD, opc_aaload, opc_aastore, opc_aconst_null, opc_aload, opc_aload_0, opc_aload_1, opc_aload_2, opc_aload_3, opc_anewarray, opc_areturn, opc_arraylength, opc_astore, opc_astore_0, opc_astore_1, opc_astore_2, opc_astore_3, opc_athrow, opc_baload, opc_bastore, opc_bipush, opc_caload, opc_castore, opc_checkcast, opc_d2f, opc_d2i, opc_d2l, opc_dadd, opc_daload, opc_dastore, opc_dcmpg, opc_dcmpl, opc_dconst_0, opc_dconst_1, opc_ddiv, opc_dload, opc_dload_0, opc_dload_1, opc_dload_2, opc_dload_3, opc_dmul, opc_dneg, opc_drem, opc_dreturn, opc_dstore, opc_dstore_0, opc_dstore_1, opc_dstore_2, opc_dstore_3, opc_dsub, opc_dup, opc_dup2, opc_dup2_x1, opc_dup2_x2, opc_dup_x1, opc_dup_x2, opc_f2d, opc_f2i, opc_f2l, opc_fadd, opc_faload, opc_fastore, opc_fcmpg, opc_fcmpl, opc_fconst_0, opc_fconst_1, opc_fconst_2, opc_fdiv, opc_fload, opc_fload_0, opc_fload_1, opc_fload_2, opc_fload_3, opc_fmul, opc_fneg, opc_frem, opc_freturn, opc_fstore, opc_fstore_0, opc_fstore_1, opc_fstore_2, opc_fstore_3, opc_fsub, opc_getfield, opc_getstatic, opc_goto, opc_goto_w, opc_i2b, opc_i2c, opc_i2d, opc_i2f, opc_i2l, opc_i2s, opc_iadd, opc_iaload, opc_iand, opc_iastore, opc_iconst_0, opc_iconst_1, opc_iconst_2, opc_iconst_3, opc_iconst_4, opc_iconst_5, opc_iconst_m1, opc_idiv, opc_if_acmpeq, opc_if_acmpne, opc_if_icmpeq, opc_if_icmpge, opc_if_icmpgt, opc_if_icmple, opc_if_icmplt, opc_if_icmpne, opc_ifeq, opc_ifge, opc_ifgt, opc_ifle, opc_iflt, opc_ifne, opc_ifnonnull, opc_ifnull, opc_iinc, opc_iload, opc_iload_0, opc_iload_1, opc_iload_2, opc_iload_3, opc_imul, opc_ineg, opc_instanceof, opc_invokeinterface, opc_invokespecial, opc_invokestatic, opc_invokevirtual, opc_ior, opc_irem, opc_ireturn, opc_ishl, opc_ishr, opc_istore, opc_istore_0, opc_istore_1, opc_istore_2, opc_istore_3, opc_isub, opc_iushr, opc_ixor, opc_jsr, opc_jsr_w, opc_l2d, opc_l2f, opc_l2i, opc_ladd, opc_laload, opc_land, opc_lastore, opc_lcmp, opc_lconst_0, opc_lconst_1, opc_ldc, opc_ldc2_w, opc_ldc_w, opc_ldiv, opc_lload, opc_lload_0, opc_lload_1, opc_lload_2, opc_lload_3, opc_lmul, opc_lneg, opc_lookupswitch, opc_lor, opc_lrem, opc_lreturn, opc_lshl, opc_lshr, opc_lstore, opc_lstore_0, opc_lstore_1, opc_lstore_2, opc_lstore_3, opc_lsub, opc_lushr, opc_lxor, opc_monitorenter, opc_monitorexit, opc_multianewarray, opc_new, opc_newarray, opc_nop, opc_pop, opc_pop2, opc_putfield, opc_putstatic, opc_ret, opc_return, opc_saload, opc_sastore, opc_sipush, opc_swap, opc_tableswitch, opc_wide, opc_xxxunusedxxx, POO_ASCII_CONSTANT, POO_CLASS_CONSTANT, POO_DOUBLE_CONSTANT, POO_FLOAT_CONSTANT, POO_INTEGER_CONSTANT, POO_LONG_CONSTANT, POO_NAT_CONSTANT, POO_REF_CONSTANT, POO_STRING_CONSTANT, TYP_ADDRESS, TYP_DOUBLE, TYP_FLOAT, TYP_INT, TYP_LONG, TYP_REFERENCE, TYP_VOID

 

Constructor Summary
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	visitJmlOtherRef(JmlOtherRef 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

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.

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

visitJmlOtherRef

public void visitJmlOtherRef(JmlOtherRef self)

Specified by:

visitJmlOtherRef in interface JmlVisitor

Overrides:

visitJmlOtherRef 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)