EnsuresKeyFor (checker-framework 3.39.0-eisop1 API)

```
@Documented
@Retention(RUNTIME)
@Target({METHOD,CONSTRUCTOR})
@PostconditionAnnotation(qualifier=KeyFor.class)
@InheritedAnnotation
@Repeatable(List.class)
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	Description
`java.lang.String[]`	`map`	Returns Java expressions whose values are maps, each of which contains each expression value as a key (after successful method termination).
`java.lang.String[]`	`value`	Java expressions that are keys in the given maps on successful method termination.

- Element Detail
  - value
```
java.lang.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")
java.lang.String[] map
```
    Returns Java expressions whose values are maps, each of which contains each expression value as a key (after successful method termination).
    
    Returns:
    
    Java expressions whose values are maps, each of which contains each expression value as a key (after successful method termination)
    
    See the Checker Framework Manual:
    Syntax of Java expressions