org.jmlspecs.jml4.rac
Interface JmlAstVisitor

All Superinterfaces:

JavaAstVisitor

All Known Subinterfaces:

RacAstVisitor

All Known Implementing Classes:

AstDirtyBitsRestorer, AstDirtyBitsRetriever, DefaultRacAstVisitor, DesugarSpec, JmlNullifier, ResolutionNullifier

public interface JmlAstVisitor
extends JavaAstVisitor

An AST Visitor interface for visiting every Jml-type node.

Author:

Amritam Sarcar

Method Summary

void	endVisit(JmlAllocationExpression allocationExpression, BlockScope scope)
void	endVisit(JmlArrayQualifiedTypeReference arrayQualifiedTypeReference, BlockScope scope)
void	endVisit(JmlArrayQualifiedTypeReference arrayQualifiedTypeReference, ClassScope scope)
void	endVisit(JmlArrayReference arrayReference, BlockScope scope)
void	endVisit(JmlArrayTypeReference arrayTypeReference, BlockScope scope)
void	endVisit(JmlArrayTypeReference arrayTypeReference, ClassScope scope)
void	endVisit(JmlAssertOrAssumeStatement assertOrAssumeStatement, BlockScope scope)
void	endVisit(JmlAssertStatement assertStatement, BlockScope scope)
void	endVisit(JmlAssignableClause jmlAssignableClause, BlockScope scope)
void	endVisit(JmlAssignment assignment, BlockScope scope)
void	endVisit(JmlAssumeStatement assumeStatement, BlockScope scope)
void	endVisit(JmlBooleanQuantifier jmlBooleanQuantifier, BlockScope scope)
void	endVisit(JmlCastExpression castExpression, BlockScope scope)
void	endVisit(JmlCastExpressionWithoutType castExpression, BlockScope scope)
void	endVisit(JmlClause jmlClause, BlockScope scope)
void	endVisit(JmlClinit clinit, ClassScope scope)
void	endVisit(JmlCompilationUnitDeclaration compilationUnitDeclaration, CompilationUnitScope scope)
void	endVisit(JmlConditionalExpression conditionalExpression, BlockScope scope)
void	endVisit(JmlConstraintClause jmlConstraintClause, BlockScope scope)
void	endVisit(JmlConstructorDeclaration constructorDeclaration, ClassScope scope)
void	endVisit(JmlDoStatement doStatement, BlockScope scope)
void	endVisit(JmlElemtypeExpression jmlElemtypeExpression, BlockScope scope)
void	endVisit(JmlEnsuresClause ensuresClause, BlockScope scope)
void	endVisit(JmlExplicitConstructorCall jmlExplicitConstructorCall, BlockScope scope)
void	endVisit(JmlFieldDeclaration fieldDeclaration, MethodScope scope)
void	endVisit(JmlFieldReference fieldReference, BlockScope scope)
void	endVisit(JmlFieldReference fieldReference, ClassScope scope)
void	endVisit(JmlForStatement forStatement, BlockScope scope)
void	endVisit(JmlFreshExpression jmlFreshExpression, BlockScope scope)
void	endVisit(JmlGroupName jmlGroupName, BlockScope scope)
void	endVisit(JmlInitiallyClause jmlInitiallyClause, CompilationUnitScope scope)
void	endVisit(JmlInvariantForType jmlInvariantForType, CompilationUnitScope scope)
void	endVisit(JmlLocalDeclaration localDeclaration, BlockScope scope)
void	endVisit(JmlLoopAnnotations jmlLoopAnnotations, BlockScope scope)
void	endVisit(JmlLoopInvariant jmlLoopInvariant, BlockScope scope)
void	endVisit(JmlLoopVariant jmlLoopVariant, BlockScope scope)
void	endVisit(JmlMapsIntoClause jmlMapsIntoClause, BlockScope scope)
void	endVisit(JmlMapsMemberRefExpr jmlMapsMemberRefExpr, BlockScope scope)
void	endVisit(JmlMemberFieldRef jmlMemberFieldRef, BlockScope scope)
void	endVisit(JmlMessageSend messageSend, BlockScope scope)
void	endVisit(JmlMethodDeclaration methodDeclaration, ClassScope scope)
void	endVisit(JmlMethodSpecification jmlMethodSpecification, BlockScope scope)
void	endVisit(JmlMethodSpecification jmlMethodSpecification, ClassScope classScope)
void	endVisit(JmlModifier jmlModifier, BlockScope scope)
void	endVisit(JmlName jmlName, BlockScope scope)
void	endVisit(JmlNumericQuantifier jmlNumericQuantifier, BlockScope scope)
void	endVisit(JmlOldExpression jmlOldExpression, BlockScope scope)
void	endVisit(JmlParameterizedQualifiedTypeReference parameterizedQualifiedTypeReference, BlockScope scope)
void	endVisit(JmlParameterizedQualifiedTypeReference parameterizedQualifiedTypeReference, ClassScope scope)
void	endVisit(JmlParameterizedSingleTypeReference parameterizedSingleTypeReference, BlockScope scope)
void	endVisit(JmlParameterizedSingleTypeReference parameterizedSingleTypeReference, ClassScope scope)
void	endVisit(JmlQualifiedNameReference qualifiedNameReference, BlockScope scope)
void	endVisit(JmlQualifiedNameReference qualifiedNameReference, ClassScope scope)
void	endVisit(JmlQualifiedTypeReference qualifiedTypeReference, BlockScope scope)
void	endVisit(JmlQualifiedTypeReference qualifiedTypeReference, ClassScope scope)
void	endVisit(JmlQuantifiedExpression jmlQuantifiedExpression, BlockScope blockScope)
void	endVisit(JmlRepresentsClause representsClause, CompilationUnitScope scope)
void	endVisit(JmlRequiresClause requiresClause, BlockScope scope)
void	endVisit(JmlResultReference resultReference, BlockScope scope)
void	endVisit(JmlReturnStatement returnStatement, BlockScope scope)
void	endVisit(JmlSetComprehension jmlSetComprehension, BlockScope scope)
boolean	endVisit(JmlSetStatement jmlSetStatement, BlockScope scope)
void	endVisit(JmlSignalsClause jmlSignalsClause, BlockScope scope)
void	endVisit(JmlSignalsOnlyClause jmlSignalsOnlyClause, BlockScope scope)
void	endVisit(JmlSingleNameReference singleNameReference, BlockScope scope)
void	endVisit(JmlSingleNameReference singleNameReference, ClassScope scope)
void	endVisit(JmlSingleTypeReference singleTypeReference, BlockScope scope)
void	endVisit(JmlSingleTypeReference singleTypeReference, ClassScope scope)
void	endVisit(JmlSpecCaseBlock jmlSpecCaseBlock, BlockScope scope)
void	endVisit(JmlSpecCase jmlSpecCase, BlockScope scope)
void	endVisit(JmlSpecCaseBody jmlSpecCaseBody, BlockScope scope)
void	endVisit(JmlSpecCaseHeader jmlSpecCaseHeader, BlockScope scope)
void	endVisit(JmlSpecCaseRestAsClauseSeq jmlSpecCaseRestAsClauseSeq, BlockScope scope)
void	endVisit(JmlStoreRefExpression jmlStoreRefExpression, BlockScope scope)
void	endVisit(JmlSubtypeExpression jmlSubtypeExpression, BlockScope scope)
void	endVisit(JmlTypeBodyDeclaration jmlTypeDecle, BlockScope scope)
void	endVisit(JmlTypeDeclaration typeDecle, CompilationUnitScope scope)
void	endVisit(JmlTypeExpression expression, BlockScope scope)
void	endVisit(JmlTypeofExpression jmlTypeofExpression, BlockScope scope)
void	endVisit(JmlUnaryExpression unaryExpression, BlockScope scope)
void	endVisit(JmlWhileStatement whileStatement, BlockScope scope)
void	endVisit(JmlWildcard wildcard, BlockScope scope)
void	endVisit(JmlWildcard wildcard, ClassScope scope)
boolean	visit(JmlAllocationExpression allocationExpression, BlockScope scope)
boolean	visit(JmlArrayQualifiedTypeReference arrayQualifiedTypeReference, BlockScope scope)
boolean	visit(JmlArrayQualifiedTypeReference arrayQualifiedTypeReference, ClassScope scope)
boolean	visit(JmlArrayReference arrayReference, BlockScope scope)
boolean	visit(JmlArrayTypeReference arrayTypeReference, BlockScope scope)
boolean	visit(JmlArrayTypeReference arrayTypeReference, ClassScope scope)
boolean	visit(JmlAssertOrAssumeStatement assertOrAssumeStatement, BlockScope scope)
boolean	visit(JmlAssertStatement assertStatement, BlockScope scope) Inside an annotation, an assert statement is JML assert statement.
boolean	visit(JmlAssignableClause jmlAssignableClause, BlockScope scope) Gives a frame axiom for a specification.
boolean	visit(JmlAssignment assignment, BlockScope scope)
boolean	visit(JmlAssumeStatement assumeStatement, BlockScope scope) Statements which are assumed to be true (in static analysis tools).
boolean	visit(JmlBooleanQuantifier jmlBooleanQuantifier, BlockScope scope)
boolean	visit(JmlCastExpression castExpression, BlockScope scope)
boolean	visit(JmlCastExpressionWithoutType castExpression, BlockScope scope)
boolean	visit(JmlClause jmlClause, BlockScope scope)
boolean	visit(JmlClinit clinit, ClassScope scope)
boolean	visit(JmlCompilationUnitDeclaration compilationUnitDeclaration, CompilationUnitScope scope)
boolean	visit(JmlConditionalExpression conditionalExpression, BlockScope scope)
boolean	visit(JmlConstraintClause jmlConstraintClause, BlockScope scope) Are relationships that should hold for the combination of each visible state and any visible state that occurs later in the programÕs execution.
boolean	visit(JmlConstructorDeclaration constructorDeclaration, ClassScope scope)
boolean	visit(JmlDoStatement doStatement, BlockScope scope)
boolean	visit(JmlElemtypeExpression jmlElemtypeExpression, BlockScope scope)
boolean	visit(JmlEnsuresClause ensuresClause, BlockScope scope) An ensures clause specifies a normal postcondition, i.e., a property that is guaranteed to hold at the end of the method (or constructor) invocation in the case that this method (or constructor) invocation returns without throwing an exception.
boolean	visit(JmlExplicitConstructorCall jmlExplicitConstructorCall, BlockScope scope)
boolean	visit(JmlFieldDeclaration fieldDeclaration, MethodScope scope)
boolean	visit(JmlFieldReference fieldReference, BlockScope scope)
boolean	visit(JmlFieldReference fieldReference, ClassScope scope)
boolean	visit(JmlForStatement forStatement, BlockScope scope)
boolean	visit(JmlFreshExpression jmlFreshExpression, BlockScope scope) Asserts that objects were freshly allocated.
boolean	visit(JmlGroupName jmlGroupName, BlockScope scope)
boolean	visit(JmlInitiallyClause jmlInitiallyClause, CompilationUnitScope scope) Is used to specify the initial state of model fields.
boolean	visit(JmlInvariantForType jmlInvariantForType, CompilationUnitScope scope) Properties that have to hold in all visible states.
boolean	visit(JmlLocalDeclaration localDeclaration, BlockScope scope)
boolean	visit(JmlLoopAnnotations jmlLoopAnnotations, BlockScope scope)
boolean	visit(JmlLoopInvariant jmlLoopInvariant, BlockScope scope) Is used to help prove partial correctness of a loop statement.
boolean	visit(JmlLoopVariant jmlLoopVariant, BlockScope scope) Is used to help prove termination of a loop statement.
boolean	visit(JmlMapsIntoClause jmlMapsIntoClause, BlockScope scope)
boolean	visit(JmlMapsMemberRefExpr jmlMapsMemberRefExpr, BlockScope scope)
boolean	visit(JmlMemberFieldRef jmlMemberFieldRef, BlockScope scope)
boolean	visit(JmlMessageSend messageSend, BlockScope scope)
boolean	visit(JmlMethodDeclaration methodDeclaration, ClassScope scope)
boolean	visit(JmlMethodSpecification jmlMethodSpecification, BlockScope scope)
boolean	visit(JmlMethodSpecification jmlMethodSpecification, ClassScope classScope)
boolean	visit(JmlModifier jmlModifier, BlockScope scope) In addition to the Java modifiers that can be legally attached to a class or interface definition [Gosling-etal00], in JML one can use the following modifiers.
boolean	visit(JmlName jmlName, BlockScope scope)
boolean	visit(JmlNumericQuantifier jmlNumericQuantifier, BlockScope scope)
boolean	visit(JmlOldExpression jmlOldExpression, BlockScope scope) Refers to the value that the expression had in the pre-state of a method.
boolean	visit(JmlParameterizedQualifiedTypeReference parameterizedQualifiedTypeReference, BlockScope scope)
boolean	visit(JmlParameterizedQualifiedTypeReference parameterizedQualifiedTypeReference, ClassScope scope)
boolean	visit(JmlParameterizedSingleTypeReference parameterizedSingleTypeReference, BlockScope scope)
boolean	visit(JmlParameterizedSingleTypeReference parameterizedSingleTypeReference, ClassScope scope)
boolean	visit(JmlQualifiedNameReference qualifiedNameReference, BlockScope scope)
boolean	visit(JmlQualifiedNameReference qualifiedNameReference, ClassScope scope)
boolean	visit(JmlQualifiedTypeReference qualifiedTypeReference, BlockScope scope)
boolean	visit(JmlQualifiedTypeReference qualifiedTypeReference, ClassScope scope)
boolean	visit(JmlQuantifiedExpression jmlQuantifiedExpression, BlockScope blockScope)
boolean	visit(JmlRepresentsClause representsClause, CompilationUnitScope scope) The first form of represents clauses (with <- or =) is called a functional abstraction.
boolean	visit(JmlRequiresClause requiresClause, BlockScope scope) Specifies a precondition of method or constructor.
boolean	visit(JmlResultReference resultReference, BlockScope scope) The primary \result can only be used in non-void method.
boolean	visit(JmlReturnStatement returnStatement, BlockScope scope)
boolean	visit(JmlSetComprehension jmlSetComprehension, BlockScope scope) It is used to succinctly define sets.
boolean	visit(JmlSetStatement jmlSetStatement, BlockScope scope) Is the equivalent of an assignment statement but is within an annotation.
boolean	visit(JmlSignalsClause jmlSignalsClause, BlockScope scope) Specifies the exceptional or abnormal postcondition, i.e., the property that is guaranteed to hold at the end of a method (or constructor) invocation when this method (or constructor) invocation terminates abruptly by throwing a given exception.
boolean	visit(JmlSignalsOnlyClause jmlSignalsOnlyClause, BlockScope scope) Is an abbreviation for a signals-clause that specifies what exceptions may be thrown by a method, and thus, implicitly, what exceptions may not be thrown.
boolean	visit(JmlSingleNameReference singleNameReference, BlockScope scope)
boolean	visit(JmlSingleNameReference singleNameReference, ClassScope scope)
boolean	visit(JmlSingleTypeReference singleTypeReference, BlockScope scope)
boolean	visit(JmlSingleTypeReference singleTypeReference, ClassScope scope)
boolean	visit(JmlSpecCaseBlock jmlSpecCaseBlock, BlockScope scope)
boolean	visit(JmlSpecCase jmlSpecCase, BlockScope scope)
boolean	visit(JmlSpecCaseBody jmlSpecCaseBody, BlockScope scope)
boolean	visit(JmlSpecCaseHeader jmlSpecCaseHeader, BlockScope scope) Method specification for checking precondition of method or constructor.
boolean	visit(JmlSpecCaseRestAsClauseSeq jmlSpecCaseRestAsClauseSeq, BlockScope scope)
boolean	visit(JmlStoreRefExpression jmlStoreRefExpression, BlockScope scope)
boolean	visit(JmlSubtypeExpression jmlSubtypeExpression, BlockScope scope)
boolean	visit(JmlTypeBodyDeclaration jmlTypeDecle, BlockScope scope)
boolean	visit(JmlTypeDeclaration typeDecle, CompilationUnitScope scope)
boolean	visit(JmlTypeExpression expression, BlockScope scope)
boolean	visit(JmlTypeofExpression jmlTypeofExpression, BlockScope scope)
boolean	visit(JmlUnaryExpression unaryExpression, BlockScope scope)
boolean	visit(JmlWhileStatement whileStatement, BlockScope scope)
boolean	visit(JmlWildcard wildcard, BlockScope scope)
boolean	visit(JmlWildcard wildcard, ClassScope scope)

