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