Array bounds
= Array bounds
The permitted <array indices> for a length-$n$ <array> are $0,\ldots,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.