Methods inherited from interface org.jmlspecs.jml4.rac.JavaAstVisitor

endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit

Method Detail

visit

boolean visit(JmlArrayQualifiedTypeReference arrayQualifiedTypeReference,
              BlockScope scope)

See Also:

ArrayQualifiedTypeReference

endVisit

void endVisit(JmlArrayQualifiedTypeReference arrayQualifiedTypeReference,
              BlockScope scope)

See Also:

JmlArrayQualifiedTypeReference

visit

boolean visit(JmlArrayQualifiedTypeReference arrayQualifiedTypeReference,
              ClassScope scope)

See Also:

JmlArrayQualifiedTypeReference

endVisit

void endVisit(JmlArrayQualifiedTypeReference arrayQualifiedTypeReference,
              ClassScope scope)

See Also:

JmlArrayQualifiedTypeReference

visit

boolean visit(JmlArrayReference arrayReference,
              BlockScope scope)

See Also:

ArrayReference

endVisit

void endVisit(JmlArrayReference arrayReference,
              BlockScope scope)

See Also:

JmlArrayReference

visit

boolean visit(JmlArrayTypeReference arrayTypeReference,
              BlockScope scope)

See Also:

ArrayTypeReference

endVisit

void endVisit(JmlArrayTypeReference arrayTypeReference,
              BlockScope scope)

