Top Description Methods
org.checkerframework.common.value.qual

public @Interface MinLenFieldInvariant

extends Annotation
Annotations
@Documented
@Retention:RUNTIME
@Target:TYPE
@Inherited
Imports
java.lang.annotation.Documented, .ElementType, .Inherited, .Retention, .RetentionPolicy, .Target, org.checkerframework.framework.qual.FieldInvariant
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.

Method Summary

Modifier and TypeMethod and Description
public String[]
field()

The field that has an array length qualifier in the class on which the field invariant is written.

public int[]
minLen()

Min length of the array.

Inherited from java.lang.annotation.Annotation:
annotationTypeequalshashCodetoString

Method Detail

fieldback to summary
public 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.

minLenback to summary
public int[] minLen()

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