Annotation Type  Description 

EnsuresLTLengthOf 
Indicates that the value expressions evaluate to an integer whose value is less than the lengths
of all the given sequences, if the method terminates successfully.

EnsuresLTLengthOfIf 
Indicates that the given expressions evaluate to an integer whose value is less than the lengths
of all the given sequences, if the method returns the given result (either true or false).

GTENegativeOne 
The annotated expression evaluates to an integer greater than or equal to 1.

HasSubsequence 
A sequence whose declaration is annotated with this annotation contains a named subsequence.

IndexFor 
An integer that can be used to index any of the given sequences.

IndexOrHigh 
An integer that, for each of the given sequences, is either a valid index or is equal to the
sequence's length.

IndexOrLow 
An integer that is either 1 or is a valid index for each of the given sequences.

LengthOf 
An integer that, for each of the given sequences, is equal to the sequence's length.

LessThan 
An annotation indicating the relationship between values with a byte, short, char, int, or long
type.

LessThanBottom  
LessThanUnknown  
LowerBoundBottom 
The bottom type of the lower bound type system.

LowerBoundUnknown 
The annotated expression evaluates to value that might be 2 or lower.

LTEqLengthOf 
The annotated expression evaluates to an integer whose value is less than or equal to the lengths
of all the given sequences.

LTLengthOf 
The annotated expression evaluates to an integer whose value is less than the lengths of all the
given sequences.

LTOMLengthOf 
The annotated expression evaluates to an integer whose value is at least 2 less than the lengths
of all the given sequences.

NegativeIndexFor 
The annotated expression is between
1 and a.length  1 , inclusive, for each
sequence a listed in the annotation. 
NonNegative 
The annotated expression evaluates to an integer greater than or equal to 0.

PolyIndex 
A polymorphic qualifier for the Lower Bound and Upper Bound type systems.

PolyLength 
Syntactic sugar for both @PolyValue and @PolySameLen.

PolyLowerBound 
A polymorphic qualifier for the Lower Bound type system.

PolySameLen 
A polymorphic qualifier for the SameLen type system.

PolyUpperBound 
A polymorphic qualifier for the Upper Bound type system.

Positive 
The annotated expression evaluates to an integer greater than or equal to 1.

SameLen 
An expression whose type has this annotation evaluates to a value that is a sequence, and that
sequence has the same length as the given sequences.

SameLenBottom 
The bottom type in the SameLen type system.

SameLenUnknown 
This type represents any variable that isn't known to have the same length as another sequence.

SearchIndexBottom 
The bottom type in the Search Index type system.

SearchIndexFor 
The annotated expression evaluates to an integer whose length is between
a.length  1
and a.length  1 , inclusive, for all sequences a listed in the annotation. 
SearchIndexUnknown 
The top type for the SearchIndex type system.

SubstringIndexBottom 
The bottom type in the Substring Index type system.

SubstringIndexFor 
The annotated expression evaluates to either 1 or a nonnegative integer less than the lengths
of all the given sequences.

SubstringIndexUnknown 
The top type for the Substring Index type system.

UpperBoundBottom 
The bottom type in the Upper Bound type system.

UpperBoundUnknown 
A variable not known to have a relation to any sequence length.
