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

• Название: Предисловие редактора перевода
• Анкор: Э. Дейкстра Дисциплина программирования.pdf
• Дата: 31.08.2018
• Размер: 1.14 Mb.
• Имя файла: Э. Дейкстра Дисциплина программирования.pdf
• Тип: Документы; #23816
• страница: 7 из 9

33
6 О ПРОЕКТИРОВАНИИ ПРАВИЛЬНО ЗАВЕРШАЕМЫХ КОНСТРУКЦИЙ
Основная теорема для конструкции повторения применительно к условию P , сохраняемому ин- вариантно истинным, утверждает, что
(P and wp(DO, T )) ⇒ (DO, P and non BB)
Здесь член wp(DO, T ) представляет собой слабейшее предусловие, такое, что конструкция по- вторения заввершится. Если задана произвольная конструкция DO, то в общем случае очень трудно
(а может быть, невозможно) определить wp(DO, T ). Поэтому я предлагаю проектировать наши кон- струкции повторения, постоянно помня о требовании завершимости, т. е. предлагаю искать подхо- дящее доказательство завершимости и строить программу таким способом, чтобы она удовлетворяла предположениям, на которых основывается это доказательство.
Предположим опять, что P — отношение, которое сохраняется инвариантно истинным, т.е.
(P and BB) ⇒ wp(IF, P )
для всех состояний
Пусть t — конечная целочисленная функция от текущего состояния, такая, что
(P and BB) ⇒ (t > 0)
для всех состояний и, кроме того, для любого значения t
0
и для всех
(P and BB and t ≤ t
0
+ 1)
⇒ wp(IF, t ≤ t
0
)
(3)
Тогда мы докажем, что
P ⇒ wp(DO, T )
для всех состояний
(4)
Сопоставив этот факт с основной теоремой для повторения, мы можем заключить, что имеем для всех состояний
P ⇒ wp(DO, P and non BB)
(5)
Мы покажем это, доказав сначала методом математической индукции, что
(P and t ≤ k) ⇒ H
k
(T )
для всех состояний
(6)
справедливо при всех k ≥ 0. Начнем с обоснования истинности (6) при k = 0. Поскольку H
0
(T ) =
non BB, нам требуется показать, что
(P and t ≤ 0) ⇒ non BB
для всех состояний
(7)
Однако 7 — это просто другая форма записи выражения (2): оба они равны выражению non P or non BB or (t > 0)
и поэтому (6) справедливо при k = 0.
Предположим теперь, что (6) справедливо при k = K; тогда
(P and BB and t ≤ K + l) ⇒ wp(IF, P and t ≤ K)
⇒ wp(IF, H
K
(T ));
(P and non BB and t ≤ K + 1) ⇒ non BB = H
0
(T )
И эти два логических следования можно объединить (из A ⇒ B и B ⇒ D мы можем заключить, что справедливо (A or B ⇒ C or D)):
(P and t ≤ K + 1) ⇒ wp(IF, H
K
(T )) or H
0
(T ) = H
K+1
(T )
и тем самым истинность (6) доказана для всех k ≥ 0. Поскольку t — ограниченная функция, мы имеем
(
∃k : k ≥ 0 : t ≤ k)
и
P ⇒ (∃k : k ≥ 0 : P and t ≤ k)
⇒ (∃k : k ≥ 0 : H
k
(T ))
= wp(DO, T )

