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

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

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

    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).

Я особо выделил математическую индукцию потому, что это единственный способ рассуждения, который в конечном итоге позволяет нам совладать с циклами (типа тех, что описываются с помощью заголовков повторения) и с рекурсивными процедурами. Хочу привести один пример.

Рассмотрим последовательность значений d₀, d₁, d₂,d₃, ...

заданную так:

где D - некое заданное значение и f - заданная (вычислимая) функция. Требуется присвоить переменной d значение первого элемента d_k из последовательности, которое удовлетворяет заданному (вычислимому) условию "утв". Известно, что такое значение существует для конечного k. Более формально можно сказать, что требуется установить отношение

d=d_k     (3)

где k задается выражениями

утв(d_k)     (4)

и

non утв (d_i)     (5)

для всех i, удовлетворяющих 0 i < k

Рассмотрим теперь следующий фрагмент программы:

   d:=D
   while non утв (d) do d:=f(d)

Здесь первая строка представляет начальную установку, а вторая представляет цикл, управляемый (надеюсь, не требующим пояснений) заголовком повторения while ... do. (С помощью условия if ... do, использованного в предыдущем примере, семантика заголовка повторения может быть описана формально: текст

    while B do S

семантически эквивалентен тексту

    if B do
    begin S; while B do S end

и означает, что non В - необходимое и достаточное условие прекращения повторений.)

Мы будем называть в конструкции while B do S оператор S "повторяемым оператором" и докажем, что в программе (6) после n-го выполнения повторяемого оператора справедливо (при n0)

d=d_n     (7а)

и

non утв (d_i) для всех значений i, удовлетворяющих 0i<n     (7b)

Методом перечисления убеждаемся в том, что это утверждение справедливо при n=0; мы хотим доказать (также методом перечисления), что если оно справедливо при n=N (N0), то оно справедливо и при n=N+1.

После N-го выполнения повторяемого оператора отношения (7a) и (7b) выполняются при n=N. Для того чтобы произошло (N+1)-е выполнение, необходима и достаточна истинность условия

non утв (d)

которое в силу (7а) для n=N (т. е. при d=d_N) означает

non утв (d_N)

Поэтому условие (7b) справедливо для n=N+1. Кроме того, из равенства d=dN и из (2b) следует, что

f(d)=d_N+1

так что непосредственным результатом (N+1)-го выполнения повторяемого оператора будет установление отношения

d:=f(d)

т. е. отношения (7а) для N=N+1, и таким образом индуктивный переход (7) обоснован.

Теперь покажем, что повторения прекращаются после k-гo выполнения повторяемого оператора. При n>k не может быть n-го выполнения, так как в силу (7b) это означало бы

non утв (d_k)

а это противоречило бы условию (4).

Если повторения прекращаются после n-ro выполнения повторяемого оператора, то необходимое и достаточное условие прекращения повторений, т.е.

non(non утв (d))

в силу (7а) принимает вид

утв (d_n)     (8)

Этим исключается прекращение повторений при n<k, так как оно противоречило бы условию (5). Итак, повторения прекратятся при n=k, и поэтому (3) следует из (7а), (4) следует из (8) и (5) - из (7b). Наше доказательство завершено.

Прежде чем отвлечься от этого примера, иллюстрирующего применение математической индукции в рассуждениях, я хочу сделать несколько дополнительных замечаний, потому что предчувствую, что к этому времени некоторые мои читатели (особенно опытные и компетентные программисты) придут в негодование; речь идет о тех читателях, для которых правильность программы (6) настолько очевидна, что их удивляет вся эта суета: "К чему напыщенное сведение проблемы к условиям (3), (4) и (5), когда всякий знает, что собой представляет первое значение из последовательности, удовлетворяющее некоему условию? Разумеется, он не может ожидать, что мы - люди, загруженные работой,- будем предоставлять такие длинные доказательства с полной математической отделкой всякий раз, когда употребим такой простой цикл, как этот." И так далее ...

Признаюсь чистосердечно: пышность и пространность приведенного выше доказательства раздражают и меня. Однако в настоящее время у меня нет лучшего выхода, если я действительно стремлюсь обосновать правильность этой программы. Впрочем, иногда это вызывает у меня такую же злость, какую я испытывал много лет назад, изучая мудреные доказательства первых простых теорем планиметрии, в которых утверждались факты, не менее очевидные, чeм сами аксиомы Евклида.

