Uses of Class
org.jmlspecs.checker.JmlPredicate

Packages that use JmlPredicate

org.jmlspecs.checker	Contains the source code for a parser and typechecker for JML annotations and java code.
org.jmlspecs.jmldoc.jmldoc_142
org.jmlspecs.jmlrac	Generates Java classes from JML specifications that check assertions at runtime.
org.jmlspecs.jmlrac.qexpr	Translates JML quantified expressions into Java source code to evaluate them at runtime.

Uses of JmlPredicate in org.jmlspecs.checker

Subclasses of JmlPredicate in org.jmlspecs.checker

class

JmlPredicateKeyword

Fields in org.jmlspecs.checker declared as JmlPredicate

private JmlPredicate	JmlInvariant.predicate An AST for the predicate clause of this invariant.
protected JmlPredicate	JmlConstraint.predicate An AST for the predicate clause of this constraint.
private JmlPredicate	JmlRepresentsDecl.predicate
private JmlPredicate	JmlAxiom.predicate
protected JmlPredicate	JmlPredicateClause.predOrNot
private JmlPredicate	JmlAssertOrAssumeStatement.predicate
private JmlPredicate	JmlHenceByStatement.predicate
private JmlPredicate	JmlInitiallyVarAssertion.predicate
private JmlPredicate	JmlInvariantStatement.predicate
private JmlPredicate	JmlLoopInvariant.predicate
private JmlPredicate	JmlReadableIfVarAssertion.predicate
private JmlPredicate	JmlWritableIfVarAssertion.predicate
private JmlPredicate	JmlSetComprehension.predicate
private JmlPredicate	JmlSpecQuantifiedExpression.predicate

Methods in org.jmlspecs.checker that return JmlPredicate

JmlPredicate	JmlInvariant.predicate()
JmlPredicate	JmlConstraint.predicate()
JmlPredicate	JmlRepresentsDecl.predicate() Returns the predicate of this represents declaration.
JmlPredicate	JmlAxiom.predicate()
JmlPredicate	JmlPredicateClause.predOrNot()
JmlPredicate	JmlAssertOrAssumeStatement.predicate()
JmlPredicate	JmlHenceByStatement.predicate()
JmlPredicate	JmlInitiallyVarAssertion.predicate()
JmlPredicate	JmlInvariantStatement.predicate()
JmlPredicate	JmlLoopInvariant.predicate()
JmlPredicate	JmlReadableIfVarAssertion.predicate()
JmlPredicate	JmlWritableIfVarAssertion.predicate()
JmlPredicate	JmlSetComprehension.predicate()
JmlPredicate	JmlSpecQuantifiedExpression.predicate()
JmlPredicate	JmlParser.jmlPredicate()

Methods in org.jmlspecs.checker with parameters of type JmlPredicate

void	JmlAbstractVisitor.visitJmlPredicate(JmlPredicate self)
abstract void	JmlVisitor.visitJmlPredicate(JmlPredicate self)
void	JmlVisitorNI.visitJmlPredicate(JmlPredicate self)
void	JmlAccumSubclassingInfo.visitJmlPredicate(JmlPredicate self)
void	JmlExpressionChecker.visitJmlPredicate(JmlPredicate self)

Constructors in org.jmlspecs.checker with parameters of type JmlPredicate

JmlInvariant(TokenReference where, long modifiers, boolean redundantly, JmlPredicate predicate)
Construct an invariant annotation AST.

JmlConstraint(TokenReference where, long modifiers, boolean redundantly, JmlPredicate predicate, JmlMethodNameList methodNames)
Creates a new JmlConstraint instance.

JmlRepresentsDecl(TokenReference where, long modifiers, boolean redundantly, JmlStoreRefExpression storeRef, JmlPredicate predicate)
Creates a new JmlRepresentsDecl instance.

JmlAxiom(TokenReference where, JmlPredicate predicate)

JmlPredicateClause(TokenReference where, boolean isRedundantly, JmlPredicate predOrNot)

JmlRequiresClause(TokenReference where, boolean isRedundantly, JmlPredicate predOrNot)

JmlAssertOrAssumeStatement(TokenReference where, boolean isRedundantly, JmlPredicate predicate, JExpression throwMessage, JavaStyleComment[] comments)

