Э. Дейкстра. ”Дисциплина программирования” 51
(Этот пример обнаруживает некоторое сходство со вторым примером данной главы. Заметим, однако,
что в этом примере допускается равенство n нулю. В таком случае интервал возможных значений для
квантора "∀" пуст и должно быть верным, что всешесть = истина.) По аналогии со вторым примером
введем инвариантное отношение
P : всешесть =(∀i:0≤i<j:f(i)=6))and 0 ≤ j ≤ n
поскольку это отношение легко сделать истинным при j =0иктомуже(Pand j = n) ⇒ R .
Единственное, что мы должны сделать, это понять, как увеличивать j при инвариантности P .Поэтому
берем
wp("j := j +1",P)=(всешесть =(∀i:0≤i<j+1:f(i)=6))and 0 ≤ j +1≤n
Справедливость последнего члена следует из справедливости P and j 6= n; и в этом нет никакой
проблемы, так как мы уже решили, что условие j 6= n, взятое в качестве предохранителя, является
остаточно слабым, чтобы делать выводы о значении