Uses of Class
org.jmlspecs.checker.JmlMethodSpecification

Packages that use JmlMethodSpecification

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 JmlMethodSpecification in org.jmlspecs.checker

Subclasses of JmlMethodSpecification in org.jmlspecs.checker

class	JmlExtendingSpecification A method specification that extetends inherited specifications.
class	JmlSpecification JmlSpecification.java

Fields in org.jmlspecs.checker declared as JmlMethodSpecification

private JmlMethodSpecification	JmlClassBlock.methodSpecification
private JmlMethodSpecification	JmlMethodDeclaration.methodSpecification
private JmlMethodSpecification	JmlMethodDeclaration.combinedMethodSpecification

Methods in org.jmlspecs.checker that return JmlMethodSpecification

JmlMethodSpecification	JmlMemberDeclaration.getCombinedSpecification() Returns null unless overridden by a subclass.
JmlMethodSpecification	JmlMethodDeclaration.methodSpecification()
JmlMethodSpecification	JmlMethodDeclaration.getCombinedSpecification() Returns the method specifications of this member declaration combined with the specifications of those it refines.
JmlMethodSpecification	JmlSourceMethod.getSpecification() Returns the specification AST for this method.
JmlMethodSpecification	JmlParser.jmlMethodSpecification(long mods)
private JmlMethodSpecification	TestJmlParser.methodSpecificationFrom(String mspec)
protected JmlMethodSpecification	TestJmlParser.Helper.getMethodSpecification(String sourceCode)

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

void	JmlAbstractVisitor.visitJmlMethodSpecification(JmlMethodSpecification self)
abstract void	JmlVisitor.visitJmlMethodSpecification(JmlMethodSpecification self)
static JmlMethodDeclaration	JmlMethodDeclaration.makeInstance(TokenReference where, long modifiers, CTypeVariable[] typevariables, CType returnType, String ident, JFormalParameter[] parameters, CClassType[] exceptions, JBlock body, JavadocComment javadoc, JavaStyleComment[] comments, JmlMethodSpecification methodSpecification)
static JmlConstructorDeclaration	JmlConstructorDeclaration.makeInstance(TokenReference where, long modifiers, String ident, JFormalParameter[] params, CClassType[] exceptions, JConstructorBlock body, JavadocComment javadoc, JavaStyleComment[] comments, JmlMethodSpecification methodSpecification)
void	JmlVisitorNI.visitJmlMethodSpecification(JmlMethodSpecification self)

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

JmlClassBlock(TokenReference where, boolean isStatic, JavadocComment javadoc, JmlMethodSpecification methodSpecification)
Constructs an initializer specification AST node.

JmlClassBlock(TokenReference where, boolean isStatic, JStatement[] body, JavadocComment javadoc, JmlMethodSpecification methodSpecification)
Constructs an initializer AST node annotated with a method specification.

JmlMethodDeclaration(TokenReference where, JmlMethodSpecification methodSpecification, JMethodDeclaration delegee)

JmlConstructorDeclaration(TokenReference where, JmlMethodSpecification methodSpecification, JConstructorDeclaration delegee)

Uses of JmlMethodSpecification in org.jmlspecs.jmldoc.jmldoc_142

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

protected void

JmlHTML.insertSpecification(StringBuffer s, JmlMethodSpecification jms) This method actually generates a string representing the given JmlMethodSpecification and appends it to the given StringBuffer.

Uses of JmlMethodSpecification in org.jmlspecs.jmlrac

Fields in org.jmlspecs.jmlrac declared as JmlMethodSpecification

protected JmlMethodSpecification

TransMethod.desugaredSpec desugared specification of the target method to be translated

Methods in org.jmlspecs.jmlrac that return JmlMethodSpecification

JmlMethodSpecification

DesugarSpec.perform(JmlMethodSpecification mspec, CClassType[] exceptions) Returns a desugared specification of the given method specification.

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

JmlMethodSpecification	DesugarSpec.perform(JmlMethodSpecification mspec, CClassType[] exceptions) Returns a desugared specification of the given method specification.
void	RacPrettyPrinter.visitJmlMethodSpecification(JmlMethodSpecification self)

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

TransMethod.SpecCaseCollector(JmlMethodSpecification mspec)
Constructs a new instance.