34
Э. Дейкстра. ”Дисциплина программирования”
и тем самым доказано (4).
Интуитивно теорема совершенно ясна. С одной стороны, P останется истиной, а следовательно,
t ≥ 0 тоже останется истиной; с другой стороны, из отношения (3) следует, что каждая выборка охраняемой команды приведет к эффективному уменьшению t по крайней мере на 1. Неограниченное количество выборок охраняемых команд уменьшило бы значение t ниже любого предела, что привело бы к противоречию.
Применимость этой теоремы основывается на выполнении условий (2) и (3). Отношение (2) яв- ляется достаточно простым, отношение (3) выглядит более запутанным. Наша основная теорема для конструкции повторения при
Q = (P and BB and t ≤ t
0
+ 1)
R = (t ≤ t
0
)
(присутствие свободной переменной t
0
в обоих предикатах является причиной того, что мы говорили о "паре предикатов") позволяет нам заключить, что условие (3) справедливо, если
(
∀j : 1 ≤ j ≤ n : (P and B
j and t ≤ t
0
+ 1)
⇒ wp(SL
j
, t ≤ t
0
))
Иначе говоря, нам нужно доказать для всякой охраняемой команды, что выборка приведет к эффективному yменьшению t. Помня о том, что t является функцией от текущего состояния, мы можем рассмотреть wp(SL
j
, t ≤ t
0
)
(8)
Это предикат, включающий, помимо координатных переменных пространства состояний, также и свободную переменную t
0
. До сих пор мы рассматривали такой предикат как предикат, характери- зующий некое подмножество состояний. Однако для любого заданного состояния мы можем также рассматривать предикат как условие, налагаемое на t
0
. Пусть t
0
= t min представляет собой мини- мальное решение уравнения (8) относительно t
0
, тогда мы можем интерпретировать значение t min как наименьшую верхнюю границу для конечного значения t. Если вспомнить, что, подобно функ- ции t, t min также является функцией от текущего состояния, то можно интерпретировать предикат t
min
≤ t − 1
как слабейшее предусловие, при котором гарантируется, что выполнение SL
j
, Уменьшит значение t по крайней мере на 1.
Обозначим это предусловие, где — мы повторяем —аргумент является целочисленной функцией от текущего состояния, через wdec(SL
j
, t)
При этом инвариантность P и эффективное уменьшение t гарантируются, если мы имеем при всех значениях j
(P and B
j
)
⇒ (wp(SL
j
, P ) and wdec(SL
j
, t))
Обычно практический способ отыскания подходящего предохранителя B
j состоит в следующем.
Уравнение (9) относится к типу
(P and Q) ⇒ R
где (практически вычислимое!) значение Q нужно найти для заданных значений P и R. Мы замечаем,
что
1. Q = R является решением.
2. Q = (Q1 and Q2) является решением и P ⇒ Q2, то Q1 тоже является решением.
3. Если Q = (Q1 or Q2) является решением и P ⇒ non Q2, (или, что сводится к тому же самому,
(P and Q2) = F ), то Q1 тоже является решением.
4. Если Q является решением и Q1 ⇒ Q, то Q1 тоже является решением.
Замечание 1. Если, действуя таким образом, мы приходим к кандидатуре Q для B
j
, такой, что P ⇒
non Q, то эта кандидатура может быть далее упрощена (в соответствии с предыдущим наблюдением 3,
поскольку при любом Q мы имеем Q = (ложьorQ)) к виду Q = ложь; это означает, что рассматриваемая охраняемая команда введена неудачно: ее можно исключить из набора, потому что она никогда не будет выбираться. (Конец замечания 1.)

Э. Дейкстра. ”Дисциплина программирования”
35
Замечание 2. Часто на практике расщепляют уравнение (9) на два уравнения:
(P and B
j
)
⇒ wp(SL
j
, P )
(9а)
(P and B
j
)
⇒ wdec(SL
j
, t)
(9б)
и рассматривают их по отдельности. Тем самым разделяются две задачи: (9а) относится к тому, что остается инвариантным, тогда как (9б) относится к тому, что обеспечивает продвижение вперед. Если,
имея дело с уравнением (9а), мы приходим к решению B
j
, такому, что P ⇒ B
j
, то тогда очевидно,
что это условие не будет удовлетворять уравнению (9б), поскольку при таком B
j инвариантность P
привела бы к недетерминированности (Конец замечания 2.)
Таким образом, мы можем построить конструкцию DO, такую, что
P ⇒ wp(DO, P and non BB)
Наши условия B
j должны быть достаточно сильными, чтобы удовлетворялись следования (9); в ре- зультате этого новое гарантируемое постусловие P and non BB может оказаться слишком слабым и не обеспечить нам желаемого постусловия R. В таком случае мы все-таки не решили нашу проблему и нам следует рассмотреть другие возможности.

