Замечание к алгоритму 176

Э. Шуграф (S с h U е g г а f Е. «САСМ», 1972, № 12)

Алгоритм 176 содержит одну опечатку *. Строка, имеющая вид begin eil=yli]; должна быть

begin eti]: = z[i];

Замечание к алгоритму 195

Э. Шуграф (S с h U е g г а f Е. «САСМ», 1972, № 12)

Алгоритм 195 был переведен на ФОРТРАН-IV для мащины IBM 360/50. Были использованы различные матрицы с различными значениями пит**. Регистрировались затраты мащинного времени и проверялась точность результатов. Время выполнения процедуры (в секундах) приведено в табл. 32.

Таблица 32

Можно считать, что время выполнения процедуры пропорциенально ((т-1)4--ь2)Х/г (обратите внимание на определение т). При проверке результатов было обнаружено, что для вырожденных и близких к вырожденным матриц алгоритм дает неверные рещения. Это можно устранить, если для проверки на вырожденность ввести параметр eps и метку-параметр signal. Для этого в описании процедуры первые две строки нужно заменить на следующие: procedure (c,n,m,eps,signal) dataresult: (v);

value n,m; real eps; integer n,m; label signal; array c,v; После оператора

If abs(c[r,l])>abs(dpiv,l]) then piv:=r; . вставить оператор

if abs(oipiv,l])<eps then go to signal;

Подтверждение к алгоритму 210a

Б. Л. Шмульян, Москва, июнь 1972.

Алгоритм 210а был переведен на язык ФОРТРАН-IV (с соответствующими изменениями), транслирован в системе 4-70 и использован при п=4 для построения графиков функций по дискретным значениям (с помощью мащинного графопостроителя). Процедура иа ФОРТРАНЕ-IV имела вид

SUBROUTINE LAGR(N,U,A,X,Y) С ALGORITM 210А

DIMENSION X(1),Y(1)

* Эта опечатка была уже замечена авторами выпуска «Алгоритмы (151-200)» и исправлена в алгоритме 176а. Следует заметить, что в данном замечании Э. Шугра-фа ничего не говорится о первой поправке к алгоритму 176, указанной в «Свидетельстве к алгоритму 176а» [25]. (Прим. ред.)

** Здесь используются обозначения алгоритма 195а. В алгоритме 195 эти буквы были прописными. (Прим. ред.)

А=0.0 N1=N+1 DO 20 J=1.N1 R=1.0

DO 10 I = 1,N1 10 IF (I.NE.J) R=R*(U-X(I))/(X(J)-X(I)) 20 A=A+R*Y(J)

REroRN

Подтверждение к алгоритму 245

«Доказательство алгоритмов - новый вид подтверждения»

Р. Лондон (London R. L. «САСМ». 1970, № 6)

Аннотация

Подтверждение алгоритма может принимать форму доказательства правильности алгоритма. В качестве иллюстративного, но имеющего практическое значение примера этого утверяедения, приведено доказательство того, что алгоритм 245 является правильным.

Подтверждение алгоритмов путем доказательства

Поскольку теперь существуют соответствующие технические приемы доказательства правильности многих алгоритмов (см., например, [181-221]), то можно и уместно подтверждать алгоритмы с помощью таких доказательств. Подтверждение путем апробирования по-прежнему остается полезным, так как оно проще и дает также, например, и сведения о затратах времени. Однако наличие доказательства могло бы быть желательным дополнительным подтверждением, алгоритма. Доказательство убедительно показывает, что алгоритм отлажен, поскольку в нем нет никаких ошибок.

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

В качестве примера подтверждения алгоритма здесь доказывается, что алгоритм TREESORT 3* правильно выполняет свою задачу сортировки массива М]} : п] в порядке возрастания. Данный алгоритм был уже раньше подтвержден («САСМ», 1965, №7), но в этом подтверждении, например, не была сделана проверка для массивов нечетной длины. Поскольку TREESORT 3 является быстрым алгоритмом сортировки массива иа месте его записи, широко применяемым на практике и достаточно сложным, так что его правильность не самоочевидна, то использование TREESORT 3 в качестве примера представляет нечто большее, чем абстрактное упражнение. Это пример большой практической важности.

