Generating the invariant for array use often involves dividing the array into 2 parts: the part already processed in the loop, and the lart yet to be processed.
{ INV: a<=k<=b and forall i, a <= i < k : x[i]=x0[i+1] and forall i, k <= i <= b : x[i]=x0[i] }We want to say:
a <= k <= b
i < k ==> x[i] = x0[i+1]
i >= k ==> x[i] = x0[i]