TURBO PASCAL

Программы   

Turbo Pascal 

Игры

Документация   

Странности

FAQ

Ссылки

Форум

Живой Журнал

Гостевая книга

Рассылка

Благодарности

Об авторе

В моих примерах я буду формулировать требования задачи в форме "для фиксированных х, у, ... ", что является сокращенной записью формы "для любых значений xq, уо, ... постусловие вида х = xq and у = уо and ... должно вызывать предусловие, из которого следует, что х = xq and у = уо and ...". Эта связь между постусловием и предусловием будет гарантирована тем, что мы будем относиться к таким величинам как к "временным константам"; они не будут встречаться в левых частях операторов присваивания.

Для фиксированных хну обеспечить истинность отношения R(m).

и следующая программа будет работать, не подвергаясь опасности отказа.

Второе примечание: то, что мы построили правильную программу, не означает, что мы справились с задачей. Программирование в равной степени является как математической, так и инженерной дисциплиной; мы должны заботиться о правильности в той же мере, как скажем, и об эффективности. Исходя из предположения, что на вычисление значения функции / для данного аргумента затрачивается относительно много времени, хороший инженер должен обратить внимание на то, что в программе, по всей вероятности, будет многократно вычисляться f(k) для одного и того же значения k. В этом случае рекомендуется пойти на сделку и пожертвовать некоторым объемом памяти, чтобы сэкономить часть времени, затрачиваемого на вычисление. Но при этом наши усилия, направленные на повышение эффективности программы и уменьшение затрат времени, ни в коей мере не должны служить извинением за внесение беспорядка в программу. (Это очевидная вещь, но я хочу подчеркнуть эту мысль, потому что очень часто запутанность программы оправдывается ссылкой на эффективность. Однако при ближайшем рассмотрении такое оправдание всегда оказывается необоснованным, должно быть, потому, что запутанность программы всегда неоправданна.) Чтобы аккуратно реализовать обмен времени вычислений на память, можно воспользоваться методом введения одной или нескольких дополнительных переменных, чье значение можно использовать, так как сохраняется инвариантным некоторое отношение. В данном примере было замечено, что возможны частые повторные вычисления f(k) для одного и того же k, а это наводит на мысль о введении дополнительной переменной, скажем max, и расширении инвариантного отношения за счет дополнительного члена

Замечание. До того как я начал пользоваться этими формальными построениями, я всегда использовал "j < n" в качестве предохранителя в этой конструкции повторения, теперь я должен отучитъся от этой привычки, так как в случае, подобном данному, конечно, предпочтительнее предохранитель "j 7^ п". Для этого имеются две причины. Предохранитель "j =£• п" позволяет нам сделать вывод, что по завершении программы j = п, не ссылаясь при этом на инвариантное отношение Р; тем самым упрощается дискуссия о том, что дает нам вся конструкция в целом по сравнению с предохранителем "j < п". Гораздо важнее, однако, что предохранитель "j ^ п" ставит завершение программы в зависимость от (части) инвариантного отношения, а именно j < п, и поэтому ему следует отдать предпочтение, так как его использование приведет к усилению конструкции. Если в результате выполнения j := j + 1 значение j так возрастет, что станет справедливым отношение j > п, предохранитель "j < п" не поднимет тревогу, тогда как предохранитель "j ^ п" по крайней мере не допустит нормального завершения. Такой аргумент представляется вполне весомым, даже если не принимать во внимание сбой машины. Пусть в последовательности х_{0, х\, х2,... значение х0 задается, а значение xi для г > 0 определяется как xi = f(xi-i), где / — некоторая вычислимая функция. Будем внимательно и точно следить за тем. чтобы сохранялось инвариантным отношение X = xi. Предположим, что в программе имеется монотонно возрастающая переменная п, такая, что для некоторых значений п нас интересуют хп. При условии что п > г, мы всегда можем сделать истинным отношение X = хп при помощи}

Тогда для любого значения to и для всех состояний

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

Первая импликация следует из (1), определения Hx+i(T) и (2); равенство в третьей строке очевидно; импликация в четвертой строке выводится при помощи присоединения (В В or поп В В) и последующего ослабления обоих членов; импликация в пятой строке следует из (6) при k = К и определения Ho(t < to); остальное понятно. Таким образом, мы доказали справедливость (6) для всех k > О, а отсюда немедленно вытекают (4) и (5).

Измените нашу вторую программу таким образом, чтобы она вычисляла также и частное, и дайте формальное доказательство правильности вашей программы. (Конец упражнения.)

И опять мы пытаемся обеспечить истинность желаемого отношения R при помощи конструкции повторения, для которой инвариантное отношение Р выводится путем замены константы переменной. Заменяя константу d переменной dd, чьи значения будут представляться только в виде d * ( степень 3), мы приходим к инвариантному отношению Р:

а затем будем увеличивать dd, пока его значение не станет достаточно большим и таким, что г < dd. Получим следующую программу:

Измените приведенную выше программу таким образом, чтобы она вычисляла также и частное, и дайте формальное доказательство правильности вашей программы, Это доказательство должно наглядно показывать, что всякий раз, когда вычисляется dd/З, имеет место 3\dd. (Конец упражнения.)

do г > dd —¥ г := г — dd od

Если мы возьмем RI в качестве сохраняемого инвариантным отношения Р, получим такое возможное решение:

Очевидно, что после первого присваивания Р становится истинным и ни одна из охраняемых команд не нарушает его истинности. По завершении программы мы имеем поп ВВ, а это есть отношение R2. В том, что программа действительно придет к завершению, каждый из нас убеждается по-разному в зависимости от своей профессии: математик мог бы заметить, что число перестановок убывает, исследователь операций будет интерпретировать это как максимизацию gl + 2*g2 + 3*g3 + 4* g4, а я — как физик — сразу "вижу", что центр тяжести смещается в одном направлении (вправо, если быть точным). Программа примечательна в том смысле, что, какие бы предохранители мы ни выбрали, никогда не возникнет опасности нарушения истинности Р: предохранители, используемые в нашем примере, являются чистым следствием необходимости завершения программы.