Конечно, я не осмеливаюсь утверждать (по крайней мере теперь!), что программист должен предоставлять такое доказательство всякий раз, когда пишет в своей программе простой цикл. Тогда бы он вообще никогда не смог написать программу любого размера! ЭТО было бы столь же нереально, как явное и полное сведение любого доказательства в планиметрии к аксиомам Евклида. (См. раздел "О количественной ограниченности наших возможностей".)

Хочу сделать три вывода из сказанного. Во-первых, когда программист рассматривает конструкцию типа (6) как заведомо правильную, он имеет на это право потому, что знаком с такой конструкцией. Я предпочитаю рассматривать его поведение как неосознанную ссылку на теорему, которую он знает, хотя не исключено, что он никогда не удосуживался сформулировать ее. Когда-то он убедился в ее правильности, хотя, возможно, он уже забыл свой способ доказательства и хотя этот способ (возможно) и непригоден для публикации. Тем не менее мы могли бы сформулировать свое мнение о программе (6) в виде, скажем, "теоремы линейного поиска", а зная такое название, гораздо легче (и более естественно) апеллировать к нему интуитивно.

Во-вторых, насколько мне известно, не существует набора теорем типа рассмотренной выше, полезность которых была бы общепризнанной. Однако не следует удивляться этому, так как отсутствие такого набора теорем является непосредственным следствием того факта, что не сформулировано четко понятие основного объекта, т.е. программы. Тип объекта, с которым имеет дело программист, т.е. программы, значительно менее формализован, чем тип объекта в планиметрии. Между тем развитая интуиция программиста выражается, по-видимому, в том, что он ограничивается по мере возможности хорошо знакомыми структурами программ и проявляет особую осторожность и тщательность при построении необычных (для себя) программных конструкций. Однако для формализации программирования могли бы оказаться полезными поиски теорем, соответствующих таким необычным программам.

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

Если исходить из вычислений, то алгоритм - это то, что остается, если абстрагироваться от конкретных значений обрабатываемых данных. Понятие "переменной" представляет собой абстракцию соответствующего текущего значения. Я слышал (к большому сожалению, не могу вспомнить, от кого) мнение, что, как только человек осознал, как в программировании используются переменные, он понял сущность программирования. Мы можем найти подтверждение этому мнению, если вспомним использование математической индукции применительно к повторениям цикла: с одной стороны, именно благодаря абстракции понятия вводятся таким образом, что удается сформулировать индуктивный переход; с другой стороны, именно организация повторений требует введения понятия "переменной". (При отсутствии повторений мы могли бы ограничиться "величинами", значения которых должны определяться не более чем по одному разу и никогда не переопределяются в отличие от значений переменных.)

Абстракция присутствует также в процессе присваивания операциям имен и использования этих операций с точки зрения того, "что она делает", с полным безразличием к тому, "как она работает". (Аналогично следует считать, что руководство по программированию описывает абстрактную машину: конкретная аппаратура, предоставляемая изготовителем, - это не что иное как механическая - и обычно несовершенная! - модель этой абстрактной машины.) Имеется явная аналогия между использованием в программе именованной операции независимо от того, "как она работает", и использованием теоремы независимо от того, как она доказывалась. Даже если ее доказательство исключительно запутанное, теорема может оказаться очень удобной для практического использования.

Здесь я снова сошлюсь на количественную ограниченность наших возможностей. Рассуждение с перечислением не вызывает нареканий, пока оно проходит, но поскольку мы мыслим довольно медленно, такое рассуждение пройдет не слишком далеко. Рассуждение с перечислением оказывается подходящим интеллектуальным средством только при строгом соблюдении умеренности его применения. Следует рассматривать абстракцию как основной интеллектуальный прием, позволяющий ослабить количественные ограничения, которые накладываются на рассуждение с перечислением.

(В этом месте М. Вуджер из Национальной физической лаборатории, Теддингтон, Англия, сделал замечание, которое я с благодарностью привожу. "Имеется аналогия между неанализируемыми терминами, в которых формулируется аксиома или теорема, и неанализируемыми операндами, к которым предполагается применять именованную операцию".)