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] }Prove that this program is correct with respect to the given PRE and POST specifications...