org.checkerframework.framework.qual

Annotation Type PreconditionAnnotation

@Target(value=ANNOTATION_TYPE)
 @Retention(value=RUNTIME)
public @interface PreconditionAnnotation

A meta-annotation that indicates that an annotation is a precondition annotation, i.e., a type-specialized version of RequiresQualifier. The annotation that is annotated as PreconditionAnnotation must have a value called value that is an array of Strings of the same format and with the same meaning as the value expression in RequiresQualifier.

The value qualifier that is necessary for a precondition specified with RequiresQualifier is hard-coded here with the value qualifier.

Author:

Stefan Heule

See Also:

RequiresQualifier

Required Element Summary

Required Elements

Modifier and Type	Required Element and Description
java.lang.Class<? extends java.lang.annotation.Annotation>	qualifier The hard-coded qualifier for the precondition.

Element Detail

qualifier

public abstract java.lang.Class<? extends java.lang.annotation.Annotation> qualifier

The hard-coded qualifier for the precondition.