Annotation Type ContractElement
-
@Documented @Retention(RUNTIME) public @interface 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.