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