Uses of Class
org.jmlspecs.checker.JmlBehaviorSpec

Packages that use JmlBehaviorSpec

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.

Uses of JmlBehaviorSpec in org.jmlspecs.checker

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

void	JmlAbstractVisitor.visitJmlBehaviorSpec(JmlBehaviorSpec self)
abstract void	JmlVisitor.visitJmlBehaviorSpec(JmlBehaviorSpec self)
void	JmlVisitorNI.visitJmlBehaviorSpec(JmlBehaviorSpec self)

Uses of JmlBehaviorSpec in org.jmlspecs.jmldoc.jmldoc_142

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

void	SpecWriter.visitJmlBehaviorSpec(JmlBehaviorSpec self)

Uses of JmlBehaviorSpec in org.jmlspecs.jmlrac

Methods in org.jmlspecs.jmlrac that return JmlBehaviorSpec

private JmlBehaviorSpec

DesugarSpec.addDefaultRequiresClause(JmlBehaviorSpec bs) Adds a default requires clause to the given behaviorSpec, bs, and returns it.

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

private JmlBehaviorSpec	DesugarSpec.addDefaultRequiresClause(JmlBehaviorSpec bs) Adds a default requires clause to the given behaviorSpec, bs, and returns it.
void	DesugarSpec.visitJmlBehaviorSpec(JmlBehaviorSpec self) Desugars a behavior specification.
void	RacPrettyPrinter.visitJmlBehaviorSpec(JmlBehaviorSpec self) Prints a JML behavior spec.
void	TransMethod.SpecCaseCollector.visitJmlBehaviorSpec(JmlBehaviorSpec self)