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