Proof Example: Using Arrays

Consider this program to do a left shift of array elements...
indices run from a to b, x[a] is altered, but x[b] stays the same

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