Package org.checkerframework.common.value.qual

Annotation Type 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
      java.lang.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 Detail

      • minLen

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

      • field

        java.lang.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.