org.checkerframework.checker.nullness.qual

Annotation Type EnsuresKeyForIf

@Documented
 @Retention(value=RUNTIME)
 @Target(value={METHOD,CONSTRUCTOR})
 @ConditionalPostconditionAnnotation(qualifier=KeyFor.class)
 @InheritedAnnotation
 @Repeatable(value=EnsuresKeyForIf.List.class)
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
String[]	expression Java expressions that are keys in the given maps after the method returns the given result.
String[]	map
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 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

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

Returns:

Java expressions whose values are maps, each of which contains each expression value as a key (after the method returns the given result)

See the Checker Framework Manual:

Syntax of Java expressions