Э. Дейкстра Дисциплина программирования. Предисловие редактора перевода
 Скачать 1.14 Mb.
|
|
if x ≥ y → m := x [] y ≥ x → m := y fi Поскольку (x ≥ y or y ≥ x) = T , отказа никогда не произойдет (попутно мы получили доказательство существования: для любых значений x и y существует m, удовлетворяющее R(m)). Поскольку (x ≥ y and y ≥ x) = F , наша программа не обязательно детерминирована. Если первоначально x = y, то оказывается неопределенным, какое из двух присваиваний будет выбрано для исполнения; такая недетерминированность совершенно корректна, так как мы показали, что выбор не имеет значения. Замечание. Если бы среди доступных примитивов имелась функция "max", мы могли бы написать программу m := max(x, y), поскольку R(max(x, y)) = T . (Конец замечания.) Полученная программа не производит очень сильного впечатления; с другой стороны, мы видим, что в процессе вывода программы из постусловия на долю нашей изобретательности почти ничero не осталось. Э. Дейкстра. ”Дисциплина программирования” 41 Второй пример Для фиксированного значения n (n > 0) задана функция f (i) для 0 ≤ i < n. Обеспечить истинность R: 0 ≤ k < n and (∀i : 0 ≤ i < n : f(k) ≥ f(i)) Поскольку наша программа должна работать при любом положительном значении n, трудно себе представить, как можно обеспечить истинность R, не прибегая к помощи цикла; поэтому мы ищем отношение P , которое легко можно сделать истинным в начале программы и такое, что в конце (P and non BB) ⇒ R. Следовательно, отыскивая P , мы ищем отношение, более слабое, чем R; иначе говоря, мы хотим получить обобщение нашего конечного состояния. Стандартный способ обобщения отношения — это замена константы переменной (возможно, в ограниченном интервале), и здесь мой опыт подсказывает мне, что нужно заменить константу n новой переменной, например j, и взять в качестве P 0 ≤ k < j ≤ n and (∀i : 0 ≤ i < j : f(k) ≥ f(i)) где условие j ≤ n добавлено для того, чтобы область определения функции f была конечной. Теперь, имея такое обобщение, мы легко получаем (P and j = n) ⇒ R Чтобы подтвердить возможность использования таким образом выбранного P, мы должны рас- полагать легким средством для обеспечения истинности P в начале программы. Поскольку (k = 0 and j = 1) ⇒ P мы отваживаемся предложить следующую структуру для нашей программы (комментарии даются в скобках): k, j := 0, 1 {P стало истинным}; do j = n → некий шаг к j = n при инвариантности P od {R стало истинным} Снова мой опыт подсказывает мне выбрать в кaчестве монотонно убывающей функции t текущего состояния функцию t = (n − j), которая и в самом деле такова, что P ⇐ (t ≥ 0). Чтобы гарантировать монотонное убывание t, я предлагаю увеличивать j на 1, после чего мы можем написать wp("j := j + 1", P ) = 0 ≤ k < j + 1 ≤ n and (∀i : 0 ≤ i < j + 1 : f(k) ≥ f(i)) = 0 ≤ k < j + 1 ≤ n and (∀i : 0 ≤ i < j : f(k) ≥ f(i)) and f(k) ≥ f(j) Первые два члена следуют из P and j = n (потому что (j ≤ n and j = n) ⇒ (j + 1 ≤ n), и именно поэтому мы решили увеличить j только на 1). Следовательно, (P and j = n and f (k) ≥ f (j)) ⇒ wp("j := j + 1", P ) и мы можем использовать последнее условие в качестве предохранителя. Программа k, j := 0, 1; do j = n → if f (k) ≥ f (j) → j := j + 1 fi od действительно даст правильный ответ, если она завершится нормально. Однако нормальное завер- шение не гарантировано, поскольку конструкция выбора может привести к отказу — и это действи- тельно так и будет, если k = 0 не удовлетворяет R. Если неверно, что f (k) ≥ f (i), мы можем сделать это отношение верным при помощи присваивания k := j и продолжить наши исследования: wp("k, j := j, j + 1", P ) = 0 ≤ j < j + 1 ≤ n and (∀i : 0 ≤ i < j + 1 : f(j) ≥ f(i)) = 0 ≤ j < j + 1 ≤ n and (∀i : 0 ≤ i < j : f(j) ≥ f(i)) С огромным облегчением мы замечаем, что (P and j = n and f (k) ≤ f (j)) ⇒ wp("k, j := j, j + 1", P ) 42 Э. Дейкстра. ”Дисциплина программирования” и следующая программа будет работать, не подвергаясь опасности отказа. k, j = 0, 1; do j = n → if f (k) ≥ f (j) → j := j + 1 [] f(k) ≤ f(j) → k, j := j, j + 1 fi od Следует сделать несколько примечаний. Первое: поскольку предохранители конструкции выбора не обязательно исключают друг друга, программа таит в себе внутреннюю недетерминированность того же типа, что и в первом примере. Эта недетермированность может проявиться и внешне. Функция f могла оказаться такой, что конечное значение k неоднозначно; в этом случае наша программа может выработать любое допустимое значение! Второе примечание: то, что мы построили правильную программу, не означает, что мы справи- лись с задачей. Программирование в равной степени является как математической, так и инженерной дисциплиной; мы должны заботиться о правильности в той же мере, как скажем, и об эффективности. Исходя из предположения, что на вычисление значения функции f для данного аргумента затрачи- вается относительно много времени, хороший инженер должен обратить внимание на то, что в про- грамме, по всей вероятности, будет многократно вычисляться f (k) для одного и того же значения k. В этом случае рекомендуется пойти на сделку и пожертвовать некоторым объемом памяти, чтобы сэко- номить часть времени, затрачиваемого на вычисление. Но при этом наши усилия, направленные на повышение эффективности программы и уменьшение затрат времени, ни в коей мере не должны слу- жить извинением за внесение беспорядка в программу. (Это очевидная вещь, но я хочу подчеркнуть эту мысль, потому что очень часто запутанность программы оправдывается ссылкой на эффектив- ность. Однако при ближайшем рассмотрении такое оправдание всегда оказывается необоснованным, должно быть, потому, что запутанность программы всегда неоправданна.) Чтобы аккуратно реали- зовать обмен времени вычислений на память, можно воспользоваться методом введения одной или нескольких дополнительных переменных, чье значение можно использовать, так как сохраняется инвариантным некоторое отношение. В данном примере было замечено, что возможны частые по- вторные вычисления f(k) для одного и того же k, а это наводит на мысль о введении дополнительной переменной, скажем max, и расширении инвариантного отношения за счет дополнительного члена max = f (k) Это отношение должно стать истинным, когда k получит начальное значение, и должно сохра- няться инвариантным (при помощи явного присваивания значения переменной max) после измене- ния k. Мы приходим к следующей пpoгpaмме: k, j, max := 0, 1, f (0); do j = n → if max ≥ f (j) → j := j + 1 [] max ≤ f(j) → k, j, max := j, j + 1, f(j) fi od Вероятно, эта программа гораздо более эффективна, чем наша предыдушая версия, В таком случае хороший инженер на этом не остановится, потому что теперь он обнаружит, что мог бы распо- рядиться повторными вычислениями f (j) для одного и того же j. Для этого можно ввести дополни- тельную переменную, скажем h, и обеспечить инвариантность h = f (j) Однако мы нe можем сделать это на том же глобальном уровне, как для нашего предыдущего чле- на: значение j = n не исключено, а при этом значение f (j) не обязательно определено. Следовательно, истинность отношения h = f (j) должна заново обеспечиваться после каждой проверки, показываю- щей, что j = n, по завершении внешней охраняемой команды (так сказать, "как раз перед od") мы имеем h = f (j − 1), но нас это не должно беспокоить, и пусть все остается так, как есть. k, j, max := 0, 1, f (0); do j = n → h := f (j); if max ≥ h → j := j + 1 [] max ≤ h → k, j, max := j, j + 1, h fi od Последнее примечание касается не столько нашего решения задачи, сколько наших соображений о подходе к решению. Мы говорили о математическом подходе, мы говорили об инженерном подходе Э. Дейкстра. ”Дисциплина программирования” 43 и провели разделение между этими подходами, сосредоточивая внимание то на одном, то на другом аспекте. Хотя разделение подходов абсолютно необходимо, когда речь идет о более сложных задачах, я должен подчеркнуть, что, сосредоточивая внимание на одном из аспектов, не следует полностью игнорировать другие аспекты. Разрабатывая математическую часть проекта, мы должны помнить, что даже математически правильная программа может погибнуть, если она плоха с инженерной точки зрения. Аналогично, осуществляя "сделку" между памятью и временем, мы должны делать это аккуратно и систематически, чтобы по неряшливости не внести ошибок в программу; кроме того, хотя предварительно был проведен математический анализ, мы должны к тому же достаточно хорошо разбираться в задаче, чтобы судить о том, приведут ли предполагаемые изменения к значительному улучшению программы. Замечание. До того как я начал пользоваться этими формальными построениями, я всегда ис- пользовал "j < n" в качестве предохранителя в этой конструкции повторения, теперь я должен отучитъся от этой привычки, так как в случае, подобном данному, конечно, предпочтительнее предо- хранитель "j = n". Для этого имеются две причины. Предохранитель "j = n" позволяет нам сделать вывод, что по завершении программы j = n, не ссылаясь при этом на инвариантное отношение P ; тем самым упрощается дискуссия о том, что дает нам вся конструкция в целом по сравнению с предохранителем "j < n". Гораздо важнее, однако, что предохранитель "j = n" ставит завершение программы в зависимость от (части) инвариантного отношения, а именно j ≤ n, и поэтому ему следует отдать предпочтение, так как его использование приведет к усилению конструкции. Если в резуль- тате выполнения j := j + 1 значение j так возрастет, что станет справедливым отношение j > n, предохранитель "j < n" не поднимет тревогу, тогда как предохранитель "j = n" по крайней мере не допустит нормального завершения. Такой аргумент представляется вполне весомым, даже если не принимать во внимание сбой машины. Пусть в последовательности x 0 , x 1 , x 2 , . . . значение x 0 задается, а значение x i для i > 0 определяется как x i = f (x i−1 ), где f — некоторая вычислимая функция. Будем внимательно и точно следить за тем. чтобы сохранялось инвариантным отношение X = x i . Предпо- ложим, что в программе имеется монотонно возрастающая переменная n, такая, что для некоторых значений n нас интересуют x n . При условии что n ≥ i, мы всегда можем сделать истинным отношение X = x n при помощи do i = n → i, X := i + 1, f (X) od Если же отношение n ≥ i не обязательно имеет место (может быть, последующие изменения в программе привели к тому, что в процессе вычислений n будет не только возрастать), приведенная выше конструкция (к счастью!) не придет к завершению, в то время как конструкция do i < n → i, X := i + 1, f (X) od не обеспечит истинности отношения X = x n . Мораль этой истории такова, что при прочих равных условиях мы должны выбирать наши предохранители как можно более слабыми. (Конец замечания.) Третий пример Для фиксированных a(a ≥ 0) и d(d > 0) требуется обеспечить истинность R: 0 ≤ r < d and d|(a − r) (Здесь вертикальная черта " |" заменяет собой слова "является делителем".) Иначе говоря, нам тре- буется вычислить наименьший неотрицательный остаток r, полученный в результате деления a на d. Чтобы эта задача действительно была задачей, мы должны ограничить использование арифметиче- ских операций только операциями сложения и вычитания. Поскольку условие d|(a − r) выполняется при r = a и при этом, так как a ≥ 0, верно, что 0 ≤ r, предлагается выбрать в качестве инвариантного отношения P : 0 ≤ r and d|(a − r) В качестве функции t, убывание которой должно обеспечить завершение работы программы, мы выбираем само r. Поскольку изменение r должно быть таким, чтобы неизменно выполнялось условие d|(a − r), r можно изменять только на число, кратное d, например на само d. Таким образом, нам, как оказалось, предлагается вычислить wp("r := r − d", P ) and wdec("r := r − d", r) = 0 ≤ r − d and d|(a − r + d) and d > 0 Поскольку член d > 0 можно было бы добавить к инвариантному отношению P , обоснования тре- бует только первый член; мы находим соответствующий предохранитель "r ≥ d" и пробуем составить 44 Э. Дейкстра. ”Дисциплина программирования” такую программу: if a ≥ 0 and d > 0 → r := a; do r ≥ d → r := r − d od fi По завершении программы стало истинным отношение P and non r ≥ d, из чего следует истин- ность R, и, таким образом, задача решена. Предположим теперь, что нам, кроме того, потребовалось бы присвоить q такое значение, чтобы по окончании программы было бы также верно, что a = d ∗ q + r иначе говоря, требуется найти не только остаток, но и частное. Попробуем добавить этот член к нашему инвариантному отношению. Поскольку (a = d ∗ q + r) ⇒ (a = d ∗ (q + 1) + (r − d)) мы приходим к программе if a ≥ 0 and d > 0 → q, r := 0, a; do r ≥ d → q, r := q + 1, r − d od fi На выполнение приведенных выше программ будет, конечно, затрачиваться очень много времени, если частное велико. Можем ли мы сократить это время? Очевидно, этого можно добиться, если умень- шать r на величину, кратную и большую d. Вводя для этой цели новую переменную, скажем dd, мы получаем условие, которое должно неизменно выполняться на протяжении всей рa6oты программы: d|dd and dd ≥ d Мы можем ускорить нашу первую программу, заменив "r := r − d" уменьшением, возможно повторным, r на dd, предоставляя в то же время возможность dd, первоначально равному d, довольно быстро возрастать, например каждый раз удваивая dd. Тогда мы приходим к следующей программе: if a ≥ 0 and d > 0 → r := a; do r ≥ d → dd := d; do r ≥ dd → r := r − dd; dd := dd + dd od od fi Ясно, что отношение 0 ≤ r and d|(a − r) сохраняется инвариантным, и поэтому программа обеспечит истинность R, если она завершится нормально, но так ли это? Конечно, так, поскольку внутренний цикл, который завершается при dd > 0, возбуждается только при начальных состояниях, удовлетво- ряющих условию r ≥ dd, и поэтому уменьшение r := r − dd выполняется по крайней мере один раз для каждого повторения внешнего цикла. Но такое рассуждение (хотя и достаточно убедительное!) является весьма неформальным, а по- скольку в этой главе мы говорим о формальном построении программ, мы можем попробовать сфор- мулировать и доказать теорему, которой интуитивно воспользовались. Пусть IF, DO и ВВ понимаются в обычном смысле, и P — это отношение, сохраняющееся инва- риантным, т.е. (P and BB) ⇒ wp(IF, P ) для всех состояний (1) и пусть t — целочисленная функция, такая, что для любого значения t 0 и для всех состояний (P and BB and t ≤ t 0 + 1) → wp(IF, t ≤ t 0 ) (2) или, что то же, (P and BB) ⇒ wdec(IF, t) для всех состояний (3) Э. Дейкстра. ”Дисциплина программирования” 45 Тогда для любого значения t 0 и для всех состояний (P and BB and wp(DO, T ) and t ≤ t 0 + 1) ⇒ wp(DO, t ≤ t 0 ) (4) или, что то же, (P and BB and wp(DO, T )) ⇒ wdec(DO, t) (5) В словесной формулировке: если сохраняемое инвариантным отношение P гарантирует, что каждая выбранная для исполнения охраняемая команда вызывает действительное уменьшение t, то кон- струкция повторения вызовет действительное уменьшение t, если она нормально завершится после по крайней мере одного выполнения какой-либо охраняемой команды. Теорема настолько очевидна, что было бы досадно, если бы ее доказательство оказалось трудным, но, к счастью, это не так. Мы покажем, что из (1) и (2) следует, что для любого значения t 0 и для всех состояний (P and BBandH k (T )) and t ≤ t 0 + 1) ⇒ H k (t ≤ t 0 ) (6) для всех k ≥ 0. Это справедливо для k = 0, поскольку (BBandH 0 (T )) = F , и, исходя из предположения, что (6) справедливо для k = K, мы должны показать, что (6) справедливо и для k = K + 1. (P and BB and H K+1 (T ) and t ≤ t 0 + 1) ⇒ wp(IF, P ) and wp(IF, H K (T )) and wp(lF, t ≤ t 0 ) = wp(IF, P and H K (T ) and t ≤ t 0 ) ⇒ wp((IF, (P and BB and H K (T ) and t ≤ t0 + 1) or (t ≤ t 0 and non BB)) ⇒ wp(IF, H K (t ≤ t 0 ) or H 0 (t ≤ t 0 )) = wp(IF, H K (t ≤ t 0 )) ⇒ wp(IF, H K (t ≤ t 0 )) or H 0 (t ≤ t 0 ) = H K+1 (t ≤ t 0 ) Первая импликация следует из (1), определения H K+1 (T ) и (2); равенство в третьей строке оче- видно; импликация в четвертой строке выводится при помощи присоединения (BB or non BB) и последующего ослабления обоих членов; импликация в пятой строке следует из (6) при k = K и определения H 0 (t ≤ t 0 ); остальное понятно. Таким образом, мы доказали справедливость (6) для всех k > 0, а отсюда немедленно вытекают (4) и (5). Упражнение Измените нашу вторую программу таким образом, чтобы она вычисляла также и частное, и дайте формальное доказательство правильности вашей программы. (Конец упражнения.) Предположим теперь, что имеется маленькое число, скажем 3, на которое нам позволено умно- жать и делить, и что эти операции выполняются достаточно быстро, так что имеет смысл восполь- зоваться ими. Будем обозначать произведение "m ∗ 3" (или "3 ∗ m") и частное "m/3"; последнее выражение будет использоваться только при условии, что первоначально справедливо 3 |m. (Мы ведь работаем с целыми числами, не так ли?) И опять мы пытаемся обеспечить истинность желаемого отношения R при помощи конструк- ции повторения, для которой инвариантное отношение P выводится путем замены константы пе- ременной. Заменяя константу d переменной dd, чьи значения будут представляться только в виде d ∗ ( степень 3), мы приходим к инвариантному отношению P : 0 ≤ r < dd and dd (а − r) and (∃i : i ≥ 0 : dd = d ∗ 3 i ) Мы обеспечим истинность этого отношения и затем, заменяя его инвариантным, постараемся достичь состояния, при котором d = dd. Чтобы обеспечить истинность P , нам понадобится еще одна конструкция повторения: сначала мы обеспечим истинность отношения 0 ≤ r and dd (a − r) and (∃i : i ≥ 0 : dd = d ∗ 3 i ) |