See Also:

JmlArrayTypeReference

visit

boolean visit(JmlArrayTypeReference arrayTypeReference,
              ClassScope scope)

See Also:

JmlArrayTypeReference

endVisit

void endVisit(JmlArrayTypeReference arrayTypeReference,
              ClassScope scope)

See Also:

JmlArrayTypeReference

visit

boolean visit(JmlAssertStatement assertStatement,
              BlockScope scope)

Inside an annotation, an assert statement is JML assert statement. An assert statements tells JML to check that the specified predicate is true at the given point in the program. Examples include:

 //@ assert 0 < x;
 //@ assert false;
 

See Also:

AssertStatement

endVisit

void endVisit(JmlAssertStatement assertStatement,
              BlockScope scope)

See Also:

JmlAssertStatement

visit

boolean visit(JmlAssumeStatement assumeStatement,
              BlockScope scope)

Statements which are assumed to be true (in static analysis tools). For RAC, they are checked the same way as in JmlAssertStatement. Examples include:

 //@ assume x == 3;
 //@ assume 0 < x;
 

See Also:

JmlAssertStatement

endVisit

void endVisit(JmlAssumeStatement assumeStatement,
              BlockScope scope)

See Also:

JmlAssumeStatement

visit

boolean visit(JmlAssignment assignment,
              BlockScope scope)

