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

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

27
где фигурные скобки "
{" и "}" следует читать так: "conpовождается любым числом (быть может,
нулем) экземпляров содержимого скобок".
(Другой вариант синтаксиса охраняемой команды может выглядеть так:
список операторов ::= оператор
{; оператор }
охраняемая команда ::= логическое выражение
→
список операторов
Однако по причинам, которые не должны нас теперь интересовать, я предпочитаю синтаксис, в котором вводится понятие охраняющего заголовка).
В этом сочетании логическое выражение, предшествующее стрелке, называется "предохраните- лем". Идея состоит в том, что следующий за стрелкой список операторов будет выполняться лишь при том условии, что обеспечена начальная истинность значения соответствующего предохранителя.
Предохранитель позволяет нам избежать выполнения списка операторов при тех первоначальных об- стоятельствах, когда это полнение оказалось бы нежелательным или (если употребляются частично определенные операции) невозможным.
Истинность значения предохранителя является необходимым предварительным условием для выполнения охраняемой команды как целого; это условие, разумеется, не является достаточным,
поскольку тем или иным способом — с двумя такими способами мы встретимся — до него еще долж- на дойти потенциальная "очередь". Именно поэтому охраняемая команда не рассматривается как оператор: оператор безоговорочно выполняется, когда наступает его очередь, а охраняемая коман- да может использоваться в качестве строительного блока для оператора. Если говорить точнее, мы предложим два различных способа составления оператора из набора охраняемых команд.
После некоторого осмысливания рассмотрение набора охраняемых команд представляется впол- не естественным. Предположим, что нам требуется построить конструкцию, такую, чтобы при усло- вии, что начальное состояние удовлетворяет Q, конечное состояние удовлетворяло R. Предположим далее, что нам не удается найти единый список операторов, который выполнял бы эту работу в лю- бых случаях. (Если бы такой список операторов существовал, то мы именно его бы и использовали и не возникло бы потребности в охраняемых командах.) Однако нам может удасться найти несколько списков операторов, каждый из которых будет выполнять нужную работу для некoero подмножества возможных начальных состояний. К каждому из этих списков операторов мы можем присоединить в качестве предохранителя логическое выражение, характеризующее то подмножество, для которого этот список подходит, и если у нас имеется вполне достаточный набор предохранителей, такой, что из истинности Q всегда логически следует истинность значения хотя бы одного предохранителя, то для каждого начального состояния, удовлетворяющего Q, мы располагаем конструкцией, которая переведет систему в состояние, удовлетворяющее условию R, причем этой конструкцией служит одна из охраняемых команд, чей предохранитель имел начальное значение "истина". Чтобы выразить это,
определим сначала набор охраняемых команд ::= охраняемая команда
{[] охраняемая команда }
где символ "[]" выступает в роли разделителя вариантов, в остальном не упорядоченных. Один из спо- собов формирования оператора из набора охраняемых команд состоит в том, чтобы включить такой набор в пару скобок "if . . . fi", при этом наш синтаксис для синтаксической категории, именуемой "оператор", пополняется следующей формой:
оператор ::= if набор охраняемых команд fi
Таким образом, мы получаем возможность объединить несколько охраняемых команд в новую кон- струкцию. Мы можем представить себе работу, которая произойдет после запуска этой конструкции,
следующим образом. Выбирается одна из охраняемых команд, чей предохранитель является истин- ным, и запускается ее список операторов.
Прежде чем мы перейдем к изложению формального описания семантики нашей новой конструк- ции, уместно сделать три замечания.
1. Предполагается, что все предохранители определены; если это не так, т. е. вычисление какого-то предохранителя может прииести к работе без правильного завершения, то допускается, что и вся конструкция не сможет правильно завершить свою работу.
2. Вообще говоря, наша конструкция приведет к недетерминированности при тех начальных со- стояниях, для которых истинны значения более чем одного предохранителя, поскольку остается

