Package org.checkerframework.checker.nullness.qual

Annotation Interface EnsuresKeyFor

@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:
See the Checker Framework Manual:
Map Key Checker

  • Nested Class Summary

    Nested Classes
    Modifier and Type
    Class
    Description
    static @interface 
    EnsuresKeyFor.List
    A wrapper annotation that makes the EnsuresKeyFor annotation repeatable.

  • Required Element Summary

    Required Elements
    Modifier and Type
    Required Element
    Description
    String[]
    map
    Returns Java expressions whose values are maps, each of which contains each expression value as a key (after successful method termination).
    String[]
    value
    Java expressions that are keys in the given maps on successful method termination.

  • Element Details

    • value

      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") 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