See Also:

Assignment

endVisit

void endVisit(JmlAssignment assignment,
              BlockScope scope)

See Also:

JmlAssignment

visit

boolean visit(JmlCastExpression castExpression,
              BlockScope scope)

See Also:

CastExpression

endVisit

void endVisit(JmlCastExpression castExpression,
              BlockScope scope)

See Also:

JmlCastExpression

visit

boolean visit(JmlCastExpressionWithoutType castExpression,
              BlockScope scope)

endVisit

void endVisit(JmlCastExpressionWithoutType castExpression,
              BlockScope scope)

visit

boolean visit(JmlCompilationUnitDeclaration compilationUnitDeclaration,
              CompilationUnitScope scope)

endVisit

void endVisit(JmlCompilationUnitDeclaration compilationUnitDeclaration,
              CompilationUnitScope scope)

visit

boolean visit(JmlConstructorDeclaration constructorDeclaration,
              ClassScope scope)

See Also:

ConstructorDeclaration

endVisit

void endVisit(JmlConstructorDeclaration constructorDeclaration,
              ClassScope scope)

See Also:

JmlConstructorDeclaration

visit

boolean visit(JmlEnsuresClause ensuresClause,
              BlockScope scope)

An ensures clause specifies a normal postcondition, i.e., a property that is guaranteed to hold at the end of the method (or constructor) invocation in the case that this method (or constructor) invocation returns without throwing an exception. Examples include:

 //@ ensures x == 5;
 //@ ensures x > 0 && x != 2;
 

endVisit

void endVisit(JmlEnsuresClause ensuresClause,
              BlockScope scope)

See Also:

JmlEnsuresClause

visit

boolean visit(JmlFieldDeclaration fieldDeclaration,
              MethodScope scope)

See Also:

FieldDeclaration

endVisit