Краткое описание алгоритма 245 и метод доказательства

Работу алгоритма легче всего проследить, если его рассматривать как бинарное дерево. Элемент .массива Mlk-i-2] будет считаться родителем элемента Щк] для 2fe /г. Другими словами, дети элемента МЦ] - это M{2j] и M[2j-\-l] при условии, что по крайней мере один из детей существует.

* Т. е. процедура алгоритма 245. Соответствующая процедура алгоритма 245а имеет идентификатор treesort. (Прим. ред.)

Первая часть алгоритма переставляет элементы массива М, так чтобы для неко торого сегмента этого массива любой родитель стал больше любого из своих детеЬ, Каждое выполнение вспомогательной процедуры siftup расширяет этот сегмент, вызывая появление еще одного родителя, доминирующего над своими детьми. Вторая часть алгоритма использует процедуру siftup для того, чтобы сделать родителей превосходящими своих детей по всему массиву, меняет значениями MJ] с иоследним элементом и повторяет указанные действия над массивом, укороченным на один элемент. Все вышесказанное является мотивировкой, а не частью формального доказательства.

Доказательство правильности алгоритма 245 состоит из трех частей. Сначала. показывается, что процедура siftup выполняется так, как это формально определено-ниже. Затем показывается, что тело процедуры TREESORT 3, использующее процедуру siftup двумя способами, сортирует массив в порядке возрастания (доказательство-процедуры exchange опущено). Доказательство проводится по методу, описанному в работах [18i, 19i, 22i]: между строками программ вставляются утверждения, касающиеся хода вычисления, и доказательство заключается в демонстрации того, что каждое утверждение истинно в любой момент, когда выполнение процедуры достигает-этого утверждения, в предположении, что ранее встречавшиеся утверждения истинны. В заключение отдельно показывается, что процедура всегда заканчивается.

Нумеруются строки доказуемого алгоритма и соответственно утверждения, записанные в форме комментариев программы. Нумерация используется только для ссылок и никакого другого значения не имеет. Дополнительная пара скобок begin - end была-вставлена в тело процедуры TREESORT 3 для того, чтобы можно было различать. моменты вьшолнения двух утверждений (3-1 и 4.1). В процедуре siftup правильный-результат выражают утверждения 10-1 и 10.2; в теле процедуры TREESORT 3 то же-выражают утверждения 9.3 и 9-4.

Определение npou,edtjpu siftup и система обозначений

Определим формально процедуру siftup (i,n) так, что в ней п будет означать просто некоторый формальный параметр, а не длину массива М*. Пусть A{s) означает последовательность неравенств M{k-2\M[k\ для 2skn (если s>n-2, то .4(s) - пустая последовательность). Если перед обращением к процедуре siftup{i,n) выполняется .4(i-l-l) и если 1г/гразмер массива, то после выполнения обращения siftup (i,n)

1) будет выполняться Л (i),

2) элементы сегмента массива от Af[i] до Щп] будут переставлены,

3) сегмент массива вне интервала от M[i] до М{п] останется неизмененным.

Для доказательства этих свойств процедуры siftup необходимо ввести некоторые-обозначения. Формальный параметр ** i внутри процедуры siftup будет меняться. Поскольку i вызывается по значению, то вне siftup такого изменения наблюдаться не будет. Тем не менее в доказательстве процедуры siftup необходимо наравне с текущим значением i пользоваться и его начальным значением.

Пусть io будет значением i перед входом в процедуру siftup. Аналогично пусть. Мо будет значением массива М перед входом в процедуру siftup. Утверждение <s:M-p(Mc) при М:=сору» означает «Если выполнено M{i]:=eopy, то М является перестановкой Мс, как это описано в п. 2) и 3) определения процедуры siftup». Утверждение Ш = р{Мо)» означает то же самое, только без ссылки на выполнение МЩ:=сору.

* В алгоритме 245а некоторые обозначения изменены, а именно М заменено на т, loop - на iter. (Прим. ред.)

** По-вииимому, здесь Р. Лондон имел в виду фактический параметр, соответствующий формальному параметру L (Прим. ред.)