Э. Дейкстра Дисциплина программирования. Предисловие редактора перевода
 Скачать 1.14 Mb.
|
|
46 Э. Дейкстра. ”Дисциплина программирования” а затем будем увеличивать dd, пока его значение не станет достаточно большим и таким, что r < dd. Получим следующую программу: if a ≥ 0 and d > 0 → r, dd := a, d; do r ≥ dd → dd := dd ∗ 3 od; do dd = d → dd := dd/3; do r ≥ dd → r := r − dd od od fi Упражнение Измените приведенную выше программу таким образом, чтобы она вычисляла также и частное, и дайте формальное доказательство правильности вашей программы, Это доказательство должно на- глядно показывать, что всякий раз, когда вычисляется dd/3, имеет место 3|dd. (Конец упражнения.) Для приведенной выше программы характерна довольно распространенная особенность. На внешнем уровне две конструкции повторения расположень подряд; когда две или больше конструк- ций повторения на одном и том же уровне следуют друг за другом, охраняемые команды более поздних конструкций оказываются, как правило, более сложными, чем команды предыдущих конструкций. (Это явление известно как "закон Дейкстры", который, однако, не всегда выполняется.) Причина такой тенденции ясна: каждая конструкция повторения добавляет свое "and non BB" к отношению, которое она сохраняет инвариантным, и это дополнительное отношение следующая конструкция так- же должна сохранять инвариантным. Если бы не внутренний цикл, второй цикл был бы в точности противоположен первому; и функция дополнительного оператора do r ≥ dd → r := r − dd od именно в том и состоит, чтобы восстанавливать возможно нарушенное отношение r < dd, достигаемое при выполнении первого цикла. Четвертый пример Для фиксированных Q1, Q2, Q3 и Q4 требуется обеспечить истинность R, причем R задается как R1 and R2, где R1: последовательность значений (q1, q2, q3, q4) есть некоторая перестановка значений (Ql, Q2, Q3, Q4) R2: q1 ≤q2 ≤q3 ≤q4 Если мы возьмем R1 в качестве сохраняемого инвариантным отношения P , получим такое воз- можное решение: q1, q2, q3, q4 := Q1, Q2, Q3, Q4; do q1 > q2 → q1, q2 := q2, q1 [] q2 > q3 → q2, q3 := q3, q2 [] q3 > q4 → q3, q4 := q4, q3 od Очевидно, что после первого присваивания P становится истинным и ни одна из охраняемых команд не нарушает его истинности. По завершении программы мы имеем non BB, а это есть отношение R2. В том, что программа действительно придет к завершению, каждый из нас убеждается по-разному в зависимости от своей профессии: математик мог бы заметить, что число перестановок убывает, исследователь операций будет интерпретировать это как максимизацию q1 + 2 ∗ q2 + 3 ∗ q3 + 4 ∗ q4, а я — как физик — сразу "вижу", что центр тяжести смещается в одном направлении (вправо, если быть точным). Программа примечательна в том смысле, что, какие бы предохранители мы ни выбрали, никогда не возникнет опасности нарушения истинности P: предохранители, используемые в нашем примере, являются чистым следствием необходимости завершения программы. Замечание. Заметьте, что мы могли бы добавить также и другие варианты, такие, как q1 > q3 → q1, q3 := q3, q1 причем их нельзя использовать для замены одного из трех, перечисленных в программе. (Конец замечания.) Это хороший пример того, какого рода ясности можно достичь при нашей недетерминирован- ности; излишне говорить однако, что я не рекомендую сортировать большое количество значений аналогичным способом. Э. Дейкстра. ”Дисциплина программирования” 47 Пятый пример Нам требуется составить программу аппроксимации квадратного корня; более точно: для фик- сированного n (n > 0) программа должна обеспечить истинность R : a 2 ≤ n and (a + 1) 2 > n Чтобы ослабить это отношение, можно, например, отбросить один из логических сомножителей, скажем последний, и сосредоточиться на P : a 2 ≤ n Очевидно, что это отношение верно при a = 0, поэтому выбор начального значения не должен нас беспокоить. Мы видим, что если второй член не является истинным, то это вызывается слишком маленьким значением a, поэтому мы могли бы обратиться к оператору "a := a + 1". Формально мы получаем wp("a := a + 1", P ) = ((a + 1) 2 ≤ n) Используя это условие в качестве (единственного!) предохранителя, мы получаем (P andnon BB) = R и приходим к следующей программе: if n ≥ 0 → a := 0 {P стало истинным}; do (a + 1) 2 ≤ n → a := a + 1 {P осталось истинным} od {R стало истинным } fi {R стало истинным } При составлении программы мы исходили из предположения, что онa завершится, и это действи- тельно так, поскольку корень из неотрицательного числа есть монотонно возрастающая функция: в качестве t мы можем взять функцию n − a 2 Эта программа довольно очевидна, к тому же она и не очень эффективна: при больших значениях n она будет работать довольно долго. Другой способ обобщения R — это введение другой переменной (скажем, b — и снова в ограниченном интервале изменения), которая заменит часть R, например, P : a 2 ≤ n and b 2 > n and 0 ≤ a < b Благодаря такому выбору P обладает тем приятным свойством, что (P and (a + 1 = b)) ⇒ R Таким образом, мы приходим к программе, представленной в такой форме (здесь и далее кон- струкция if n ≥0 →. . . fi опускается): a, b := 0, n + 1 {P стало истинным}; do a + 1 = b → уменьшить b − a при инвариантности P od {R стало истинным} Пусть d будет величиной, на которую уменьшается разность b − a при каждом выполнении охра- няемой команды. Разность может уменьшаться либо за счет уменьшения b, либо за счет увеличения a, либо за счет и того и другого. Не теряя общности, мы можем ограничиться рассмотрением таких шагов, когда изменяется либо a, либо b, но не a и b одновременно: если a слишком мало и b слишком велико и на одном шаге только уменьшается b, тогда на следующем шаге можно увеличить a. Эти соображения приводят нас к программе в следующей форме: a, b := 0, n + 1 {P стало истинным}; do a + 1 = b → d := . . . {d имеет соответствующее значение и P по − прежнему выполняется}; if . . . → a := a + d {P осталось истинным} [] . . . → b := b − d {P осталось истинным} fi {P стало истинным} od {R стало истинным} Теперь wp("a := a + d", P ) = ((a + d) 2 ≤ n and b 2 > n) 48 Э. Дейкстра. ”Дисциплина программирования” Поскольку истинность второго члена следует из истинности P , мы можем использовать первый член в качестве нашего первого предохранителя; аналогично выводится второй предохранитель, и мы получаем очередную форму нашей программы: a, b := 0, n + 1; do a + 1 = b → d := . . . ; if(a + d) 2 ≤ n → a := a + d [] (b − d) 2 > n → b := b − d fi {P осталось истинным} od {R стало истинным} Нам остается еще соответствующим образом выбрать d. Поскольку мы взяли b − a (на самом деле, b − а − 1) в качестве нашей функции t, эффективное убывание должно быть таким, чтобы d удовлетворяло условию d > 0. Кроме того, последующая конструкция выбора не должна приводить к отказу, т. е. по крайней мере один из предохранителей должен быть истинным. Это значит, что из отрицания одного, (a + d) 2 > n, должен следовать другой, (b − d) 2 > n; это гарантируется, если a + d ≤ b − d или 2 ∗ d ≤ b − a Наряду с нижней границей мы установили также и верхнюю границу для d. Мы могли бы взять d = 1, но чем больше d, тем быстрее работает программа, поэтому мы предлагаем a, b := 0, n + 1; do a + 1 = b → d := (b − a) ÷ 2; if (a + d) 2 ≤ n → a := a + d [] (b − d) 2 > n → b := b − d fi od где n ÷ 2 есть n/2, если 2|n и (n − 1)/2, если 2|(n − 1). Использование действия ÷ побуждает нас разобратся в том, что произойдет, если мы навяжем себе ограничение на b − a, полагая, что b − a четно при каждом вычислении d. Вводя c = (b − a) и исключая b, мы получаем инвариантное отношение P : a 2 ≤ n and (a + c) 2 > n and (∃i : i ≥ 0 : c = 2 i ) и программу (в которой c играет роль d) a, c := 0, 1; do c 2 ≤ n → c := 2 ∗ c od; do c = 1 → c := c/2; if (a + c) 2 ≤ n → a := a + c [] (a − c) 2 > n → пропустить fi od Замечание. Эта программа очень похожа на последнюю программу для третьего примера, где вычислялся остаток в предположении, что мы имеем право умножать и делить на 3. В приведенной выше программе можно было бы заменить конструкцию выбора на dо (a + c) 2 ≤ n → a := a + c od Если условие, которому должен удовлетворять остаток, 0 ≤ r < d, записать как r < d and (r + d) ≥ d, сходство станет еще более отчетливым. (Конец замечания.) Понимая, что так можно окончательно "замучить" этот маленький приимер, я бы хотел тем не менее предложить последний вариант преобразования программы. Мы написали программу, исходя из предположения, что операция возведения числа в квадрат входит в состав имеющихся операций; но предположим, что это не так и что единственные операции типа умножения, имеющиеся в нашем Э. Дейкстра. ”Дисциплина программирования” 49 распоряжении,— это умножение и деление на (малые) степени 2. Тогда наша последняя программа оказывается не такой уж хорошей, т. е. она нехороша, если мы предполагаем, что значения перемен- ных, с которыми непосредственно оперирует машина, отождествлены со значениями переменных a и c, как это было бы при "абстрактных" вычислениях. Другими словами, мы можем рассматривать a и c как абстрактные переменные, чьи значения представляются (в соответствии с соглашением, предусматривающим более сложные условия, чем просто тождественность) значениями других пере- менных, с которыми в действительностм оперирует машина при выполнении программы. Мы можем позволить машине работать не непосредственно с a и c, а с р, q, r, такими, что p = a ∗ c q = c 2 r = n − a 2 Мы видим, что это — преобразование координат, и каждой траектории в нашем (a, c)-пространстве соответствует траектория в нашем (p, q, r)-пространстве. Обратное не всегда верно, так как значения p, q и r не независимы: в терминах p, q и r мы получаем избыточность и, следовательно, потенциаль- ную возможность, пожертвовав некоторым объемом памяти, не только выиграть время вычислений, но даже избавиться от необходимости возводить в квадрат! (Совершенно ясно, что преследовалась именно эта цель, когда строилось преобразование, переводящее точку в (a, c)-пространстве в точку в (р, q, r)-пространстве.) Теперь мы можем попытаться перевести все булевы выражения и перемещения в (a, c)-пространстве в соответствующие булевы выражения и перемещения в (p, q, r) -пространстве. Если бы нам удалось сделать это в терминах допустимых операций, наша задача была бы успешно решена. Предлагаемое преобразование и в самом деле отвечает нашим требованиям, и результатом его является следующая программа (переменная h была введена для очень локальной оптимизации): p, q, r := 0, 1, n; do q ≤ n → q := q ∗ 4 od; do q = 1 → q := q/4; h := p + q; p := p/2 {h = 2 ∗ p + q} if r ≥ h → p, r := p + q, r − h [] r < h → пропустить fi od { p имеет значение, требуемое для a } Этот пятый пример был включен благодаря истории его создания (правда, несколько приукра- шенной). Когда младшей из двух наших собак было всего несколько месяцев, я однажды вечером пошел погулять с ними обеими. Назавтра мне предстояло читать лекции студентам, которые всего лишь несколько недель назад начали знакомиться с программированием, и мне нужна была простая задача, чтобы на ее примере я мог "массировать" решения. В течение часовой прогулки я продумал первую, третью и четвертую программы, правда, правильно ввести h в последней программе я смог только при помощи карандаша и бумаги, когда вернулся домой. Ко второй программе, той, которая оперирует с a и b и которая была здесь представлена как переходная ступень к нашему третьему решению, я пришел лишь несколько недель спустя — и она была тогда в гораздо менее элегантной форме, чем представлена здесь. Вторая причина для ее включения в число представленных программ — это соотношение между третьей программами: по отношению к четвертой программе третья пред- ставляет собой наш первый пример так называемой "абстракции представления". Шестой пример Для фиксированных X (X > 1) и Y (Y ≥ 0) программа должна обеспечить истинность отношения R : z = X Y при очевидном предположении, что операция возведения в степень не входит в набор доступных операций. Эта задача может быть решена при помощи "абстрактной переменной", скажем h; при решении задачи мы будем пользоваться циклом, для которого инвариантным является отношение P : h ∗ z = X Y и наша (в равной степени "абстрактная") программа могла бы выглядеть так: h, z := X Y , 1 {P стало истинным}; do h = 1 → сжимать h при инвариантности P od { R стало истинным } 50 Э. Дейкстра. ”Дисциплина программирования” Последнее заключение справедливо, поскольку (P and h = 1) ⇒ R. Приведенная выше програм- ма придет к завершению, если после конечного числа применений операции "сжимания" h станет равным 1. Проблема, конечно, в том, что мы не можем представить значение h значением конкретной переменной, с которым непосредственно оперирует машина; если бы мы могли так сделать, мы могли бы сразу присвоить z значение X Y , не затрудняя себя введением h. Фокус в том, что для представле- ния текущего значения h мы можем ввести две — на этом уровне конкретные — переменные, скажем x и y, и наше первое присваивание предлагает в качестве соглашения об этом представлении h = x y Тогда условие "h = 1" переходит в условие "y = 0", и наша следующая задача состоит в том, чтобы подыскать выполнимую операцию "сжимания". Поскольку при этой операции произведение h ∗ z должно оставаться инвариантным, мы должны делить h на ту же величину, на которую умножается z. Исходя из представления h, наиболее естественным кандидатом на эту величину можно считать текущее значение x. Без дальнейших затруднений мы приходим к такому виду нашей абстрактной программы: x, y, z := X, Y, 1 {P стало истинным}; do y = 0 → y, z := y − 1, z ∗ x {P осталось истинным} od {R стало истинным} Глядя на эту программу, мы понимаем, что число выполнений цикла равно первоначальному значению Y , и можем задать себе вопрос, нельзя ли ускорить программу. Ясно, что задачей охра- няемой команды является сведение y к нулю; не изменяя значения h, мы можем проверить, нельзя ли изменить представление этого значения в надежде уменьшить значение y. Попытаемся восполь- зоваться тем фактом, что конкретное представление значения h, заданное как x y , вовсе не является однозначным. Если y четно, мы можем разделить y на 2 и возвести x в квадрат, при этом значение h совсем не изменится. Непосредственно перед операцией сжимания мы вставляем преобразование, приводящее к наиболее привлекательному преобразованию h и получаем следующую программу: x, y, z := X, Y, 1; do y = 0 → do 2 | y → x, у := x ∗ x, y/2 od; y, z := y − 1, z ∗ x od {R стало истинным } Существует только одна величина, которую можно бесконечно делить пополам и она не станет нечетной, эта величина — нуль; иначе говоря, внешний предохранитель гарантирует нам, что вну- тренний цикл придет к завершению. Я включил этот пример по разным причинам. Меня поразило открытие, что если просто вставить в программу что-то, что на абстрактном уровне действует как пустой оператор, можно так изменить алгоритм, что число операций, которое раньше было пропорционально Y , станет пропорционально только log(Y ). Это открытие было прямым следствием того, что я заставил себя думать в терминах отдельной абстрактной переменной. Программа возведения в степень, которую я знал, была следую- щей: x, y, z := X, Y, 1; do y <> 0 → if non 2| y → y, z := y − 1, z ∗ x [] 2|y → пропустить fi; x, y := x ∗ x, y/2 od Эта последняя программа очень хорошо известна, многие из нас пришли к ней независимо друг от друга. Поскольку последнее возведение x в квадрат, когда y стал равным нулю, уже излишне, на эту программу часто ссылались как на пример, подтвеждающий необходимость иметь то, что мы назвали бы "промежуточнными выходами". Принимая во внимание нашу программу, я прихожу к заключению, что этот довод слаб. Седьмой пример Для фиксированного значения n (n ≥ 0) задана функция f (i) для 0 ≤ i < n. Присвоить булевой переменной "всешесть" такое значение, чтобы в конечном результате стало справедливым R : всешесть = (∀i : 0 ≤ i < n : f (i) = 6) Э. Дейкстра. ”Дисциплина программирования” 51 (Этот пример обнаруживает некоторое сходство со вторым примером данной главы. Заметим, однако, что в этом примере допускается равенство n нулю. В таком случае интервал возможных значений для квантора " ∀" пуст и должно быть верным, что всешесть = истина.) По аналогии со вторым примером введем инвариантное отношение P : всешесть = (∀i : 0 ≤ i < j : f (i) = 6)) and 0 ≤ j ≤ n поскольку это отношение легко сделать истинным при j = 0 и к тому же (P and j = n) ⇒ R . Единственное, что мы должны сделать, это понять, как увеличивать j при инвариантности P . Поэтому берем wp("j := j + 1", P ) = (всешесть = (∀i : 0 ≤ i < j + 1 : f (i) = 6)) and 0 ≤ j + 1 ≤ n Справедливость последнего члена следует из справедливости P and j = n; и в этом нет никакой проблемы, так как мы уже решили, что условие j = n, взятое в качестве предохранителя, является остаточно слабым, чтобы делать выводы о значении |