Class | Description |
---|---|
KeYJMLPreLexer | |
KeYJMLPreLexerTokens |
This class provides better literals to the tokens in the jml preparser.
|
KeYJMLPreParser | |
TextualJMLClassAxiom |
A JML axiom declaration in textual form.
|
TextualJMLClassInv |
A JML class invariant declaration in textual form.
|
TextualJMLConstruct |
Objects of this type represent the various JML specification constructs in textual, unprocessed
form.
|
TextualJMLDepends |
A JML depends / accessible clause for a model field in textual form.
|
TextualJMLFieldDecl |
A JML field declaration (ghost or model) in textual form.
|
TextualJMLInitially |
A JML initially clause declaration in textual form.
|
TextualJMLLoopSpec |
A JML loop specification (invariant, assignable clause, decreases
clause, ...) in textual form.
|
TextualJMLMergePointDecl |
A JML merge point declaration in textual form.
|
TextualJMLMethodDecl |
A JML model method declaration in textual form.
|
TextualJMLRepresents |
A JML represents clause in textual form.
|
TextualJMLSetStatement |
A JML set statement in textual form.
|
TextualJMLSpecCase |
A JML specification case (i.e., more or less an operation contract) in
textual form.
|
Enum | Description |
---|---|
Behavior |
Enum type for the JML behavior kinds.
|