Array Shift Proof

{ PRE: a <= b and x = x0 }


    k := a
    { 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]   }
    while k < b do

      k := k + 1
 
      x[k-1] := x[k]

    endwhile

{ POST: forall i, a <= i < b : x[i] = x0[i+1] }