Annotation 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 
    A wrapper annotation that makes the EnsuresKeyForIf annotation repeatable.
  • Required Element Summary

    Required Elements
    Modifier and Type
    Required Element
    Description
    Java expressions that are keys in the given maps 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).
    boolean
    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

      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