void endVisit(JmlFieldDeclaration fieldDeclaration,
              MethodScope scope)

See Also:

JmlFieldDeclaration

visit

boolean visit(JmlFieldReference fieldReference,
              BlockScope scope)

See Also:

FieldReference

endVisit

void endVisit(JmlFieldReference fieldReference,
              BlockScope scope)

See Also:

JmlFieldReference

visit

boolean visit(JmlFieldReference fieldReference,
              ClassScope scope)

See Also:

JmlFieldReference

endVisit

void endVisit(JmlFieldReference fieldReference,
              ClassScope scope)

See Also:

JmlFieldReference

visit

boolean visit(JmlLocalDeclaration localDeclaration,
              BlockScope scope)

See Also:

LocalDeclaration

endVisit

void endVisit(JmlLocalDeclaration localDeclaration,
              BlockScope scope)

See Also:

JmlLocalDeclaration

visit

boolean visit(JmlMessageSend messageSend,
              BlockScope scope)

See Also:

MessageSend

endVisit

void endVisit(JmlMessageSend messageSend,
              BlockScope scope)

See Also:

JmlMessageSend

visit

boolean visit(JmlMethodDeclaration methodDeclaration,
              ClassScope scope)

See Also:

MethodDeclaration

endVisit

void endVisit(JmlMethodDeclaration methodDeclaration,
              ClassScope scope)

See Also:

JmlMethodDeclaration

visit

boolean visit(JmlParameterizedQualifiedTypeReference parameterizedQualifiedTypeReference,
              BlockScope scope)

See Also:

ParameterizedQualifiedTypeReference

endVisit

void endVisit(JmlParameterizedQualifiedTypeReference parameterizedQualifiedTypeReference,
              BlockScope scope)

See Also:

JmlParameterizedQualifiedTypeReference

visit

boolean visit(JmlParameterizedQualifiedTypeReference parameterizedQualifiedTypeReference,
              ClassScope scope)

See Also:

JmlParameterizedQualifiedTypeReference

endVisit

void endVisit(JmlParameterizedQualifiedTypeReference parameterizedQualifiedTypeReference,
              ClassScope scope)

See Also:

JmlParameterizedQualifiedTypeReference

visit

boolean visit(JmlParameterizedSingleTypeReference parameterizedSingleTypeReference,
              BlockScope scope)

See Also:

ParameterizedSingleTypeReference

endVisit

void endVisit(JmlParameterizedSingleTypeReference parameterizedSingleTypeReference,
              BlockScope scope)

See Also:

JmlParameterizedSingleTypeReference

visit

boolean visit(JmlParameterizedSingleTypeReference parameterizedSingleTypeReference,
              ClassScope scope)

See Also:

JmlParameterizedSingleTypeReference

endVisit

void endVisit(JmlParameterizedSingleTypeReference parameterizedSingleTypeReference,
              ClassScope scope)

See Also:

JmlParameterizedSingleTypeReference

visit

boolean visit(JmlQualifiedNameReference qualifiedNameReference,
              BlockScope scope)

See Also:

QualifiedNameReference

endVisit

void endVisit(JmlQualifiedNameReference qualifiedNameReference,
              BlockScope scope)

See Also:

JmlQualifiedNameReference

visit

boolean visit(JmlQualifiedNameReference qualifiedNameReference,
              ClassScope scope)

See Also:

JmlQualifiedNameReference

endVisit

void endVisit(JmlQualifiedNameReference qualifiedNameReference,
              ClassScope scope)

See Also:

JmlQualifiedNameReference

visit

boolean visit(JmlQualifiedTypeReference qualifiedTypeReference,
              BlockScope scope)

See Also:

QualifiedTypeReference

endVisit

void endVisit(JmlQualifiedTypeReference qualifiedTypeReference,
              BlockScope scope)

See Also:

JmlQualifiedTypeReference

visit

boolean visit(JmlQualifiedTypeReference qualifiedTypeReference,
              ClassScope scope)

See Also:

JmlQualifiedTypeReference

endVisit

void endVisit(JmlQualifiedTypeReference qualifiedTypeReference,
              ClassScope scope)

See Also:

JmlQualifiedTypeReference

visit

boolean visit(JmlRequiresClause requiresClause,
              BlockScope scope)

Specifies a precondition of method or constructor. Examples include:

 //@ requires x > 0;
 //@ requires x == 0 || x == -1;
 

endVisit

void endVisit(JmlRequiresClause requiresClause,
              BlockScope scope)

See Also:

JmlRequiresClause

visit

boolean visit(JmlResultReference resultReference,
              BlockScope scope)

The primary \result can only be used in non-void method. Its value is the value returned by the method. Its type is the return type of the method. Examples include:

 \result <= x
 \result == x
 

endVisit

void endVisit(JmlResultReference resultReference,
              BlockScope scope)

See Also:

JmlResultReference

visit

boolean visit(JmlReturnStatement returnStatement,
              BlockScope scope)

See Also:

ReturnStatement

endVisit

void endVisit(JmlReturnStatement returnStatement,
              BlockScope scope)

See Also:

JmlReturnStatement

visit

boolean visit(JmlSingleNameReference singleNameReference,
              BlockScope scope)

See Also:

SingleNameReference

endVisit

void endVisit(JmlSingleNameReference singleNameReference,
              BlockScope scope)

See Also:

JmlSingleNameReference

visit

