org.checkerframework.checker.nullness.qual

Annotation Type EnsuresKeyFor

@Documented
 @Retention(value=RUNTIME)
 @Target(value={METHOD,CONSTRUCTOR})
 @PostconditionAnnotation(qualifier=KeyFor.class)
 @InheritedAnnotation
public @interface EnsuresKeyFor

Indicates that the value expressions evaluate to a value that is a key in all the given maps, if the method terminates successfully.

Consider the following method from java.util.Map:

 @EnsuresKeyFor(value="key", map="this")
 public @Nullable V put(K key, V value) { ... }
 

This method guarantees that key has type @KeyFor("this") after the method returns.

See Also:

KeyFor, EnsuresKeyForIf

See the Checker Framework Manual:

Map Key Checker

Required Element Summary

Required Elements

Modifier and Type	Required Element and Description
String[]	map Java expressions that are maps, each of which contains each of the expressions' value on successful method termination.
String[]	value Java expressions that are keys in the given maps on successful method termination.

Element Detail

value

public abstract String[] value

Java expressions that are keys in the given maps on successful method termination.

See the Checker Framework Manual:

Syntax of Java expressions

map

@JavaExpression
 @QualifierArgument(value="value")
public abstract String[] map

Java expressions that are maps, each of which contains each of the expressions' value on successful method termination.

See the Checker Framework Manual:

Syntax of Java expressions