Package org.checkerframework.checker.nullness.qual

Annotation Interface EnsuresKeyForIf

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

  • Nested Class Summary

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

  • Required Element Summary

    Required Elements
    Modifier and Type
    Required Element
    Description
    String[]
    expression
    Java expressions that are keys in the given maps after the method returns the given result.
    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 Details

    • result

      boolean result
      The value the method must return, in order for the postcondition to hold.

    • expression

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