Package org.checkerframework.framework.qual

Annotation Interface FieldInvariant

@Documented @Retention(RUNTIME) @Target(TYPE) @Inherited public @interface FieldInvariant
Specifies that a field's type, in the class on which this annotation is written, is a subtype of its declared type. The field must be declared in a superclass and must be final.

The @FieldInvariant annotation does not currently accommodate type qualifiers with attributes, such as @MinLen(1). In this case, the type system should implement its own field invariant annotation and override AnnotatedTypeFactory.getFieldInvariantDeclarationAnnotations() and AnnotatedTypeFactory.getFieldInvariants(). See MinLenFieldInvariant for an example.

See the Checker Framework Manual:
Field invariants

  • Required Element Summary

    Required Elements
    Modifier and Type
    Required Element
    Description
    String[]
    field
    The field that has a more precise type, in the class on which the FieldInvariant annotation is written.
    Class<? extends Annotation>[]
    qualifier
    The qualifier on the field.

  • Element Details

    • qualifier

      Class<? extends Annotation>[] qualifier
      The qualifier on the field. Must be a subtype of the qualifier on the declaration of the field.

    • field

      String[] field
      The field that has a more precise type, in the class on which the FieldInvariant annotation is written. The field must be declared in a superclass and must be final.