Package org.checkerframework.common.value.qual

Annotation Interface MinLenFieldInvariant

@Documented @Retention(RUNTIME) @Target(TYPE) @Inherited public @interface MinLenFieldInvariant
A specialization of FieldInvariant for specifying the minimum length of an array. A class can be annotated with both this annotation and a FieldInvariant annotation.
See the Checker Framework Manual:
Field invariants

  • Required Element Summary

    Required Elements
    Modifier and Type
    Required Element
    Description
    String[]
    field
    The field that has an array length qualifier in the class on which the field invariant is written.
    int[]
    minLen
    Min length of the array.

  • Element Details

    • minLen

      int[] minLen
      Min length of the array. Must be greater than the min length of the array as declared in the superclass.

    • field

      String[] field
      The field that has an array length qualifier in the class on which the field invariant is written. The field must be final and declared in a superclass.