36
Э. Дейкстра. ”Дисциплина программирования”
7 ПЕРЕСМОТРЕННЫЙ АЛГОРИТМ ЕВКЛИДА
Рискуя наскучить моим читателям, я посвящу eще одну главу алгоритму Евклида. Полагаю, что к этому времени некоторые из читателей уже закодируют его в виде x, y := X, Y ;
do x = y → if x > y → x := x − y
[] y > x → y := y − x
od;
печатать(x)
где предохранитель конструкции повторения гарантирует, что конструкция выбора не приведет к отказу. Другие читатели обнаружат, что этот алгоритм можно закодировать более просто следующим образом:
x, y := X, Y ;
do x > y → x := x − y
[] y > x → y := y − x
od;
печатать(x)
Попробуем теперь забыть игру на листе картона и попытаемся изобрести заново алгоритм Ев- клида для отыскания наибольшего общего делителя двух положительных чисел X и Y . Когда мы сталкиваемся с такого рода проблемой, в принципе всегда возможны два подхода.
Первый состоит в том, чтобы пытаться следовать определению требуемого ответа настолько близ- ко, насколько это возможно. По-видимому, мы могли бы сформировать таблицу делителей числа X;
эта таблица содержала бы только конечное число элементов, среди которых имелись бы 1 в качестве наименьшего и X в качестве наибольшего элемента. (Если X = 1, то наименьший и наибольший элементы совпадут. Затем мы могли бы сформировать также аналогичную таблицу делителей Y .
Из этих двух таблиц мы могли бы сформировать таблицу чисел, присутствующих в них обеих. Она представляет собой таблицу общих делителей чисел X и Y и обязательно является непустой, так как содержит элемент 1. Следовательно, из этой третьей таблицы мы можем выбрать (поскольку она тоже конечная!) максимальный элемент, и он был бы наибольшим общим делителем.
Иногда близкое следование определению, подобное обрисованному выше, является лучшим из того, что мы можем сделать. Существует, однако, и другой подход, который стоит испробовать, если мы знаем (или можем узнать) свойства функции, подлежащей вычислению. Может оказаться, что мы знаем так много свойств, что они в совокупности определяют эту функцию, тогда мы можем попытаться построить ответ, используя эти свойства.
В случаe наибольшего общего делителя мы замечаем, например, что, поскольку делители числа
−x те же самые, что и для самого числа x, НОД(x, y) определен также для отрицательных аргументов и не меняется, если мы изменяем знак аргументов. Он определен и тогда, когда один из аргументов равен нулю; такой аргумент обладает бесконечной таблицей делителей (и поэтому нам не следует пытаться строить эту таблицу!), но поскольку второй аргумент (= 0) обладает конечной таблицей делителей, таблица общих делителей является все же непустой и конечной. Итак, мы приходим к заключению, что НОД(x, y) определен для всякой пары (x, y), такой, что (x, y) = (0, 0). Далее, в силу симметрии понятия "общий" наибольший общий делитель является симметричной функцией своих двух аргументов. Еще одно небольшое умственное усилие позволит нам убедиться в том, что наиболь- ший общий делитель двух аргументов не изменяется, если мы заменяем один из этих аргументов их суммой или разностью. Объединив все эти результаты, мы можем записать: для (x, y) = (0, 0)
НОД(x, y) = НОД(y, x).
(а)
НОД(x, y) = НОД(−x, y).
(б)
НОД(x, y) = НОД(x + y, y) = НОД(x − y, y) и т. д.
(в)
НОД(x, y) = abs(x), если x = y.
(г)
Предположим для простоты рассуждений, что этими четырьмя свойствами исчерпываются наши познания о функции НОД. Достаточно ли их? Вы видите, что первые три отношения выражают наибольший общий делитель чисел x и y через НОД для другой пары, а последнее свойство выражает его непосредственно через x. И в этом уже просматриваются контуры алгоритма, который для начала обеспечивает истинность
P = (НОД(X, Y ) = НОД(x, y))

Э. Дейкстра. ”Дисциплина программирования”
37
(это легко достигается путем присваивания "x, y := X, Y "), после чего мы "утрамбовываем" пару значений (x, y) таким образом, чтобы в соответствии с (а), (б) или (в) отношение P оставалось инва- риантным. Если мы можем opгaнизовать этот процесс утрамбовки так, чтобы достигнуть состояния,
удовлетворяющего x = y, то, согласно (г), мы находим искомый ответ, взяв абсолютное значение x.
Поскольку наша конечная цель состоит в том, чтобы обеспечить при инвариантности P истин- ность x = y, мы могли бы испытать в качестве монотонно убывающей функции функцию t = abs(x − y).
Чтобы упростить наш анализ (всегда похвальная цель!), мы отмечаем, что если начальные зна- чения x и y неотрицательные, то ничего нельзя выиграть введением отрицательного значения: если присваивание x := E обеспечило бы x < 0, то присваивание x := −E никогда не привело бы к получе- нию большего конечного значения t (потому, что y ≥ 0). Поэтому мы усиливаем наше отношение P ,
которое должно сохраняться инвариантным:
P = (P 1 and P 2)
при
P 1 = (НОД(X, Y ) = НОД(x, y))
и
P 2 = (x ≥ 0 and y ≥ 0)
Это означает, что мы отказываемся от всякого использования операций x := −x и y := −y, т.е.
преобразований, допустимых по свойству (б). Нам остаются операции из (a): x, y := y, x из (в):
x := x + y y := y + x x := x − y y := y − x x := y − x y := x − y
Будем заниматься ими по очереди и начнем с рассмотрения x, y := y, x:
wp("x, y := y, x", abs(x − y) ≤ t
0
) = (abs(y − x) ≤ t
0
)
поэтому t
min
(x, y) = abs(y − x)
следовательно wdec("x, y := y, x", abs(x − y)) = (abs(y − x) ≤ abs(x − y) − 1) = F
И здесь — для тех, кто не поверил бы без формального вывода,—мы доказали (или, если угодно,
обнаружили) с помощью нашero исчисления, что преобразующая операция x, y := y, x не представляет интереса, так как она не может привести к желаемому эффективному уменьшению выбранной нами функции t.
Следующей испытывается операция x := x + y, и мы находим, снова применяя исчисление из предыдущих глав:
wp("x := x + y", abs(x − y) ≤ t
0
) = (abs(x) ≤ t
0
)
t min
(x, y) = abs(x) = x
(мы ограничиваемся состояниями, удовлетворяющими P )
wdec("x := x + y", abs(x − y)) = (t min
(x, y) ≤ t(x, y) − 1)
= (x ≤ abs(x − y) − 1)
= (x + 1 ≤ abs(x − y))
= (x + 1 ≤ x − y or x + 1 ≤ y − x)
Поскольку из P следует отрицание первого члена и к тому же P ⇒ wp("x := x+y", P ), то уравнение нашего предохранителя
(P and B
j
)
⇒ (wp(SL
j
, P ) and wdec(SL
j
, t))

38
Э. Дейкстра. ”Дисциплина программирования”
удовлетворяется последним членом, и мы нашли нашу первую, а также (из соображений симметрии)
нашу вторую охраняемую команду:
x + 1 ≤ y − x → x := x + y и
y + 1 ≤ x − y → y := y + x
Аналогично мы находим (формальные манипуляции предоставляются в качестве упражнения при- лежному читателю)
1
≤ y and 3 ∗ y ≤ 2 ∗ x − 1 → x := x − y и
1
≤ x and 3 ∗ x ≤ 2 ∗ y − 1 → y := y − x и
x + 1 ≤ y − x → x := y − x и
y + 1 ≤ x − y → y := x − y
Разобравшись в том, чего мы достигли, мы вынуждены прийти к досадному заключению, что спо- собом, намеченным в конце предыдущей главы, нам не удалось решить свою задачу: из P and non BB
не следует, что x = y. (Например, при (x, y) = (5, 7) значения всех предохранителей оказываются лож- ными.) Мораль сказанного, разумеется, в том, что наши шесть шагов не всегда обеспечивают такой путь из начального состояния в конечное состояние, при котором abs(x − y) монотонно уменьшается.
Поэтому нам нужно испытать другие возможности.
Для начала заметим, что не повредит несколько усилить условие P 2:
P 2 = (x > 0 and y > 0)
так как начальные значения x и y удовлетворяют такому условию, и, кроме того, нет никакого смысла в генерации равного нулю значения, поскольку это значение может возникнуть только при вычитании в состоянии, где x = y, т.е. когда уже достигнуто конечное состояние. Но это только малая модификация; основная модификация должна быть связана с введением новой функции t, и я предлагаю взять такую функцию t, которая только ограничена снизу в силу инвариантности P .
Очевидным примером является t = x + y
Мы выясняем, что для одновременного присваиваивания wdec("x, y := y, x", x + y) = F
и поэтому одновременное присваивание отвергается.
Мы находим для присваивания x := x + y wdec("x := x + y", x + y) = (y < 0)
Истинность этого выражения исключается истинностью инвариантного отношения P , а следователь- но, такое присваивание (наряду с присваиванием y := y + x) также отвергается.
Однако для следующего присваивания x := x − y мы находим wdec("x := x − y", x + y) = (y > 0)
т. е. условие, которое, логически следует из условия P ( усиленного мною ради этого).
Окрыленные надеждой, мы изучаем wp("x := x − y", P ) = (НОД(X, Y ) = НОД(x − y, y) and x − y > 0 and y > 0)
Крайние члены можно отбросить, потому что они следуют из P , и у нас остается средний член: итак,
мы находим x > y → x := x − y

Э. Дейкстра. ”Дисциплина программирования”
39
и y > х → y := y − x
И на этом мы могли бы прекратить исследование, так как, когда значения обоих предохранителей становятся ложными, выполняется желаемое нами отношение x = y. Если мы продолжим, то найдем третий и четвертый варианты:
x > y − x and y > x → x := y − x и
y > x − y and x > y → y := x − y но не ясно, что можно выиграть их включением.
Упражнения.
1. Исследуйте при том же P выбор t = max(x, y).
2. Исследуйте при том же P выбор t = x + 2 ∗ y.
3. Докажите, что при X > 0 и Y > 0 следующая программа, оперирующая над четырьмя пере- менными,
x, y, u, v := X, Y, Y, X;
do x > y → x, v := x − y, v + u
[] y > x → y, u := y − x, u + v
od;
печатать((x + y)/2); печатать((u + v)/2)
печатает наибольший общий делитель чисел Х и У, а следом за ним их наименьшее общее кратное.
(Конец упражнений.)
Наконец, если наш маленький алгоритм запускается при паре (X, Y ), которая не удовлетворяет предположению X > 0 and Y > 0, то произойдут неприятности: если (X, Y ) = (0, 0), то получится неправильный нулевой результат, а если один из аргументов отрицательный, то запуск приведет к бесконечной работе. Этого можно избежать, написав
if X > 0 and Y > 0 → x, y := X, Y ;
do x > y → x := x − y[] y > x → y := y − x od; печатать(x)
fi
Включив только один вариант в конструкцию выбора, мы явно выразили условия, при которых ожидается работа этой маленькой программы. В таком виде это хорошо защищенный и довольно самостоятельный фрагмент, обладающий тем приятным свойством, что попытка запуска вне его области определения приведет к немедленному отказу.

40
Э. Дейкстра. ”Дисциплина программирования”
8 ФОРМАЛЬНОЕ РАССМОТРЕНИЕ НЕСКОЛЬКИХ НЕБОЛЬШИХ ПРИМЕРОВ
В этой главе я проведу формальное построение нескольких небольших программ для решения простых задач. Не следует понимать эту главу как предложение строить программы только так и не иначе: такое предложение было бы довольно смехотворным. Я полагаю, что многим из моих читателей знакомо большинство примеров, а если нет, они, вероятно, не задумываясь смогут написать любую из этих программ.
Следовательно, построение программ проводится здесь совсем по другим причинам. Во-первых,
это ближе познакомит нас с формализмом, развитым в предыдущих главах. Во-вторых, убедит нас в том, что по крайней мере в принципе, формализм способен сделать ясным и совершенно строгим то, что часто объясняется при помощи энергичной жестикуляции. В-третьих, многие из нас настоль- ко хорошо знают эти программы, что уже забыли, каким образом давным-давно мы убедились в их правильности: в этом отношении настоящая глава напоминает начальные уроки планиметрии,
которые по традиции посвящаются доказательству очевидного. В-четвертых, мы можем случайно обнаружить, к своему удивлению, что маленькая знакомая задачка не такая уже знакомая. Нако- нец, процесс построения программ может пролить свет на осуществимость, трудности и возможности автоматического составления программ или использования машины в процессе программирования.
Это может оказаться важным, даже если автоматическое составление программ не вызывает у нас ни малейшего интереса, потому что может помочь нам лучше оценить ту роль, которую могут или должны играть наши изобретательские способности.
В моих примерах я буду формулировать требования задачи в формe "для фиксированных x, y,
. . . ", что является сокращенной записью формы "для любых значений x
0
, y
0
, ... постусловие вида x = x
0
and y = y
0
and . . . должно вызывать предусловие, из которого следует, что x = x
0
and y =
y
0
and . . .". Эта связь между постусловием и предусловием будет гарантирована тем, что мы будем относиться к таким величинам как к "временным константам"; они не будут встречаться в левых частях операторов присваивания.
Первый пример
Для фиксированных x и y обеспечить истинность отношения R(m).
(m = x or m = y) and m ≥ x and m ≥ y
Для любых значений x и y отношение m = x может стать истинным только в результате присваи- вания m := x; следовательно, истинность (m = x or m = y) обеспечивается только выполнением либо m := x, либо m := y. В виде блок-схемы:
P icture 8.1
Все дело в том, что на входе нужно сделать правильный выбор, который обеспечит истинность
R(m) после завершения вычислений. Для этого мы "проталкиваем постусловие через альтернативы":
P icture 8.2
и мы получили предохранители! Так как
R(x) = ((x = x or x = y) and x ≥ x and x ≥ y) = (x ≥ y)
и
R(y) = ((y = x or y = y) and y ≥ x and y ≥ y) = (y ≥ x)
мы приходим к нашему решению: