@Documented @Retention(value=RUNTIME) @Target(value={METHOD,CONSTRUCTOR}) @InheritedAnnotation public @interface EnsuresNonNullIf
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();
NonNull
,
EnsuresNonNull
,
NullnessChecker
Modifier and Type | Required Element and Description |
---|---|
String[] |
expression
Java expression(s) that are non-null after the method returns the
given result.
|
boolean |
result
The return value of the method that needs to hold for the postcondition
to hold.
|
public abstract String[] expression