{ 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 { P3: P2 with k replaced by k+1 } 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] }