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 Link icon

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

    • minLen Link icon

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

      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.