boolean visit(JmlSingleNameReference singleNameReference,
              ClassScope scope)

See Also:

JmlSingleNameReference

endVisit

void endVisit(JmlSingleNameReference singleNameReference,
              ClassScope scope)

See Also:

JmlSingleNameReference

visit

boolean visit(JmlSingleTypeReference singleTypeReference,
              BlockScope scope)

See Also:

SingleTypeReference

endVisit

void endVisit(JmlSingleTypeReference singleTypeReference,
              BlockScope scope)

See Also:

JmlSingleTypeReference

visit

boolean visit(JmlSingleTypeReference singleTypeReference,
              ClassScope scope)

See Also:

JmlSingleTypeReference

endVisit

void endVisit(JmlSingleTypeReference singleTypeReference,
              ClassScope scope)

See Also:

JmlSingleTypeReference

visit

boolean visit(JmlWildcard wildcard,
              BlockScope scope)

endVisit

void endVisit(JmlWildcard wildcard,
              BlockScope scope)

visit

boolean visit(JmlWildcard wildcard,
              ClassScope scope)

endVisit

void endVisit(JmlWildcard wildcard,
              ClassScope scope)

visit

boolean visit(JmlWhileStatement whileStatement,
              BlockScope scope)

See Also:

WhileStatement

endVisit

void endVisit(JmlWhileStatement whileStatement,
              BlockScope scope)

See Also:

JmlWhileStatement

visit

boolean visit(JmlLoopAnnotations jmlLoopAnnotations,
              BlockScope scope)

endVisit

void endVisit(JmlLoopAnnotations jmlLoopAnnotations,
              BlockScope scope)

visit

boolean visit(JmlLoopInvariant jmlLoopInvariant,
              BlockScope scope)

Is used to help prove partial correctness of a loop statement. The loop invariant holds at the beginning of each iteration of the loop. Informally,

 //@ maintaining J ;
 while (B) { S }
 

Examples include:

 //@ maintaining x > 0;
 while (x < 5) { x++; }
 

In this example, //@ maintaining x > 0; is a JmlLoopInvariant.

endVisit

void endVisit(JmlLoopInvariant jmlLoopInvariant,
              BlockScope scope)

See Also:

JmlLoopInvariant

visit

boolean visit(JmlLoopVariant jmlLoopVariant,
              BlockScope scope)

Is used to help prove termination of a loop statement. It specifies an expression of type long or int that must be no less than 0 when the loop is executing, and must decrease by at least one (1) each time around the loop. Informally,

 //@ decreasing E;
 while (B) { S }
 

Examples include:

 //@ decreasing x;
 while (x != 0) { x--; }
 

In this example, //@ decreasing x; is a JmlLoopVariant.

endVisit

void endVisit(JmlLoopVariant jmlLoopVariant,
              BlockScope scope)

See Also:

JmlLoopVariant

visit

boolean visit(JmlOldExpression jmlOldExpression,
              BlockScope scope)

Refers to the value that the expression had in the pre-state of a method. Examples include:

 \old(x) != 0;
 \pre(x) > \result;
 

In this example, \old(x) and \pre(x) are JmlOldExpression.

endVisit

void endVisit(JmlOldExpression jmlOldExpression,
              BlockScope scope)

See Also:

JmlOldExpression

visit

boolean visit(JmlClause jmlClause,
              BlockScope scope)

See Also:

JmlClause

endVisit

void endVisit(JmlClause jmlClause,
              BlockScope scope)

See Also:

JmlClause

visit

boolean visit(JmlTypeDeclaration typeDecle,
              CompilationUnitScope scope)

See Also:

TypeDeclaration

endVisit

void endVisit(JmlTypeDeclaration typeDecle,
              CompilationUnitScope scope)

See Also:

JmlTypeDeclaration

visit

boolean visit(JmlAllocationExpression allocationExpression,
              BlockScope scope)

See Also:

AllocationExpression

endVisit

void endVisit(JmlAllocationExpression allocationExpression,
              BlockScope scope)

See Also:

JmlAllocationExpression

visit

boolean visit(JmlAssertOrAssumeStatement assertOrAssumeStatement,
              BlockScope scope)

See Also:

JmlAssertStatement, JmlAssumeStatement

endVisit

void endVisit(JmlAssertOrAssumeStatement assertOrAssumeStatement,
              BlockScope scope)

See Also:

JmlAssertOrAssumeStatement

visit

boolean visit(JmlAssignableClause jmlAssignableClause,
              BlockScope scope)

Gives a frame axiom for a specification. It says that, from the clientÕs point of view, only the locations named, and locations in the data groups associated with these locations, can be assigned to during the execution of the method. Examples include:

 //@ assignable \nothing;
 //@ assignable \everything;
 

endVisit

void endVisit(JmlAssignableClause jmlAssignableClause,
              BlockScope scope)

See Also:

JmlAssignableClause

visit

boolean visit(JmlClinit clinit,
              ClassScope scope)

See Also:

Clinit

endVisit

void endVisit(JmlClinit clinit,
              ClassScope scope)

See Also:

JmlClinit

visit

boolean visit(JmlConditionalExpression conditionalExpression,
              BlockScope scope)

See Also:

ConditionalExpression

endVisit

void endVisit(JmlConditionalExpression conditionalExpression,
              BlockScope scope)

See Also:

JmlConditionalExpression

visit

