Главная Промышленная автоматика.

8.!: МИМИ для l=r=i-1 8.2: M[p]M,Ip+l] для i<pn-1 8.3: M[k4-21Mikl для 4kj-1;

S end;

comment

9.1: MIIp]=M[p+l] для 2=p=n-1 9.S; M[2]M,11]

9.3: M[p]M[p+l] для lpn-1, т. e. массив M

полностью упорядочен 9.4: М является перестановкой элементов Мо;

Обоснование утверждений тела процедуры TREESORT 3

Справедливость вышеуказанных утверждений основывается на следующих соображениях.

Ю.1: Пустое утверждение, поскольку 2(n-2-f 1)>п.

.2.1: Если пришли от 0.1, то согласно 1 подставляем i=n-=-2 в 0.1. Если пришли от 3.1, то согласно 1 подставляем i=i-f-l в 3.1, для объяснения изменения i от 3.1 к 2.1.

5.2: 2.1, границы для i определяются строкой 1, а п-размер массива. 3.1: 2.1 и определение процедуры siftup (i,n). -4.1: Пустое утверждение.

4.2: Если п4, то выполняется 3; следовательно, ори i=2 имеет место 3.1. Если

пЗ, то данное утверждение пустое. €.1-6.3: Если пришли от 4.1, то

6.1-6.2: Согласно 5 подставляем i=n в 4.1 и 4.2. 6.3: Для i=n это пустое утверждение. Если пришли от 8.1, то согласно 5 подставляем i=i-I-l в 8.2, 8.3 и 8.1 соответственно.

-6.4: 5 и 6.2, т. е. А(2) для подмножества MJl:!]. •7.1: 6.1 и п. 3 определения процедуры siftup. 7.2: 6.2 и п. 1 определения процедуры siftup.

7.3: 7.2, заметив, что М[1]=М[к-;-2] при к=2 и что операция рекуррентна. 7.4: Для i = n это пустое утверждение. В других случаях 6.3 для соответствующего

г, так как согласно п.2 определения siftup iVLIl] в 7.3-это один из элементов

М[г] в 6.3 для lri. e.l: 7.3 с учетом изменений, вызванных строкой 8 (этой строкой изменились значения

только Mil] и M[i]).

8.2: Согласно 8 заменяем в 7.4 М[1] на Mli]; тогда 7.1 будет выполняться и для p = i.

8.3: 7.2, исключая только одно или два соотношения вида М[1]... и одно соотношение вида.. .МИ.

3.1-9.3: Если п2, то выполняется 8; 9.1: 8.2 при i=2. 9.2: 8.1 при i=2. 9.3: 9.1 и 9.2.

Если п1, то 9.1-9.3-пустые утверждения. 9.4: Над массивом М выполнялись только операции siftup и exchange, после каждой из которых массив М является перестановкой элементов массива Мо.

Доказательство конечности процедуры TREESORT 3

Если процедуры siftup и exchange заканчиваются, то, очевидно, заканчивается и процедура TREESORT 3. Заметим, что оба параметра процедуры sipup вызываются по значению, так что в телах операторов цикла значение i не меняется.



Процедура exchange, безусловно, заканчивается. В процедуре siftup бесконечный цикл может возникнуть только при переходе от строки 3 к строке 8Ь и обратно к строке 3. Заметим, что все изменения параметра i (только в 8Ь) и переменной / (только в строках 3 и 6Ь) JBCTpe4aroTCH только в это.м цикле, и что на каждо.м витке этого цикла меняются как i так и /. Согласно условию в строке 4 достаточно показать, что / строго возрастает по величине. Неравенство 1 означает, что 2i>i. В 8Ь /=i<2i, в то время как в 3 j=2i, т. е. у"(в 3)=2i>i=/ (в 8Ь). Следовательно, каждое присваивание переменной / в строке 3 строго увеличивает значение /. Другое присваивание переменной / (в 6Ь), если оно делается, тоже приводит к увеличению значения /.

Замечание к «Подтверждению алгоритма 245» Р. Лондона

К. Редиш (R е d i S h К. А. «The Computer Journal», 1971, № 1)

В своем «Подтверждении к алгоритму 245» («САСМ», 1970, № 6) Ралф Л. Лондон продемонстрировал широко распространенную путаницу между понятиями алгоритм, его представление и результат его трансляции - код. При современном состоянии этого вопроса мы можем, вообще говоря, пытаться доказывать алгоритм и апробировать код. Возъмш, например, утверждение Р. Лондона «... алгоритхм TREESORT 3 правильно выполняет свою задачу сортировки массива M{l:n] в порядке возрастания». В то время как это верно для алгоритма, это не будет верно для кода, пока мы не наложим ограничения на элементы массива. Ошибка в этом примере возникает от того, что процессоры обладают конечной точностью; логическое выражение АВ (real А, В) обычно будет транслироваться как А-ВО, что может дать неверный результат из-за переполнения или возникновения машинного нуля.

Остается вопрос, верно ли указанное утверждение для представления алгоритма в форме данной АЛГОЛ-программы. Поскольку в TREESORT 3 явно не используются никакие арифметические операции, то мы хможем говорить, что для данного представ ления на языке АЛГОЛ данного алгоритма доказательство справедливо. Однако это более или менее случайно; оно не было бы справедливым, если бы автор оригинала написал что-нибудь вроде if Л4/--1]-yM[y]>0 даже в одном месте. Кроме того, это налагает весьма большую ответственность на апробирование кода и значительно снижает полезность доказательств. (Существует очень много примеров математически правильных алгоритмов, которые дают совершенно неверные результаты, если используется арифметика с конечной точностью.)

