Array Shift Proof

{ PRE: a <= b and x = x0 }
    { P1: a<=a<=b and forall i, a <= i <  a : x[i]=x0[i+1]
                  and forall i, a <= i <= b : x[i]=x0[i]   }
    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
      { P2: INV with x replace by alpha(x,k-1,x[k]) }
      x[k-1] := x[k]
      { INV }
    endwhile

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