JmlAssertStatement(TokenReference where, boolean isRedundantly, JmlPredicate predicate, JExpression throwMessage, JavaStyleComment[] comments)

JmlAssumeStatement(TokenReference where, boolean isRedundantly, JmlPredicate predicate, JExpression throwMessage, JavaStyleComment[] comments)

JmlSpecStatementClause(TokenReference where, boolean isRedundantly, JmlPredicate predOrNot, boolean isNotSpecified)

JmlLabeled(TokenReference where, boolean isRedundantly, String label, JmlPredicate predOrNot, boolean isNotSpecified)

JmlBreaksClause(TokenReference where, boolean isRedundantly, String label, JmlPredicate predOrNot, boolean isNotSpecified)

JmlContinuesClause(TokenReference where, boolean isRedundantly, String label, JmlPredicate predOrNot, boolean isNotSpecified)

JmlDivergesClause(TokenReference where, boolean isRedundantly, JmlPredicate predOrNot)

JmlDurationClause(TokenReference where, boolean isRedundantly, JmlSpecExpression specExp, JmlPredicate pred)

JmlEnsuresClause(TokenReference where, boolean isRedundantly, JmlPredicate predOrNot)

JmlHenceByStatement(TokenReference where, boolean isRedundantly, JmlPredicate predicate, JavaStyleComment[] comments)

JmlInitiallyVarAssertion(TokenReference where, long modifiers, JmlPredicate predicate)

JmlInvariantStatement(TokenReference where, boolean isRedundantly, JmlPredicate predicate, JavaStyleComment[] comments)

JmlLoopInvariant(TokenReference where, boolean isRedundantly, JmlPredicate predicate)

JmlMeasuredClause(TokenReference where, boolean isRedundantly, JmlSpecExpression specExp, JmlPredicate pred)

JmlReadableIfVarAssertion(TokenReference where, long modifiers, JNameExpression fieldName, JmlPredicate predicate)

JmlWritableIfVarAssertion(TokenReference where, long modifiers, JNameExpression fieldName, JmlPredicate predicate)

JmlReturnsClause(TokenReference where, boolean isRedundantly, JmlPredicate predOrNot, boolean isNotSpecified)

JmlSetComprehension(TokenReference where, long modifiers, CType type, CType memberType, String ident, JExpression supersetPred, JmlPredicate predicate)

JmlSignalsClause(TokenReference where, boolean isRedundantly, CType type, String ident, JmlPredicate pred, boolean notSpecified)

JmlSpecQuantifiedExpression(TokenReference where, int oper, JVariableDefinition[] quantifiedVarDecls, JmlPredicate predicate, JmlSpecExpression specExpression)

JmlWhenClause(TokenReference where, boolean isRedundantly, JmlPredicate predOrNot)

JmlWorkingSpaceClause(TokenReference where, boolean isRedundantly, JmlSpecExpression specExp, JmlPredicate pred)

Uses of JmlPredicate in org.jmlspecs.jmldoc.jmldoc_142

Methods in org.jmlspecs.jmldoc.jmldoc_142 with parameters of type JmlPredicate

void	SpecWriter.visitJmlPredicate(JmlPredicate self)

Uses of JmlPredicate in org.jmlspecs.jmlrac

Subclasses of JmlPredicate in org.jmlspecs.jmlrac

class

RacPredicate An AST node class for RAC-specific predicates.

Methods in org.jmlspecs.jmlrac with parameters of type JmlPredicate

void	RacPrettyPrinter.visitJmlPredicate(JmlPredicate self) Prints a JML predicate.
void	TransExpression.visitJmlPredicate(JmlPredicate self) Translates the given JML predicate.
void	TransExpression2.visitJmlPredicate(JmlPredicate self) Translates the given JML predicate.

Constructors in org.jmlspecs.jmlrac with parameters of type JmlPredicate

RacPredicate(JmlPredicate predicate)

Uses of JmlPredicate in org.jmlspecs.jmlrac.qexpr

Methods in org.jmlspecs.jmlrac.qexpr with parameters of type JmlPredicate

void	AbstractExpressionVisitor.visitJmlPredicate(JmlPredicate self) Visits the given RAC predicate, self.