Indicates that the value expressions are non-null just after a method call, if the method terminates successfully.

This postcondition annotation is useful for methods that initialize a field:

 @EnsuresNonNull("theMap")
 void initialize() {
   theMap = new HashMap<>();
 }

It can also be used for a method that fails if a given expression is null, indicating that the argument is null if the method returns normally:

 /** Throws an exception if the argument is null. */
 @EnsuresNonNull("#1")
 void assertNonNull(Object arg) { ... }