{ 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] }