Uses of Class
org.jmlspecs.checker.JmlSpecCase

Packages that use JmlSpecCase

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

Subclasses of JmlSpecCase in org.jmlspecs.checker

class	JmlAbruptSpecCase JmlAbruptSpecCase.java
class	JmlBehaviorSpec JmlBehaviorSpec.java heavyweight-spec ::= [ privacy ] "behavior" generic-spec-case
class	JmlCodeContract An abstraction of JML method specification.
class	JmlExceptionalBehaviorSpec JmlExceptionalBehaviorSpec.java heavyweight-spec ::= [ privacy ] "exceptional_behavior" exceptional-spec-case
class	JmlExceptionalSpecCase An AST node class for the JML exceptional-spec-case.
class	JmlGeneralSpecCase An abstraction of JML specification cases.
class	JmlGenericSpecCase An AST node class for the JML generic-spec-case.
class	JmlHeavyweightSpec An AST node class for the JML heavyweight-spec.
class	JmlModelProgram JmlModelProgram.java
class	JmlNormalBehaviorSpec JmlNormalBehaviorSpec.java heavyweight-spec ::= [ privacy ] "normal_behavior" normal-spec-case
class	JmlNormalSpecCase An AST node class for the JML normal-spec-case.

Fields in org.jmlspecs.checker declared as JmlSpecCase

protected JmlSpecCase[]	JmlSpecification.specCases
private JmlSpecCase[]	JmlRedundantSpec.implications

Methods in org.jmlspecs.checker that return JmlSpecCase

JmlSpecCase[]	JmlMethodSpecification.specCases()
JmlSpecCase[]	JmlSpecification.specCases()
JmlSpecCase[]	JmlRedundantSpec.implications()
JmlSpecCase[]	JmlParser.jmlSpecCaseSeq(long mods)
JmlSpecCase	JmlParser.jmlSpecCase(long mods)
JmlSpecCase[]	JmlParser.jmlImplications()

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

JmlSpecification	JmlSpecification.newInstance(JmlSpecCase[] specCases, JmlRedundantSpec redundantSpec)
JmlSpecification	JmlExtendingSpecification.newInstance(JmlSpecCase[] specCases, JmlRedundantSpec redundantSpec)
static void	NonNullStatistics.checkSpecCase(JmlSpecCase jsc, JmlContext context, String fn, boolean fromHeavy)

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

JmlSpecification(TokenReference where, JmlSpecCase[] specCases, JmlRedundantSpec redundantSpec)

JmlExtendingSpecification(TokenReference where, JmlSpecCase[] specCases, JmlRedundantSpec redundantSpec)

JmlRedundantSpec(TokenReference where, JmlSpecCase[] implications, JmlExample[] examples)

Uses of JmlSpecCase in org.jmlspecs.jmldoc.jmldoc_142

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

void	SpecWriter.visitJmlSpecificationHelper(JmlSpecCase[] scases, boolean initialAlso)

Uses of JmlSpecCase in org.jmlspecs.jmlrac

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

protected void

RacPrettyPrinter.visitSpecCases(JmlSpecCase[] specCases) Prints spec cases.