The Checker Framework Manual:
Custom pluggable types for Java

Chapter 5 Optional Checker for possibly-present data

Use of the Optional Checker guarantees that your program will not suffer a NoSuchElementException when calling methods on an expression of Optional type. The Optional Checker also enforces Stuart Marks’s style guidelines (see below).

Java 8 introduced the Optional class, a container that is either empty or contains a non-null value.

Using Optional is intended to help programmers remember to check whether data is present or not. However, Optional itself is prone to misuse. The article Nothing is better than the Optional type gives reasons to use regular nullable references rather than Optional. However, if you do use Optional, then the Optional Checker will help you avoid Optional’s pitfalls. Most notably, the Optional Checker guarantees that your code will not suffer a NoSuchElementException due to use of an empty Optional.

Stuart Marks gave 7 rules to avoid problems with Optional:

1. Never, ever, use null for an Optional variable or return value.
2. Never use Optional.get() unless you can prove that the Optional is present.
3. Prefer alternative APIs over Optional.isPresent() and Optional.get().
4. It’s generally a bad idea to create an Optional for the specific purpose of chaining methods from it to get a value.
5. If an Optional chain has a nested Optional chain, or has an intermediate result of Optional, it’s probably too complex.
6. Avoid using Optional in fields, method parameters, and collections.
7. Don’t use an Optional to wrap any collection type (List, Set, Map). Instead, use an empty collection to represent the absence of values.

Rule #1 is guaranteed by the Nullness Checker (Chapter 3). Rules #2–#7 are guaranteed by the Optional Checker, described in this chapter. (Exception: Rule #5 is not yet implemented and will be checked by the Optional Checker in the future.)

5.1 How to run the Optional Checker

The standard way to run the Optional Checker is one of these command lines:

javac -processor optional MyFile.java ...
javac -processor org.checkerframework.checker.optional.OptionalChecker MyFile.java ...

5.2 Optional annotations

These qualifiers make up the Optional type system:

@MaybePresent

The annotated Optional container may or may not contain a value. This is the default type, so programmers do not have to write it.

@Present

The annotated Optional container definitely contains a (non-null) value.

@PolyPresent

indicates qualifier polymorphism. For a description of qualifier polymorphism, see Section 32.2.

The subtyping hierarchy of the Optional Checker’s qualifiers is shown in Figure 5.1.

5.2.1 Optional method annotations

The Optional Checker supports several annotations that specify method behavior. These are declaration annotations, not type annotations: they apply to the method itself rather than to some particular type.

@RequiresPresent

indicates a method precondition. The annotated method expects the specified expression to be a present Optional when this method is invoked. @RequiresPresent is a useful annotation for a method that requires a @MaybePresent field to be @Present.

@EnsuresPresent

indicates a method postcondition. The successful return (i.e., a non-exceptional return) of the annotated method results in the given Optional expression being present. See the Javadoc for examples of its use.

@EnsuresPresentIf

indicates a method postcondition. With @EnsuresPresent, the given Optional expression is present after the method returns. With @EnsuresPresentIf, if the annotated method returns the given boolean value (true or false), then the given Optional expression is present. See the Javadoc for examples of its use.

5.3 What the Optional Checker guarantees

The Optional Checker guarantees that your code will not throw a NoSuchElementException due to use of an absent Optional where a present Optional is needed. More specifically, the Optional Checker will issue an error if you call get or orElseThrow() on a @MaybePresent Optional receiver, because the receiver may be absent and each of these methods throws a NoSuchElementException if the receiver is empty at run time.

By contrast, the Optional Checker does not issue an error if you call orElseThrow(Supplier) with a possibly-absent Optional. That method call does not throw NoSuchElementException. The Optional Checker assumes that the programmer has mechanisms in place to handle whatever exception it throws. If you wish for the Optional Checker to warn about calling orElseThrow(Supplier) on a possibly-absent Optional, then you can use a stub file (Section 36.5) to annotate its receiver as @Present.

The Optional Checker does not check nullness properties, such as requiring that the argument to of is non-null or guaranteeing that the result of get is non-null. To obtain such a guarantee, run both the Optional Checker and the Nullness Checker (Chapter 3).

As with any checker, the guarantee is subject to certain limitations (see Section 2.3).

5.4 Suppressing optional warnings

It is often best to change the code or annotations when the Optional Checker reports a warning. Alternatively, you might choose to suppress the warning. This does not change the code but prevents the warning from being presented to you.

The Checker Framework supplies several ways to suppress warnings. The @SuppressWarnings("optional") annotation is specific to warnings raised by the Optional Checker. See Chapter 34 for additional usages. An example use is

    // might return a possibly-empty Optional
    Optional<T> wrapWithOptional(...) { ... }

    void myMethod() {
      @SuppressWarnings("optional") // with argument x, wrapWithOptional always returns a present Optional
      @Present Optional<T> optX = wrapWithOptional(x);
    }

The Optional Checker also permits the use of method calls and assertions to suppress warnings; see immediately below.

5.4.1 Suppressing warnings with assertions and method calls

Occasionally, it is inconvenient or verbose to use the @SuppressWarnings annotation. For example, Java does not permit annotations such as @SuppressWarnings to appear on statements, expressions, static initializers, etc. Here are three ways to suppress a warning in such cases:

• Create a local variable to hold a subexpression, and suppress a warning on the local variable declaration.
• Use the @AssumeAssertion string in an assert message (see Section 34.2).
• Write a call to the OptionalUtil.castPresent method.

The rest of this section discusses the castPresent method. It is useful if you wish to suppress a warning within an expression.

The Optional Checker considers both the return value and the argument to be a present Optional after the castPresent method call. The Optional Checker issues no warnings in any of the following code:

    // One way to use castPresent as a cast:
    @Present Optional<String> optString = castPresent(possiblyEmpty1);

    // Another way to use castPresent as a cast:
    castPresent(possiblyEmpty2).toString();

    // It is possible, but not recommended, to use castPresent as a statement:
    // (It would be better to write an assert statement with @AssumeAssertion
    // in its message, instead.)
    castPresent(possiblyEmpty3);
    possiblyEmpty3.toString();

The castPresent method throws AssertionError if Java assertions are enabled and the argument is an empty Optional. However, it is not intended for general defensive programming; see Section 34.2.1.

To use the castPresent method, the checker-util.jar file must be on the classpath at run time.

The Checker Framework Manual: Custom pluggable types for Java