boolean visit(JmlConstraintClause jmlConstraintClause,
              BlockScope scope)

Are relationships that should hold for the combination of each visible state and any visible state that occurs later in the programÕs execution. It is used to constrain the way that values change over time. Examples include:

 //@ constraint a == \old(a);
 //@ constraint b.length == \old(b.length);
 

endVisit

void endVisit(JmlConstraintClause jmlConstraintClause,
              BlockScope scope)

See Also:

JmlConstraintClause

visit

boolean visit(JmlDoStatement doStatement,
              BlockScope scope)

See Also:

DoStatement

endVisit

void endVisit(JmlDoStatement doStatement,
              BlockScope scope)

See Also:

JmlDoStatement

visit

boolean visit(JmlForStatement forStatement,
              BlockScope scope)

See Also:

ForStatement

endVisit

void endVisit(JmlForStatement forStatement,
              BlockScope scope)

See Also:

JmlForStatement

visit

boolean visit(JmlInitiallyClause jmlInitiallyClause,
              CompilationUnitScope scope)

Is used to specify the initial state of model fields. Examples include:

 //@ public model int x;
 //@ public initially x == 0;
 

In this example, initially x == 0; is a JmlInitiallyClause.

endVisit

void endVisit(JmlInitiallyClause jmlInitiallyClause,
              CompilationUnitScope scope)

See Also:

JmlInitiallyClause

visit

boolean visit(JmlInvariantForType jmlInvariantForType,
              CompilationUnitScope scope)

Properties that have to hold in all visible states. Examples include:

 //@ invariant b != null && b.length == 6;
 

endVisit

void endVisit(JmlInvariantForType jmlInvariantForType,
              CompilationUnitScope scope)

See Also:

JmlInvariantForType

visit

boolean visit(JmlRepresentsClause representsClause,
              CompilationUnitScope scope)

The first form of represents clauses (with <- or =) is called a functional abstraction. This form defines the value of the store-ref-expression in a visible state as the value of the spec-expression that follows the l-arrow-or-eq. The second form (with \such_that) is called a relational abstraction. This form constrains the value of the store-ref-expression in a visible state to satisfy the given predicate. Examples include:

 protected int x_;
 //@       in x;
 //@ protected represents x <- x_;
 

In this example, representx x <- x_; is a JmlRepresentsClause.

endVisit

void endVisit(JmlRepresentsClause representsClause,
              CompilationUnitScope scope)

See Also:

JmlRepresentsClause

visit

boolean visit(JmlSetStatement jmlSetStatement,
              BlockScope scope)

Is the equivalent of an assignment statement but is within an annotation. It is used to assign a value to a ghost variable or to a ghost field. Examples include:

 //@ set i = 0;
 //@ set collection.elementType = \type(int);
 

endVisit

boolean endVisit(JmlSetStatement jmlSetStatement,
                 BlockScope scope)

See Also:

JmlSetStatement

visit

boolean visit(JmlSignalsClause jmlSignalsClause,
              BlockScope scope)

Specifies the exceptional or abnormal postcondition, i.e., the property that is guaranteed to hold at the end of a method (or constructor) invocation when this method (or constructor) invocation terminates abruptly by throwing a given exception. Examples include:

 //@ signals (Exception) x < 0;
 

endVisit

void endVisit(JmlSignalsClause jmlSignalsClause,
              BlockScope scope)

See Also:

JmlSignalsClause

visit

boolean visit(JmlSignalsOnlyClause jmlSignalsOnlyClause,
              BlockScope scope)

Is an abbreviation for a signals-clause that specifies what exceptions may be thrown by a method, and thus, implicitly, what exceptions may not be thrown. Examples include:

 signals_only NullPointerException;
 

endVisit

void endVisit(JmlSignalsOnlyClause jmlSignalsOnlyClause,
              BlockScope scope)

See Also:

JmlSignalsOnlyClause

visit

boolean visit(JmlTypeBodyDeclaration jmlTypeDecle,
              BlockScope scope)

endVisit

void endVisit(JmlTypeBodyDeclaration jmlTypeDecle,
              BlockScope scope)

visit

boolean visit(JmlUnaryExpression unaryExpression,
              BlockScope scope)

See Also:

UnaryExpression

endVisit

void endVisit(JmlUnaryExpression unaryExpression,
              BlockScope scope)

See Also:

JmlUnaryExpression

visit

boolean visit(JmlSpecCaseBlock jmlSpecCaseBlock,
              BlockScope scope)

endVisit

void endVisit(JmlSpecCaseBlock jmlSpecCaseBlock,
              BlockScope scope)

visit

boolean visit(JmlSpecCaseBody jmlSpecCaseBody,
              BlockScope scope)

endVisit

void endVisit(JmlSpecCaseBody jmlSpecCaseBody,
              BlockScope scope)

visit

boolean visit(JmlSpecCaseRestAsClauseSeq jmlSpecCaseRestAsClauseSeq,
              BlockScope scope)

endVisit

void endVisit(JmlSpecCaseRestAsClauseSeq jmlSpecCaseRestAsClauseSeq,
              BlockScope scope)

visit

boolean visit(JmlFreshExpression jmlFreshExpression,
              BlockScope scope)

Asserts that objects were freshly allocated. Examples include,

 \fresh(x,y)
 

In this example, \fresh(x,y) asserts that x and y are not null and that the objects bound to these identifiers were not allocated in the pre-state.

