Package org.checkerframework.checker.optional.qual

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 present 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

    Required Elements
    Modifier and Type
    Required Element
    Description
    String[]
    value
    The expression (of Optional type) that is present, if the method returns normally.

  • Element Details

    • value

      String[] value
      The 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