Package org.checkerframework.checker.nonempty.qual

Annotation Interface EnsuresNonEmpty

@Retention(RUNTIME)
@Target({METHOD,CONSTRUCTOR})
@PostconditionAnnotation(qualifier=NonEmpty.class)
@InheritedAnnotation
public @interface EnsuresNonEmpty

Indicates that a particular expression evaluates to a non-empty value, if the method terminates successfully.

This annotation applies to Collection, Iterator, Iterable, and Map, but not Optional.

This postcondition annotation is useful for methods that make a value non-empty by side effect:

   @EnsuresNonEmpty("ids")
   void addId(String id) {
     ids.add(id);
   }
 

It can also be used for a method that fails if a given value is empty, indicating that the argument is non-empty if the method returns normally:

   /** Throws an exception if the argument is empty. */
   @EnsuresNonEmpty("#1")
   void useTheMap(Map<T, U> arg) { ... }
 

See Also:

• NonEmpty
• NonEmptyChecker

See the Checker Framework Manual:

Non-Empty Checker

Required Element Summary

Required Elements

Modifier and Type	Required Element	Description
String[]	value	The expression (a collection, iterator, iterable, or map) that is non-empty, if the method returns normally.

Element Details

value

String[] value

The expression (a collection, iterator, iterable, or map) that is non-empty, if the method returns normally.

Returns:

the expression (a collection, iterator, iterable, or map) that is non-empty, if the method returns normally