Uses of Class
org.jmlspecs.jml4.ast.JmlInitiallyClause

Packages that use JmlInitiallyClause

org.jmlspecs.jml4.ast
org.jmlspecs.jml4.rac

Uses of JmlInitiallyClause in org.jmlspecs.jml4.ast

Fields in org.jmlspecs.jml4.ast declared as JmlInitiallyClause

static JmlInitiallyClause[]

JmlInitiallyClause.EMPTY_INITIALLY_ARRAY

Methods in org.jmlspecs.jml4.ast with parameters of type JmlInitiallyClause

void	JmlTypeDeclaration.setInitiallyClauses(JmlInitiallyClause[] clauses)

Uses of JmlInitiallyClause in org.jmlspecs.jml4.rac

Methods in org.jmlspecs.jml4.rac with parameters of type JmlInitiallyClause

void	JmlAstVisitor.endVisit(JmlInitiallyClause jmlInitiallyClause, CompilationUnitScope scope)
void	DefaultRacAstVisitor.endVisit(JmlInitiallyClause jmlInitiallyClause, CompilationUnitScope scope)
void	AstDirtyBitsRetriever.endVisit(JmlInitiallyClause jmlInitiallyClause, CompilationUnitScope scope)
void	AstDirtyBitsRestorer.endVisit(JmlInitiallyClause jmlInitiallyClause, CompilationUnitScope scope)
boolean	JmlAstVisitor.visit(JmlInitiallyClause jmlInitiallyClause, CompilationUnitScope scope) Is used to specify the initial state of model fields.
boolean	DefaultRacAstVisitor.visit(JmlInitiallyClause jmlInitiallyClause, CompilationUnitScope scope)
boolean	AstDirtyBitsRetriever.visit(JmlInitiallyClause jmlInitiallyClause, CompilationUnitScope scope)
boolean	AstDirtyBitsRestorer.visit(JmlInitiallyClause jmlInitiallyClause, CompilationUnitScope scope)