Array Shift Proof


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


    k := a


    while k < b do

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

    endwhile

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