О сравнении программ

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

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

Я проделал много экспериментов, и могу следующим образом подытожить накопленный мною опыт. Две программы, которые вызывают вычисления, приводящие к одинаковым результатам, эквивалентны именно в этом смысле и заведомо ни в каком другом. :и мы хотим сравнивать программы с целью сравнения соответствующих им вычислений, то основной вывод состоит в следующем. Это невозможно (или бесполезно, непривлекательно, или ужасно трудно, или подберите любой другой отрицательный эпитет), если по-разному организовано следование по двум программам, которые мы пытаемся сравнить.

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

Исключая побочный эффект логической проверки и предполагая значение "B2" постоянным (т. е. не изменяемым при выполнении "S1", так и "S2"), мы можем установить эквивалентность следующих двух программ:

if B2 then

begin while B1 do S1 end

else begin while B1 do S2 end

(1)

while Bl do

begin if B2 then S1 else S2 end

(2)

В первой конструкции следование на первом уровне управляется заголовком выбора, а во второй конструкции - заголовком повторения. Я могу доказать эквивалентность результатов вычислений, однако я не могу считать эти программы эквивалентными при какой-либо другой полезной интерпретации понятия эквивалентности. Я вынужден был прийти к заключению, что "трудно сравнивать" программы (1) и (2). Сначала такой вывод весьма удручал меня. Однако со временем я смирился с тем, что такая несравнимость является реальным фактом; в этом одна из основных причин того, что выбор между (1) и (2) приходится рассматривать как волевое решение, которое должно приниматься с учетом детального изучения вариантов. Именно кажущаяся тривиальность выбора побуждает меня придавать особое значение изучению, которое должно влиять на такой выбор. Это изучение вариантов программ выходит за рамки данного раздела, но я собираюсь вернуться к нему в дальнейшем.

Приведу теперь второй, несколько более сложный пример несравнимости.

Заданы два массива X[1:N] и Y [1:N] и имеется логическая переменная "равны"; требуется составить программу, которая присваивает логической переменной "равны" значение высказывания "данные два массива поэлементно равны".

Пустые массивы (при N=0) считаются равными.

Введя переменную j и присваивая переменной "равны" значение высказывания "среди первых j пар не обнаружено отличий", мы можем написать следующие две программы:

j:=0; равны: = true; while jN do

begin j:=j+1; равны:=равны(X[j] = Y[j]) end

(3)

j:=0; равны = true; while jN равны do begin j:=j+1; равны:=(X[j] = Y[j]) end

(4)

Программа (4) отличается от программы (3) тем, что повторения заканчиваются, как только обнаружено отличие в какой-то паре. При одних и тех же входных данных число повторений в этих двух программах может отличаться; поэтому эти программы сравнимы в нашем понимании только тогда, когда две последние строки каждой программы считаются описывающими единое действие, не подразделяемое на поддействия. Но какая же между ними связь с точки зрения результатов после завершения повторений? Чтобы выяснить это, докажем правильность данных программ. Для массивов X и Y мы можем определить (N+l) функций РАВНЫj при 0jN следующим образом:

при j=0 PABHЫj=true

при j>0 РАВНЫj=РАВНЫj-1(X[j]=Y[j])

(5)

В терминах этих функций требуется доказать окончательный результат: равны=РАВНЫN

Обе программы сохраняют отношение

равны := РАВНЫj

(6)

при возрастании значений j,, начиная от j=0. Было бы заманчиво рассматривать программы (3) и (4) как различные конкретизации одной и той же (абстрактной) программы (7):

j:=0; равны : = РАВНЫ0; while "возможно, все еще: равны РАВНЫN" do begin j:=j+1; равны: =РАВНЫj end

(7)

в которой фраза "возможно, все еще: равны РАВНЫN", заменяет некоторое открытое элементарное условие типа "до сих пор". В процессе выполнения этой программы будет поддерживаться отношение равны=РАВНЫj

Программы (3) и (4) отличаются тем, что они с помощью разных критериев обеспечивают для переменной "равны" конечное значение РАВНЫN.

В программе (3) выбран очень простой критерии, а именно j=N

Когда начинается очередное выполнение повторяемого оператора, отношение равны=РАВНЫj

все еще выполняется. Поэтому после выполнения присваивания j:=j+1 выполняется отношение равны =РАВНЫj-1

и поэтому оператор присваивания равны:=равны (X[j] - Y[j])

представляет собой непосредственную запись рекуррентного соотношения (5). Чтобы прийти к программе (4), мы должны предварительно провести некоторый анализ применительно к рекуррентному соотношению (5). Из этого соотношения можно вывести (опять таки с помощью математической индукции), что если PABHЫj=false, то PABHЫN=false и поэтому если PABHЫj=false, то РАВНЫj=РАВНЫN. Если возникает такая ситуация, то можно гарантировать и равенство "равны=РАВНЫN,", и это приводит к программе (4). Набор поддействий, с которыми должен справиться повторяемый оператор в программе (4), ограничивается начальным состоянием "paвны=true", и поэтому в программе (4) присваивание "равны: = РАВНЫj" может быть упрощено до вида равны:=(Х[j] =Y[j])

Теперь ясно, почему введение программы (7) как абстракции программ (3) и (4) только запутало ситуацию. С помощью фразы "возможно, все еще: равныРАВНЫN" мы устанавливали истинность или ложность логического выражения, не сформулировав само это выражение, и это оказалось очень сложным. Мы пытались интерпретировать (7) как программу, в которой следование на верхнем уровне было частично не определено и изменялось в зависимости от конкретизации. В итоге мы пытались рассматривать последние строки программы (7) как модель для последних строк как программы (3), так и программы (4), но это оказалось бесперспективным, поскольку вызываемые этими строками вычисления не могут быть разложены с соблюдением взаимно однозначного соответствия. На этом мы заканчиваем обсуждение программ, которые мы считаем несравнимыми. Примеры сравнимых программ будут встречаться в следующих разделах.Заключительное замечание: мы сформулировали принцип, что "сопоставляемые вычисления могут быть разложены в последовательность действий, между которыми удается установить взаимно однозначное соответствие". Мы вовсе не требовали, чтобы такие сопоставляемые действия приводили к одинаковым результатам! Мы можем сравнивать не только разные варианты программ для выполнения одной и той же работы, но и различные программы для выполнения сходных работ.

Содержание раздела