Заметки по структурному программированию

       

О перечислении


Я считаю, что мы прибегаем к перечислению, когда пытаемся проверить правильность вычислений, которые сводятся к обозримому множеству последовательно выполняемых операторов, включая условные операторы выбора одного из двух или более вариантов. Приведу простой пример "рассуждения с перечислением".

Требуется доказать, что последовательное выполнение следующих двух операторов:

dd:=dd/2; if dd r do r:=r-dd

применительно к переменным r и dd сохраняет отношения

0 r < dd(1)

инвариантными. Достаточно "проследить" этот кусочек программы, предположив, что первоначально условие (1) выполняется. После выполнения первого оператора, уменьшающего вдвое значение dd, но не изменяющего r, будут выполняться отношения

0 r < 2*dd     (2)

Теперь выделим два взаимно исключающих случая.

  1. ddr. В сочетании с (2) это приводит к отношениям

    dd r < 2*dd     (3)

    В этом случае будет выполнен оператор, следующий за do. В результате r уменьшится на dd, и из (3) следует, что в конечном итоге

    0 r < dd

    т. е. отношение (1) будет выполняться.

  2. Отрицание ddr (т. е. dd>r).

    В этом случае следующий за do оператор будет пропущен, и поэтому окончательным будет неизмененное значение r. В этом случае сочетание отношений dd>r и (2), справедливого после выполнения первого оператора, приводит сразу к

    0 r < dd

    так что и во втором случае будет выполняться условие (1).

Итак, мы завершили доказательство инвариантности отношения (1); одновременно мы завершили пример рассуждения с перечислением, включающий условия.



Содержание раздела