| Annotation Type |
Description |
|
AnnotationProcessorImplementation
|
|
|
ClassInvariant
|
Indicates that annotations being marked as @ClassInvariant are to be treated
as class invariant modifying annotations. |
|
ContractElement
|
Indicates that annotations being marked as @ContractElement are to be used
by some contract element being either a class-invariant, pre- or post-condition. |
|
Postcondition
|
Indicates that annotations being marked as @Postcondition are to be treated
as post-condition modifying annotations. |
|
Precondition
|
Indicates that annotations being marked as @Precondition are to be treated
as pre-condition modifying annotations. |