Indicates that the given expressions are non-null, if the method returns the given result (either true or false).

Here are ways this conditional postcondition annotation can be used:

Method parameters: A common example is that the equals method is annotated as follows:

@EnsuresNonNullIf(expression="#1", result=true)
  public boolean equals(@Nullable Object obj) { ... }

because, if equals returns true, then the first (#1) argument to equals was not null.

Fields: The value expressions can refer to fields, even private ones. For example:

@EnsuresNonNullIf(expression="this.derived", result=true)
  public boolean isDerived() {
    return (this.derived != null);
  }

As another example, an Iterator may cache the next value that will be returned, in which case its hasNext method could be annotated as:

@EnsuresNonNullIf(expression="next_cache", result=true)
  public boolean hasNext() {
    if (next_cache == null) {
      return false;
    }
    ...
  }

An EnsuresNonNullIf annotation that refers to a private field is useful for verifying that client code performs needed checks in the right order, even if the client code cannot directly affect the field.

Method calls: If Class#isArray() returns true, then Class#getComponentType() returns non-null. You can express this relationship as:

@EnsuresNonNullIf(expression="getComponentType()", result=true)
  public native @Pure boolean isArray();

You can write two @EnsuresNonNullIf annotations on a single method:

    @EnsuresNonNullIf(expression="outputFile", result=true)
    @EnsuresNonNullIf(expression="memoryOutputStream", result=false)
    public boolean isThresholdExceeded() { ... }