Uses of Class
org.jmlspecs.checker.JmlHeavyweightSpec

Packages that use JmlHeavyweightSpec

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

Subclasses of JmlHeavyweightSpec in org.jmlspecs.checker

class	JmlBehaviorSpec JmlBehaviorSpec.java heavyweight-spec ::= [ privacy ] "behavior" generic-spec-case
class	JmlExceptionalBehaviorSpec JmlExceptionalBehaviorSpec.java heavyweight-spec ::= [ privacy ] "exceptional_behavior" exceptional-spec-case
class	JmlNormalBehaviorSpec JmlNormalBehaviorSpec.java heavyweight-spec ::= [ privacy ] "normal_behavior" normal-spec-case

Methods in org.jmlspecs.checker that return JmlHeavyweightSpec

JmlHeavyweightSpec

JmlParser.jmlHeavyweightSpec(long mods)

Uses of JmlHeavyweightSpec in org.jmlspecs.jmldoc.jmldoc_142

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

void	SpecWriter.visitJmlBehaviorSpecHelper(JmlHeavyweightSpec self, String s)

Uses of JmlHeavyweightSpec in org.jmlspecs.jmlrac

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

private void

DesugarSpec.visitHeavyweightSpec(JmlHeavyweightSpec self) Desugars a general/normal/exceptional behavior specification.