Array index ($i$)

An integer identifying a position in an array. With zero-based indexing and capacity $m$, valid array indices are $0,\dots ,m-1$. An array index identifies the slot rather than its stored value.

The permitted array indices for a length-$n$ array are $0,\dots ,n-1$ under zero-based indexing. A one-past-the-end index $n$ can describe an empty remaining segment but cannot be dereferenced. Proving bounds safety requires showing that every executed read and write uses a permitted index, including evaluations in a loop guard. A known target inside the array can sometimes supply a stronger loop invariant than an explicit bounds test.