Class | Description |
---|---|
TextualJMLAssertStatement |
A JML assert/assume statement.
|
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.
|
TextualJMLAssertStatement.Kind | |
TextualJMLLoopSpec.ClauseHd |
Heap-dependent clauses
|
TextualJMLSpecCase.Clause |
Heap-independent clauses
|
TextualJMLSpecCase.ClauseHd |
Heap-dependent clauses
|
Copyright © 2003-2019 The KeY-Project.