org.checkerframework.common.value.qual

Annotation Type MinLenFieldInvariant

@Documented
 @Retention(value=RUNTIME)
 @Target(value=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 and 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 Detail

minLen

public abstract int[] minLen

Min length of the array. Must be greater than the min length of the array as declared in the superclass.

field

public abstract 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.