28
Э. Дейкстра. ”Дисциплина программирования”
неопределенным, какой из соответствующих списков операторов будет тогда выбираться для запуска. Hикакой недетерминированности не возникает, если все предохранители попарно ис- ключают друг друга.
3. Если начальное состояние таково, что ни один из предохранителей не является истиной, то мы встречаемся с начальным состоянием, для которого не подходит ни один из вариантов, а следовательно, и вся конструкция в целом. Запуск при таком начальном состоянии приведет к отказу.
Замечание. Если мы допускаем также и пустой набор охраняемых команд, то оператор "if-fi"
семантически эквивалентен нашему прежнему оператору "отказать". (Конец замечания.)
(В следующем формальном определении слабейшего предусловия для конструкции if-fi мы огра- ничимся случаем, когда все предохранители являются полностью определенными функциями. Если это не так, то нужно переписать выражение с использованием символа cand при дополнительном требовании, чтобы начальное состояние принадлежало области определения всех предохранителей.)
Обозначим через "IF" оператор 1
ifB
1
→ SL
1
[]B
2
→ SL
2
[] . . . []B
n
→ SL
n
fi
Тогда для любого постусловия R
wp(IF, R) = (∃j : 1 ≤ j ≤ n : B
j
) and (∀j : 1 ≤ j ≤ n : B
j
⇒ wp(SL
j
, R))
Эту формулу следует читать так: wp(IF, R) является истиной для каждой такой точки в простран- стве состояний, где хотя бы одно значение j из отрезка 1 ≤ j ≤ n, такое, что B
j является истиной, и где, кроме того, для всех j из отрезка 1 ≤ j ≤ n, таких, что B
j
— истина, значение wp(SL
j
, R) также является истиной. Используя символ ". . . ", как мы уже делали при описании самого оператора IF,
мы можем предложить иную форму определения:
wp(IF, R) =(B
1
or B
2
or . . . or B
n
)and
(B
1
⇒ wp(SL
1
, R))and
(B
2
⇒ wp(SL
2
, R)) and . . . and
(B
n
⇒ wp(SL
n
, R))
Понимание этих формул не представляет особого труда. Требованием, чтобы значение хотя бы одного предохранителя являлось истиной, отражается факт отказа в случае, когда значения для всех предохранителей ложны. Кроме того, мы требуем для каждого начального состояния, удовлетворя- ющего wp(IF, R), чтобы выполнялось B
j
⇒ wp(SL
j
, R) для всех j. Для тех значений j, при которых
B
j
— ложь, это следование истинно независимо от значения wp(SL
j
, R), т. е. для таких значений j,
разумеется, безразлично, что будет делать SL
j
. При нашей реализации это учитывается в том, что для запуска не берется SL
j с ложным начальным значением предохранителя B
j
. При тех значениях j, для которых B
j
— истина, данное следование может быть истиной только в том случае, когда wp(SL
j
, R)
также является истиной. Поскольку наше формальное определение требует истинности следования при всех значениях j, то реализация на самом деле имеет свободу выбора, когда более чем один предо- хранитель является истиной. Конструкция if-fi представляет собой только один из двух возможных способов построения оператора из набора охраняемых команд. В конструкции if-fi состояние, при котором все предохранители имеют ложные значения, ведет к отказу. В нашей второй форме мы разрешаем, чтобы состояние, при котором нет ни одного предохранителя с истинным значением,
приводило к правильному завершению; поскольку в этой ситуации не запускается никакой список операторов, вполне естественно, что при этом возникает семантическая эквивалентность с пустым оператором. Однако это разрешение на правильное завершение, когда нет ни одного предохранителя с истинным значением, дополняется тем, что работе не разрешается завершаться, пока хотя бы один предохранитель является истиной. Итак, после запуска проверяются все предохранители. Если нет ни одного истинного значения предохранителя, то работа завершается; если же имеются предохра- нители с истинными значениями, то один из соответствующих списков операторов запускается, а после его завершения реализация снова начинает общую проверку всех предохранителей. Эта вторая конструкция обозначается путем заключения списка охраняемых команд в пару скобок "do .. od".
Формальное определение слабейшего предусловия для конструкции do-od является более слож- ным, чем для конструкции if-fi; дело в том, что первое выражается через второе. Мы сначала приведем это формальное определение, а затем объясним его. Обозначим через "DO" оператор
doB
1
→ SL
1
[]B
2
→ SL
2
[] . . . []B
n
→ SL
n
od
1 SL- аббревиатура для Statement List — список операторов. —Прим. перев.