По-видимому, доказательство представления алгоритма на языке АЛГОЛ должно учитывать раздел 3.3.6 сообщения об этом языке [21]: «Числа и переменные типа real должны интерпретироваться в смысле численного анализа, т. е. как объекты, определенные с присущей им конечной точностью.»

Для доказательства TREESORT 3 мы могли бы добавить ограничения

1) min{abs(M[i])}tol

2) max{abs(Mii])} 1/2х (максимальное представимое число типа real),

где tol - наименьшее представимое число типа real, разделенное на macheps, где та-cheps -это наименьшее число, такое что l-fmacheps 1. [Условие 2) могло бы быть заменено условием, что все Mii] одного знака.]

Теперь мы могли бы с ycnexoiM начинать апробирование кода; значения величин, используемых в условиях 1) и 2), должны быть хорошо известны для конкретного процессора, и главная задача состоит в том, чтобы проверить, точно ли код соответствует алгоритму. Несмотря на то, что апробирование выполняется проще, оно должно быть исчерпывающим; опечатка может привести к коварны.м последствиям.

Ответ Р. Лондона на вышеуказанное замечание К. Редиша.

Замечание д-ра К. Редиша представляет собой стандартное возражение, часто высказываемое против такого рода доказательства. Мое утверждение состояло и состо-



ИТ В-том, что подтверждение алгоритма может принимать форму доказательства правильности алгоритма. В тех пределах, в которых доказательство учитывает особенности конкретного процессора и конкретной машины, хорошо известные различия между алгоритмом, его представлением и кодом можно игнорировать. Существование «математически правю;ьных алгоритмов, которые дают совершенно неверные результаты, если используется арифметика с конечной точностью» означает только то, что доказательство математической правильности не применимо полностью к соответствующему коду. Но коды доказывались - доказательства [26i, 27i] правильности (исходный код) машинного представления в интервальной арифметике охватывают такие детали, как величина машинных оперантов, машинная арифметика, переполнение, машинный нуль и операции с двойной точностью.

Кроме того, мое подтверждение путем доказательства следует совету Хоара C24i, С.579] «...по-видимому, лучше доказывать «условную» правильность программы и полагаться на представление, чтобы предупреждать, если нужно, отказ от вьшолнения программы, возникающий в результате нарушения границы представления».

Эта точка зрения дает ответ на беспокойство Редиша относительно переполнения и машинного нуля, но она не может быть применима к вопросу об ошибках округления и к вопросу о точности. Разумеется, я не претендую на то, что смогу дать анал.та •ошибок такой, какой дается в численном анализе. Если доказанный алгоритм вызывает затруднения и если верят доказательству, то причину этих затруднений будут искать в специфических особенностях машины (не учтенных в доказательстве), а ие в так называемых «логических ошибках». Доказательство исключает их надежно.

Редиш утверждает, что необходимо накладывать ограничения на элементы массива. Однако существуют реализации языка АЛГОЛ (такие как на машине Burroughs В 5500), в которых неравенство АВ не приводит к переполнению или машинному нулю. (Отношение проверяется непосредственно, без вычитания.) Эти ограничения не являются необходимыми даже для кода TREESORT 3, хотя ограничения 1) и 2) представляются достаточными, чтобы исключить переполнение или машинный нуль. Однако ограничение 1) нужно исправить. Слово «наименьшее» в обоих случаях его применения яолжно быть заменено словами «наименьшее положительное».

Рассмотрим еще строку 3 процедуры siftup

loop: j: = 2Xi;

а представим себе, что сортируется массив yM{l:Af], где N - наибольшее целое число, представимое в данном процессоре. Существуют простые примеры, которые требуют вычисления j=2xN, т. е. зависящей от представления величины, которая необходима в тесте строки 4. Поскольку массив такого размера, по существу, невозможно даже описать, то 1Можно избегать применения массивов с границей индекса Л-4-2. Так нужно ли и об ЭТОМ заявлять в явной форме?

Разумеется, в других алгоритмах ограничения могут быть очень нужны, но это зависит от типа доказательства (или от различий между алгоритмом, его представлением и кодом). В идеальном случае особенности арифметики конечной точности (см., например, [28i, 29i]) в доказательстве подтверждения должны учитываться. Но когда это неуместно, невыполнимо или просто ие делалось, то допустимо «качество на риск покупателя», точно так же как оно допустимо сейчас, когда доверяют алгоритму, подтвержденному стандартным способом на своей собственной машине. Представляется маловерочтным, что стандартное подтверждение или подтверждение доказательством когда-нибудь смогут или будут должны охватывать все особенности всех машин.

Хотя опечатка, на которую ссылается Редиш, действительно может привести к каверзным последствиям, но это могут сделать и многие другие подобные факторы, такие как изменения в трансляторе или операционной системе, не объявленные со времени последнего выхода програ1Ммиста на машину, непонимание программистом структуры языка или ошибка перфорации. Все эти важные вещи находятся вне моего





0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 [41] 42 43

0.0037