EnsuresKeyForIf (checker-framework 3.39.0-eisop1 API)

```
@Documented
@Retention(RUNTIME)
@Target({METHOD,CONSTRUCTOR})
@ConditionalPostconditionAnnotation(qualifier=KeyFor.class)
@InheritedAnnotation
@Repeatable(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	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`	Returns Java expressions whose values are maps, each of which contains each expression value as a key (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
```
boolean result
```
    The value the method must return, in order for the postcondition to hold.
- - expression
```
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
```
@JavaExpression
@QualifierArgument("value")
java.lang.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).
    
    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