Uses of Class
org.jmlspecs.checker.JmlInvariant

Packages that use JmlInvariant

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

Fields in org.jmlspecs.checker declared as JmlInvariant

protected JmlInvariant[]	JmlTypeDeclaration.invariants
protected JmlInvariant[]	JmlTypeDeclaration.combinedInvariants

Methods in org.jmlspecs.checker that return JmlInvariant

JmlInvariant[]	CParseClassContext.invariants()
JmlInvariant[]	JmlTypeDeclaration.invariants()
JmlInvariant[]	JmlTypeDeclaration.combinedInvariants()
private JmlInvariant[]	TestJmlParser.invariantsFrom(JmlCompilationUnit unit)

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

void	JmlAbstractVisitor.visitJmlInvariant(JmlInvariant self)
abstract void	JmlVisitor.visitJmlInvariant(JmlInvariant self)
void	CParseClassContext.addInvariant(JmlInvariant inv)
static JmlClassDeclaration	JmlClassDeclaration.makeInstance(TokenReference where, long modifiers, String ident, CTypeVariable[] typevariables, CClassType superType, boolean isWeakSubtype, CClassType[] interfaces, boolean[] interfaceWeaklyFlags, ArrayList methods, ArrayList inners, JPhylum[] fieldsAndInits, JmlInvariant[] invariants, JmlConstraint[] constraints, JmlRepresentsDecl[] representsDecls, JmlAxiom[] axioms, JmlVarAssertion[] varAssertions, JavadocComment javadoc, JavaStyleComment[] comment, boolean isRefinedType) Constructs a class declaration in the parsing tree.
static JmlInterfaceDeclaration	JmlInterfaceDeclaration.makeInstance(TokenReference where, long modifiers, String ident, CTypeVariable[] typevariables, CClassType[] interfaces, boolean[] interfaceWeaklyFlags, ArrayList methods, ArrayList inners, JPhylum[] fieldsAndInits, JmlInvariant[] invariants, JmlConstraint[] constraints, JmlRepresentsDecl[] representsDecls, JmlAxiom[] axioms, JmlVarAssertion[] varAssertions, JavadocComment javadoc, JavaStyleComment[] comment, boolean isRefinedType) Constructs an interface declaration in the parsing tree.
void	JmlVisitorNI.visitJmlInvariant(JmlInvariant self)
static boolean	JmlAdmissibilityVisitor.checkInvariant(JmlInvariant expr, JmlExpressionContext ectx) Admissibility checks an invariant.

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

JmlTypeDeclaration(TokenReference where, boolean[] interfaceWeaklyFlags, JmlInvariant[] invariants, JmlConstraint[] constraints, JmlRepresentsDecl[] representsDecls, JmlAxiom[] axioms, JmlVarAssertion[] varAssertions, JTypeDeclaration delegee)

JmlClassDeclaration(TokenReference where, boolean isWeakSubtype, boolean[] interfaceWeaklyFlags, JmlInvariant[] invariants, JmlConstraint[] constraints, JmlRepresentsDecl[] representsDecls, JmlAxiom[] axioms, JmlVarAssertion[] varAssertions, JClassDeclarationWrapper delegee)
Constructs a new JML class declaration; clients should use factory method makeInstance instead.

JmlInterfaceDeclaration(TokenReference where, boolean[] interfaceWeaklyFlags, JmlInvariant[] invariants, JmlConstraint[] constraints, JmlRepresentsDecl[] representsDecls, JmlAxiom[] axioms, JmlVarAssertion[] varAssertions, JInterfaceDeclarationWrapper delegee)
Constructs a new JML interface declaration; clients should use factory method makeInstance instead.

Uses of JmlInvariant in org.jmlspecs.jmldoc.jmldoc_142

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

void	SpecWriter.visitJmlInvariant(JmlInvariant self)

Uses of JmlInvariant in org.jmlspecs.jmlrac

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

RacNode	TransInvariant.translate(JmlInvariant[] invariants) Generates both static and instance invariant check methods and return them.
private RacNode	TransInvariant.translate(JmlInvariant[] invariants, boolean forStatic) Generates and returns a static or an instance invariant check method for the given invariant clauses, invariants.
private static boolean	TransInvariant.isCheckable(JmlInvariant inv) Returns true if the given invariant clause is checkable.
void	RacPrettyPrinter.visitJmlInvariant(JmlInvariant self) Prints a JML invariant.