endVisit

void endVisit(JmlFreshExpression jmlFreshExpression,
              BlockScope scope)

See Also:

JmlFreshExpression

visit

boolean visit(JmlMapsIntoClause jmlMapsIntoClause,
              BlockScope scope)

endVisit

void endVisit(JmlMapsIntoClause jmlMapsIntoClause,
              BlockScope scope)

visit

boolean visit(JmlMapsMemberRefExpr jmlMapsMemberRefExpr,
              BlockScope scope)

endVisit

void endVisit(JmlMapsMemberRefExpr jmlMapsMemberRefExpr,
              BlockScope scope)

visit

boolean visit(JmlMemberFieldRef jmlMemberFieldRef,
              BlockScope scope)

endVisit

void endVisit(JmlMemberFieldRef jmlMemberFieldRef,
              BlockScope scope)

visit

boolean visit(JmlMethodSpecification jmlMethodSpecification,
              BlockScope scope)

endVisit

void endVisit(JmlMethodSpecification jmlMethodSpecification,
              BlockScope scope)

visit

boolean visit(JmlName jmlName,
              BlockScope scope)

endVisit

void endVisit(JmlName jmlName,
              BlockScope scope)

visit

boolean visit(JmlSetComprehension jmlSetComprehension,
              BlockScope scope)

It is used to succinctly define sets. Examples include:

 new JMLObjectSet {Integer i | myIntSet.has(i) &&
       i != null && 0 <= i.intValue() && i.intValue() <= 10 }
 

In the above example, JMLObjectSet is the subset of non-null Integer objects found in the set myIntSet whose values are between 0 and 10, inclusive.

endVisit

void endVisit(JmlSetComprehension jmlSetComprehension,
              BlockScope scope)

See Also:

JmlSetComprehension

visit

boolean visit(JmlSpecCase jmlSpecCase,
              BlockScope scope)

endVisit

void endVisit(JmlSpecCase jmlSpecCase,
              BlockScope scope)

visit

boolean visit(JmlSpecCaseHeader jmlSpecCaseHeader,
              BlockScope scope)

Method specification for checking precondition of method or constructor. Examples include:

 //@ requires x > 0;
 //@ requires x != 1;
 

See Also:

JmlRequiresClause

endVisit

void endVisit(JmlSpecCaseHeader jmlSpecCaseHeader,
              BlockScope scope)

See Also:

JmlSpecCaseHeader

visit

boolean visit(JmlStoreRefExpression jmlStoreRefExpression,
              BlockScope scope)

endVisit

void endVisit(JmlStoreRefExpression jmlStoreRefExpression,
              BlockScope scope)

visit

boolean visit(JmlSubtypeExpression jmlSubtypeExpression,
              BlockScope scope)

endVisit

void endVisit(JmlSubtypeExpression jmlSubtypeExpression,
              BlockScope scope)

visit

boolean visit(JmlBooleanQuantifier jmlBooleanQuantifier,
              BlockScope scope)

endVisit

void endVisit(JmlBooleanQuantifier jmlBooleanQuantifier,
              BlockScope scope)

visit

boolean visit(JmlGroupName jmlGroupName,
              BlockScope scope)

endVisit

void endVisit(JmlGroupName jmlGroupName,
              BlockScope scope)

visit

boolean visit(JmlModifier jmlModifier,
              BlockScope scope)

In addition to the Java modifiers that can be legally attached to a class or interface definition [Gosling-etal00], in JML one can use the following modifiers.

 pure model
 spec_java_math spec_safe_math spec_bigint_math
 code_java_math code_safe_math code_bigint_math
 nullable_by_default
 

endVisit

void endVisit(JmlModifier jmlModifier,
              BlockScope scope)

See Also:

JmlModifier

visit

boolean visit(JmlNumericQuantifier jmlNumericQuantifier,
              BlockScope scope)

endVisit

void endVisit(JmlNumericQuantifier jmlNumericQuantifier,
              BlockScope scope)

visit

boolean visit(JmlTypeExpression expression,
              BlockScope scope)

endVisit

void endVisit(JmlTypeExpression expression,
              BlockScope scope)

See Also:

JmlTypeExpression

visit

boolean visit(JmlElemtypeExpression jmlElemtypeExpression,
              BlockScope scope)

endVisit

void endVisit(JmlElemtypeExpression jmlElemtypeExpression,
              BlockScope scope)

visit

boolean visit(JmlExplicitConstructorCall jmlExplicitConstructorCall,
              BlockScope scope)

See Also:

ExplicitConstructorCall

endVisit

void endVisit(JmlExplicitConstructorCall jmlExplicitConstructorCall,
              BlockScope scope)

See Also:

JmlExplicitConstructorCall

visit

boolean visit(JmlTypeofExpression jmlTypeofExpression,
              BlockScope scope)

endVisit

void endVisit(JmlTypeofExpression jmlTypeofExpression,
              BlockScope scope)

visit

boolean visit(JmlMethodSpecification jmlMethodSpecification,
              ClassScope classScope)

endVisit

void endVisit(JmlMethodSpecification jmlMethodSpecification,
              ClassScope classScope)

visit

boolean visit(JmlQuantifiedExpression jmlQuantifiedExpression,
              BlockScope blockScope)

endVisit

void endVisit(JmlQuantifiedExpression jmlQuantifiedExpression,
              BlockScope blockScope)