Э. Дейкстра Дисциплина программирования

Э. Дейкстра. ”Дисциплина программирования” 51

(Этот пример обнаруживает некоторое сходство со вторым примером данной главы. Заметим, однако, что в этом примере допускается равенство n нулю. В таком случае интервал возможных значений для квантора "8" пуст и должно быть верным, что всешесть = истина.) По аналогии со вторым примером введем инвариантное отношение

P : всешесть = (8i : 0 i < j : f(i) = 6)) and 0 j n

поскольку это отношение легко сделать истинным при j = 0 и к тому же (P and j = n) ) R . Единственное, что мы должны сделать, это понять, как увеличивать jпри инвариантности P. Поэтому берем

wp("j := j + 1";P) = (всешесть = (8i : 0 i < j + 1 : f(i) = 6)) and 0 j + 1 n

Справедливость последнего члена следует из справедливости P and j 6= n; и в этом нет никакой проблемы, так как мы уже решили, что условие j 6= n, взятое в качестве предохранителя, является остаточно слабым, чтобы делать выводы о значении