Generating the Invariant

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:

k is somewhere between a and b:
```
   a <= k <= b
```
for elements done, shift holds:
```
   i < k ==> x[i] = x0[i+1]
```
for elements not done, no shift:
```
   i >= k ==> x[i] = x0[i]
```