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

Nested and Inner Type Summary

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

Method Summary

Modifier and Type	Method and Description
public String[]	expression() Java expressions that are keys in the given maps after the method returns the given result.
public String[]	Returns: Java expressions whose values are maps, each of which contains each expression value as a key (after the method returns the given result) 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).
public boolean	result() The value the method must return, in order for the postcondition to hold.

Inherited from java.lang.annotation.Annotation:: annotationType equals hashCode toString

Method Detail

expression	back to summary
public String[] expression() Java expressions that are keys in the given maps after the method returns the given result.

map	back to summary
public 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:String[] Java expressions whose values are maps, each of which contains each expression value as a key (after the method returns the given result) Annotations @JavaExpression @QualifierArgument:value

map

back to summary

public 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:String[]

Java expressions whose values are maps, each of which contains each expression value as a key (after the method returns the given result)

Annotations

@JavaExpression
@QualifierArgument:value

result	back to summary
public boolean result() The value the method must return, in order for the postcondition to hold.

org.checkerframework.checker.nullness.qual back to summary

public @Interface EnsuresKeyForIf.List

Annotations

extends Annotation

@Documented
@Retention:RUNTIME
@Target:METHOD, CONSTRUCTOR
@ConditionalPostconditionAnnotation
qualifier:KeyFor
@InheritedAnnotation

A wrapper annotation that makes the EnsuresKeyForIf annotation repeatable.

Programmers generally do not need to write this. It is created by Java when a programmer writes more than one EnsuresKeyForIf annotation at the same location.

Method Summary

Modifier and Type	Method and Description
public EnsuresKeyForIf[]	Returns: the repeatable annotations value() Returns the repeatable annotations.

Inherited from java.lang.annotation.Annotation:: annotationType equals hashCode toString

Method Detail

value	back to summary
public EnsuresKeyForIf[] value() Returns the repeatable annotations. Returns:EnsuresKeyForIf[] the repeatable annotations

value

back to summary

public EnsuresKeyForIf[] value()

Returns the repeatable annotations.

Returns:EnsuresKeyForIf[]: the repeatable annotations