 Array bounds

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.