Annotation Interface EnsuresPresent
@Documented
@Retention(RUNTIME)
@Target({METHOD,CONSTRUCTOR})
@PostconditionAnnotation(qualifier=Present.class)
@InheritedAnnotation
public @interface EnsuresPresent
Indicates that the expression evaluates to a non-empty Optional, if the method terminates
successfully.
This postcondition annotation is useful for methods that construct a non-empty Optional:
@EnsuresPresent("optStr")
void initialize() {
optStr = Optional.of("abc");
}
It can also be used for a method that fails if a given Optional value is empty, indicating that
the argument is null if the method returns normally:
/** Throws an exception if the argument is empty. */
@EnsuresPresent("#1")
void useTheOptional(Optional<T> arg) { ... }
- See Also:
- See the Checker Framework Manual:
- Optional Checker
-
Required Element Summary
-
Element Details
-
value
String[] valueThe expression (of Optional type) that is present, if the method returns normally.- Returns:
- the expression (of Optional type) that is present, if the method returns normally
-