| 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.
|