Замечание. Заметьте, что мы могли бы добавить также и другие варианты, такие, как

причем их нельзя использовать для замены одного из трех, перечисленных в программе. (Конец замечания.)

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

Нам требуется составить программу аппроксимации квадратного корня; более точно: для фиксированного п (п > 0) программа должна обеспечить истинность

распоряжении,— это умножение и деление на (малые) степени 2. Тогда наша последняя программа оказывается не такой уж хорошей, т. е. она нехороша, если мы предполагаем, что значения переменных, с которыми непосредственно оперирует машина, отождествлены со значениями переменных а и с, как это было бы при "абстрактных" вычислениях. Другими словами, мы можем рассматривать а и с как абстрактные переменные, чьи значения представляются (в соответствии с соглашением, предусматривающим более сложные условия, чем просто тождественность) значениями других переменных, с которыми в действительности оперирует машина при выполнении программы. Мы можем позволить машине работать не непосредственно с а и с, а с р, q, r, такими, что

Мы видим, что это — преобразование координат, и каждой траектории в нашем (а, с)-пространстве соответствует траектория в нашем (р, q, г)-пространстве. Обратное не всегда верно, так как значения р, q и г не независимы: в терминах р, q и г мы получаем избыточность и, следовательно, потенциальную возможность, пожертвовав некоторым объемом памяти, не только выиграть время вычислений, но даже избавиться от необходимости возводить в квадрат! (Совершенно ясно, что преследовалась именно эта цель, когда строилось преобразование, переводящее точку в (а, с)-пространстве в точку в (р, q, г)-пространстве.) Теперь мы можем попытаться перевести все булевы выражения и перемещения в (а, с)-пространстве в соответствующие булевы выражения и перемещения в (р, q, r) -пространстве. Если бы нам удалось сделать это в терминах допустимых операций, наша задача была бы успешно решена. Предлагаемое преобразование и в самом деле отвечает нашим требованиям, и результатом его является следующая программа (переменная h была введена для очень локальной оптимизации)

Этот пятый пример был включен благодаря истории его создания (правда, несколько приукрашенной). Когда младшей из двух наших собак было всего несколько месяцев, я однажды вечером пошел погулять с ними обеими. Назавтра мне предстояло читать лекции студентам, которые всего лишь несколько недель назад начали знакомиться с программированием, и мне нужна была простая задача, чтобы на ее примере я мог "массировать" решения. В течение часовой прогулки я продумал первую, третью и четвертую программы, правда, правильно ввести h в последней программе я смог только при помощи карандаша и бумаги, когда вернулся домой. Ко второй программе, той, которая оперирует с а и Ъ и которая была здесь представлена как переходная ступень к нашему третьему решению, я пришел лишь несколько недель спустя — и она была тогда в гораздо менее элегантной форме, чем представлена здесь. Вторая причина для ее включения в число представленных программ — это соотношение между третьей программами: по отношению к четвертой программе третья представляет собой наш первый пример так называемой "абстракции представления".

Для фиксированных X (X > 1) и Y (Y > 0) программа должна обеспечить истинность отношения

Последнее заключение справедливо, поскольку (Р and h = 1) => R. Приведенная выше программа придет к завершению, если после конечного числа применений операции "сжимания" h станет равным 1. Проблема, конечно, в том, что мы не можем представить значение h значением конкретной переменной, с которым непосредственно оперирует машина; если бы мы могли так сделать, мы могли бы сразу присвоить z значение X^{Y , не затрудняя себя введением h. Фокус в том, что для представления текущего значения h мы можем ввести две — на этом уровне конкретные — переменные, скажем хну, и наше первое присваивание предлагает в качестве соглашения об этом представлении}

Тогда условие "h ^ 1" переходит в условие "у ^ 0", и наша следующая задача состоит в том, чтобы подыскать выполнимую операцию "сжимания". Поскольку при этой операции произведение h * z должно оставаться инвариантным, мы должны делить h на ту же величину, на которую умножается z. Исходя из представления h, наиболее естественным кандидатом на эту величину можно считать текущее значение х. Без дальнейших затруднений мы приходим к такому виду нашей абстрактной программы:

Глядя на эту программу, мы понимаем, что число выполнений цикла равно первоначальному значению Y, и можем задать себе вопрос, нельзя ли ускорить программу. Ясно, что задачей охраняемой команды является сведение у к нулю; не изменяя значения h, мы можем проверить, нельзя ли изменить представление этого значения в надежде уменьшить значение у. Попытаемся воспользоваться тем фактом, что конкретное представление значения h, заданное как х^{у, вовсе не является однозначным. Если у четно, мы можем разделить у на 2 и возвести х в квадрат, при этом значение h совсем не изменится. Непосредственно перед операцией сжимания мы вставляем преобразование, приводящее к наиболее привлекательному преобразованию h и получаем следующую программу:}

Тогда условие "h ^ 1" переходит в условие "у ^ 0", и наша следующая задача состоит в том, чтобы подыскать выполнимую операцию "сжимания". Поскольку при этой операции произведение h * z должно оставаться инвариантным, мы должны делить h на ту же величину, на которую умножается z. Исходя из представления h, наиболее естественным кандидатом на эту величину можно считать текущее значение х. Без дальнейших затруднений мы приходим к такому виду нашей абстрактной программы:

 Оглавление

На первую страницу

(с)Все права защищены

По всем интересующим вопросам прошу писать на электронный адрес