Э. Дейкстра. ”Дисциплина программирования”
29
и через "IF" оператор, получаемый путем заключения того же набора охраняемых команд в пару скобок "if ... fi". Если условия H
k
(R) задаются в виде
H
0
(R) = R and non(∃j : 1 ≤ j ≤ n : B
j
)
и при k > 0
H
k
(R) = wp(IF, H
k−1
(R)) or H
0
(R)
то wp(DO, R) = (∃k : k ≥ 0 : H
k
(R))
Здесь интуитивно мы понимаем H
k
(R) следующим образом: это слабейшее предусловие, такое,
что конструкция do-od завершит свою работу после не более чем k выборок охраняемых команд,
причем система останется в конечном состоянии, удовлетворяющем постусловию R.
При k = 0 требуется, чтобы конструкция do-od завершила работу, не производя выборки какой- либо охраняемой команды, т. е. не допускается существования какого-либо предохранителя с истин- ным значением, что и выражено вторым логическим сомножителем. При этом начальная истинность
R очевидным образом является необходимым условием для конечной истинности R, что и выражено первым логическим сомножителем.
При k > 0 нам нужно различать два случая: либо ни один из предохранителей не имеет истин- ного значения, но тогда должно выполняться условие R, и это приводит нас ко второму логическому слагаемому; либо хотя бы один предохранитель является истиной, и тогда события развиваются так,
как при однократном запуске оператора "IF" (в начальном состоянии, которое не может привести к немедленному отказу вследствие отсутствия истинных значений предохранителей). Однако после та- кого выполнения, при котором производилась выборка одной охраняемой команды, нам необходима гарантия попадания в состояние, такое, чтобы потребовалось не более чем (k−1) дальнейших выборок для достижения завершения работы в конечном состоянии, удовлетворяющем R. В соответствии с нашим определением, таким постусловием для этого оператора "IF" служит H
k−1
(R).
Согласно последней строке, определяющей wp(DO, R), должно существовать такое значение k,
чтобы потребовалось не более чем k выборок для обеспечения завершения работы в конечном состоя- нии, удовлетворяющем постусловию R.
Замечание. Если мы допускаем также и пустой набор oxраняемых команд, то в силу сказанного оператор "do od" семантически эквивалентен нашему прежнему оператору "пропустить". (Конец
замечания.)

30
Э. Дейкстра. ”Дисциплина программирования”
5 ДВЕ ТЕОРЕМЫ
В этой главе мы выводим две теоремы об операторах, которые строятся из наборов охраняемых команд. Первая теорема касается конструкции выбора if-fi, а вторая — конструкции повторения do-od. В этом главе мы будем рассматривать конструкции, выводимые из набора охраняемых команд
B
1
→ SL
1
[]B
2
→ SL
2
[] . . . []B
n
→ SL
n
Будем обозначать через "IF" и "DO" операторы, получаемые заключением этого набора охраня- емых команд в пары скобок "if ... fi" и "do ... od" соответственно. Мы будем также использовать сокращение
BB = (∃j : 1 ≤ j ≤ n : B
j
)
Теорема. (Основная теорема для конструкции выбора)
Используя введенные только что обозначения, мы можем сформулировать основную теорему для конструкции выбора:
Пусть конструкция выбора IF и пара предикатов Q и R таковы, что
Q ⇒ BB
(1)
и
(
∀j : 1 ≤ j ≤ n : (Q and B
j
)
⇒ wp(SL
j
, R))
(2)
одновременно справедливы для всех состояний. Тогда
Q ⇒ wp(IF, R)
(3)
справедливо также для всех состояний. Поскольку, в силу определения,
wp(IF, R) = BB and (∀j : 1 ≤ j ≤ n : B
j
⇒ wp(SL
j
, R))
и, согласно (1), из Q логически следует первый член правой части, то отношение (3) доказывается,
если на основании (2) мы можем сделать вывод, что
Q ⇒ (∀j : 1 ≤ j ≤ n : B
j
⇒ wp(SL
j
, R))
(4)
справедливо для всех состояний. Для любого состояния, при котором Q является ложью, отношение
(4) истинно в силу определения логического следования. Для любого состояния, при котором Q явля- ется истиной, и для любого значения j мы можем различать два случая: либо B
j является ложью, но тогда B
j
⇒ wp(SL
j
, R) является истиной в силу определения следования, либо B
j является истиной,
но тогда, согласно (2), wp(SL
j
, R) является истиной, а следовательно, B
j
⇒ wp(SL
j
, R) тоже является истиной. В результате мы доказали отношение (4), а следовательно, и (3).
Замечание. В частном случае бинарного выбора (n = 2) и при B
2
= non B
1
мы имеем BB = T , и слабейшее предусловие преобразуется так:
(B
1
⇒ wp(SL
1
, R)) and (non B
1
⇒ wp(SL
2
, R)) =
(non B
1
or wp(SL
1
, R)) and (B
1
or wp(SL
2
, R)) =
(B
1
and wp(SL
1
, R)) or (non B
1
and wp(SL
2
, R))
(5)
Последнее преобразование возможно потому, что из четырех перекрестных произведений член B
1
and non B
1
= F может быть отброшен, а член wp(SL
1
, R) and wp(SL
2
, R) тоже может быть отброшен по следующей причине: в любом состоянии, где он истинен, обязательно является истиной какой-то один из двух членов формулы (5), и поэтому его самого можно исключить из дизъюнкции. Формула
(5) имеет прямое отношение к предложенному Хоаром способу описания семантики конструкции if-
then-else из языка АЛГОЛ 60. Поскольку здесь BB = T логически следует из чего угодно, мы можем вывести (3) при более слабом предположении:
((Q and B
1
)
⇒ wp(SL
1
, R)) and ((Q and non B
1
)
⇒ wp(SL
2
, R))
(Конец замечания.)

