5.3.3 Arraylength

The syntax of an arraylength-expression is as follows:

     arraylength-expression ::= \length(expression)

An arraylength-expression can be used without restrictions. If Expr is an expression with as type a reference to an array, the expression \length(Expr) denotes the length of the array pointed to be Expr. If Expr does not point to an array this is a typing error. At source code level, for every array a, the expression a.length can be used to inspect the length of the array. Occurrence of such an expression in the program code compiles into the special bytecode instruction arraylength. The BML arraylength-expression allows to express properties using the array length also in bytecode-level specifications. Thus, given that the source code level expression (with array type) Expr-s compiles into the bytecode level expression Expr-b, the semantics of \length(Expr-b) corresponds to the semantics of Expr-s.length.