Package org.checkerframework.checker.nonempty.qual

Annotation Interface RequiresNonEmpty

@Documented @Retention(RUNTIME) @Target({METHOD,PARAMETER}) @PreconditionAnnotation(qualifier=NonEmpty.class) public @interface RequiresNonEmpty
Indicates a method precondition: the specified expressions that may be a collection, iterator, iterable, or map must be non-empty when the annotated method is invoked.

For example: 

 import java.util.LinkedList;
 import java.util.List;
 import org.checkerframework.checker.nonempty.qual.NonEmpty;
 import org.checkerframework.checker.nonempty.qual.RequiresNonEmpty;
 import org.checkerframework.dataflow.qual.Pure;

 class MyClass {

   List<String> list1 = new LinkedList<>();
   List<String> list2;

   @RequiresNonEmpty("list1")
   @Pure
   void m1() {}

   @RequiresNonEmpty({"list1", "list2"})
   @Pure
   void m2() {}

   @RequiresNonEmpty({"list1", "list2"})
   void m3() {}

   void m4() {}

   void test(@NonEmpty List<String> l1, @NonEmpty List<String> l2) {
     MyClass testClass = new MyClass();

     testClass.m1(); // Compile-time error: m1 requires that list1 is @NonEmpty.

     testClass.list1 = l1;
     testClass.m1(); // OK

     testClass.m2(); // Compile-time error: m2 requires that list2 is @NonEmpty

     testClass.list2 = l2;
     testClass.m2(); // OK

     testClass.m4();

     testClass.m2(); // Compile-time error: m4 is not pure and might have assigned a field.
   }
 }
This annotation should not be used for formal parameters (instead, give them a @NonEmpty type). The @RequiresNonEmpty annotation is intended for non-parameter expressions, such as field accesses or method calls.
See the Checker Framework Manual:
Non-Empty Checker