org.checkerframework.checker.nullness.qual

Annotation Type EnsuresKeyForIf

@Documented
 @Retention(value=RUNTIME)
 @Target(value={METHOD,CONSTRUCTOR})
 @InheritedAnnotation
public @interface EnsuresKeyForIf

Indicates that the given expressions evaluate to a value that is a key in all the given maps, if the method returns the given result (either true or false).

As an example, consider the following method in java.util.Map:

   @EnsuresKeyForIf(result=true, expression="key", map="this")
   public boolean containsKey(String key) { ... }
 

If an invocation m.containsKey(k) returns true, then the type of k can be inferred to be @KeyFor("m").

See Also:

KeyFor, EnsuresKeyFor

See the Checker Framework Manual:

Map Key Checker

Required Element Summary

Required Elements

Modifier and Type	Required Element and Description
java.lang.String[]	expression Java expressions that are keys in the given maps after the method returns the given result.
java.lang.String[]	map Java expressions that are maps, each of which contains each of the expressions' value after the method returns the given result.
boolean	result The value the method must return, in order for the postcondition to hold.

Element Detail

result

public abstract boolean result

The value the method must return, in order for the postcondition to hold.

expression

public abstract java.lang.String[] expression

Java expressions that are keys in the given maps after the method returns the given result.

See the Checker Framework Manual:

Syntax of Java expressions

map

public abstract java.lang.String[] map

Java expressions that are maps, each of which contains each of the expressions' value after the method returns the given result.

See the Checker Framework Manual:

Syntax of Java expressions