О перечислении
Я считаю, что мы прибегаем к перечислению, когда пытаемся проверить правильность вычислений, которые сводятся к обозримому множеству последовательно выполняемых операторов, включая условные операторы выбора одного из двух или более вариантов. Приведу простой пример "рассуждения с перечислением".
Требуется доказать, что последовательное выполнение следующих двух операторов:
dd:=dd/2; if dd r do r:=r-dd
применительно к переменным r и dd сохраняет отношения
0 r < dd(1)
инвариантными. Достаточно "проследить" этот кусочек программы, предположив, что первоначально условие (1) выполняется. После выполнения первого оператора, уменьшающего вдвое значение dd, но не изменяющего r, будут выполняться отношения
0 r < 2*dd (2)
Теперь выделим два взаимно исключающих случая.
- ddr. В сочетании с (2) это приводит к отношениям
dd r < 2*dd (3)
В этом случае будет выполнен оператор, следующий за do. В результате r уменьшится на dd, и из (3) следует, что в конечном итоге
0 r < dd
т. е. отношение (1) будет выполняться.
- Отрицание ddr (т. е. dd>r).
В этом случае следующий за do оператор будет пропущен, и поэтому окончательным будет неизмененное значение r. В этом случае сочетание отношений dd>r и (2), справедливого после выполнения первого оператора, приводит сразу к
0 r < dd
так что и во втором случае будет выполняться условие (1).
Итак, мы завершили доказательство инвариантности отношения (1); одновременно мы завершили пример рассуждения с перечислением, включающий условия.