Э. Дейкстра. ”Дисциплина программирования”
31
Теоремa для конструкции выбора представляет особую важность в случае, когда пара предикатов
Q и R может быть записана в виде
R = P
Q = P and BB
В этом случае предпосылка (1) выполняется автоматически, а поскольку (BB and B
j
) = B
j
, предпо- сылка (2) сводится к виду
(
∀j : 1 ≤ j ≤ n : (P and B
j
)
⇒ wp(SL
j
, P ))
(6)
из чего мы можем вывести, согласно (3),
(P and BB) ⇒ wp(IF, P )
для всех состояний
(7)
Это отношение послужит предпосылкой для нашей следующей теоремы.
Теорема. (Основная теорема для конструкции повторениения.)
Пусть набор охраняемых команд с построенной для него конструкцией выбора IF и предикат P
таковы, что
(P and BB) ⇒ wp(IF, P )
(7)
справедливо для всех состояний. Тогда для соответствующей конструкции повторения DO можно вывести, что
(P and wp(DO, T )) ⇒ wp(DO, P and non BB)
(8)
для всех состояний.
Эту теорему, которая известна также под названием "основная теорема инвариантности для ци- клов", на интуитивном уровне не трудно понять. Предпосылка (7) говорит нам, что если предикат
P первоначально истинен и одна из охраняемых команд выбирается для выполнения, то после ее выполнения P сохранит свою истинность. Иначе говоря, предохранители гарантируют, что выпол- нение соответствующих списков операторов не нарушит истинности P , если начальное значение P
было истинным. Следовательно, вне зависимости от того, как часто производится выборка охра- няемой команды из имеющегося набора, предикат P будет справедлив при любой новой проверке предохранителей. После завершения всей конструкции повторения, когда ни один из предохраните- лей не является истиной, мы тем самым закончим работу в конечном состоянии, удовлетворяющем
P and non BB. Вопрос в том, завершится ли работа правильно. Да, если условие wp(DO, T ) справед- ливо и вначале; поскольку любое состояние удовлетворяет T , то wp(DO, T ) по определению является слабейшим предусловием для начального состояния, такого, что запуск оператора DO приведет к правильно завершаемой работе.
Формальное доказательство основной теоремы для конструкции повторения основывается на формальном описании семантики этой конструкции (см. предыдущую главу), из которого мы выво- дим
H
0
(T ) = non BB
(9)
при k > 0 : H
k
(T ) = wp(IF, H
k−1
(T )) or non BB
(10)
H
0
(P and non BB) = P and non BB
(11)
при k > 0 : H
k
(P and non BB) = wp(IF, H
k−1
(P and non BB)) or P and non BB
(12)
Начнем с того, что докажем посредством математической индукции, что предпосылка (7) гаран- тирует справедливость
(P and H
k
(T )) ⇒ H
k
(P and non BB)
(13)
для всех состояний.
В силу отношений (9) и (11) отношение (13) справедливо при k = 0. Мы покажем, что отношение
(13) может быть доказано при k = K (K > 0) на основании предположения, что (13) справедливо при k = K − 1.
P and H
k
(T ) = P and wp(IF, H
K−1
T )) or P and non BB
= P and BB and wp(IF, H
K−1
(T )) or P and non BB
⇒ wp(IF, P )andwp(IF, H
K−1
(T )) or P and non BB
= wp(IF, P )andH
K−1
(T ))orP andnonBB
⇒ wp(IF, H
K−1
(P andnonBB))orP andnonBB
= H
K
(P andnonBB)

32
Э. Дейкстра. ”Дисциплина программирования”
Равенство в первой строке следует из (10), равенство во второй строке следует из того, что всегда wp(IF, R) ⇒ BB, логическое следование в третьей строке вытекает из (7), равенство в четвертой строке основывается на свойстве 3 преобразователей предикатов, следование в пятой строке вытекает из свойства 2 преобразователей предикатов и из индуктивного предположения (13) для k = K − 1,
и последняя строка следует из (12). Итак, мы доказали (13) для k = K, а следовательно, для всех значений k ≥ 0.
Наконец, для любой точки в пространстве состояний мы имеем, в силу (13),
P and wp(DO, T ) = (∃k : k ≥ 0 : P andH
k
(T ))
⇒ (∃k : k ≥ 0 : H
k
(P and non BB))
= wp(DO, P and non BB)
и тем самым доказана основная теорема (8) для конструкции повторения. Ценность основной теоре- мы для конструкции повторения основывается на том, что ни в предпосылке, ни в ее следствии не упоминается фактическое число выборок охраняемой команды. Поэтому она применима даже в тех случаях, когда это число не определяется начальным состоянием.

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