An annotation indicating the length of an array or a string. If an expression's type has this annotation, then at run time, the expression evaluates to an array or a string whose length is one of the annotation's arguments.

For example, String @ArrayLen(2) [] is the type for an array of two strings, and String @ArrayLen({1, 2, 4, 8}) [] is the type for an array that contains 1, 2, 4, or 8 strings.