Indicates that the value of the given expression is a sequence containing at least the given number of elements, if the method returns the given result (either true or false).

When the annotated method returns result, then all the expressions in expression are considered to be MinLen(targetValue).

Nested and Inner Type Summary

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

Method Summary

Modifier and Type	Method and Description
public String[]	Returns: an array of Java expression(s), each of which is a sequence with the given minimum length after the method returns `result` expression() Returns Java expression(s) that are a sequence with the given minimum length after the method returns `result`.
public boolean	Returns: the return value of the method under which the postcondition to hold result() Returns the return value of the method under which the postcondition to hold.
public int	Returns: the minimum number of elements in the sequence targetValue() Returns the minimum number of elements in the sequence.

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

Method Detail

expression back to summary

expression	back to summary
public String[] expression() Returns Java expression(s) that are a sequence with the given minimum length after the method returns `result`. Returns:String[] an array of Java expression(s), each of which is a sequence with the given minimum length after the method returns `result`

public String[] expression()

Returns Java expression(s) that are a sequence with the given minimum length after the method returns result.

Returns:String[]: an array of Java expression(s), each of which is a sequence with the given minimum length after the method returns result

result	back to summary
public boolean result() Returns the return value of the method under which the postcondition to hold. Returns:boolean the return value of the method under which the postcondition to hold

result

back to summary

public boolean result()

Returns the return value of the method under which the postcondition to hold.

Returns:boolean: the return value of the method under which the postcondition to hold

targetValue	back to summary
public int targetValue() Returns the minimum number of elements in the sequence. Returns:int the minimum number of elements in the sequence Annotations @QualifierArgument:value

targetValue

back to summary

public int targetValue()

Returns the minimum number of elements in the sequence.

Returns:int

the minimum number of elements in the sequence

Annotations

@QualifierArgument:value

org.checkerframework.common.value.qual back to summary

public @Interface EnsuresMinLenIf.List

Annotations

extends Annotation

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

A wrapper annotation that makes the EnsuresMinLenIf annotation repeatable.

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

Method Summary

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

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

Method Detail

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

value

back to summary

public EnsuresMinLenIf[] value()

Return the repeatable annotations.

Returns:EnsuresMinLenIf[]: the repeatable annotations