Дедуктивный синтез программ

Рассмотрим серию конкретных примеров различных методов автоматического синтеза программ с использованием метода резолюций.

Синтез программы в функциональной форме

Самый простой пример — синтез программы уровня языка ассемблера в функциональной форме^[1].

Пусть имеется одноадресная вычислительная машина с сумматором и с тремя ячейками^[2], которые адресуются идентификаторами а, b и с. Пусть в этой машине есть команды:

• • load — загрузить число из ячейки в сумматор;
• • add — прибавить содержимое ячейки к содержимому сумматора;
• • store — записать содержимое сумматора в ячейку.

Мы хотим синтезировать программу для решения задачи с := а + Ь.

Введем только один предикат Р (и, х, у, z, s), который означает следующее: в сумматоре находится значение и, в первой ячейке — х, во второй — у, в третьей — 2, машина находится в состоянии s. Тогда аксиоматика и вывод по методу резолюций с использованием предиката ANS (см. и. 4.2.4) имеют следующий вид.

Аксиомы:

• 1) ->Р (и, х, у, z, s) v Р (х, х, у, 2, load (a, s));
• 2) -iР (и, х, у, 2, s) v Р (и+у, х, у, 2, add (6, s));
• 3) -IР (и, x, у, z, s) v P (u, x, y, u, store (c, s));
• 4) P (el, e2, e3, eA, d).

Первая строчка — описание семантики команды «загрузить содержимое ячейки а в сумматор». Аналогично описываются команды add и store (строки 2 и 3).

Аксиома, которая здесь используется (строка 4), такова: вычислительная машина всегда находится в некотором состоянии, и в ячейках и в сумматоре что-то есть.

Цель:

5) -IР (и, х, у, х + у, s) v ANS (s).

Мы хотим, чтобы в ячейках а и b находились какие-то числа i и г/, а в ячейке с — число х + у. То состояние, в котором это будет достигнуто, и есть интересующий нас ответ.

Вывод:

• 6) —ъР (рс + у, х, у, 2,, v) v A/V5(store (c, s)) 5,3;
• 7) -iР (х, х, у, 2, л) v ANS (store (c, add (5, s))) 6,2;
• 8) -iР (и, х, у, 2, s) v /LV.S'(store (c, add (6, load (a, s)))) 7,1;
• 9) /WS (store (c, add (6, load (a, d)))) 8,4.

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

Эту же программу можно синтезировать в несколько другом виде, более привычном для приверженцев императивного подхода. Для этого изменим предикат Р (и, х, у, z, L): смысл первых четырех параметров остается неизменным, L — список команд, исполнение которых привело систему из начального состояния в текущее. При этом под состоянием подразумевается конфигурация системы.

Аксиомы:

• 1) -пР (и, х, у, z, Т) v Р (х, х, у, z, [Т, 1оас1(й)]);
• 2) —iР (и, х, у, z, Т) v Р (и + у, х, у, z, [Т, add (/;)|);
• 3) —iР (и, х, у, z, Г) v Р (и, х, у, и, [Т, store (c)]);
• 4) Р (е, е2, еЗ, «4, []).

Цель:

5) —iP (u, х, у, х + у, L) v ANS (L).

Вывод:

• 6) -1 Р (х + у, х, у, 2, Г) v Т, store© ]) 5,3;
• 7) —Р (х, х, у, 2, Г) v ANS(| Т, add (6), store (c)|) 6,2;
• 8) -IР (и, х, у, z, T)/ ANS{ Т, load (fl), add (ft), store© ]) 7,1;
• 9) /EV5([load («), add (/>), store (c)]) 8,4.

Полученный результат действительно является программой на ассемблере.

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

Сделаем еще одно важное замечание по этому примеру. Программу из трех машинных команд мы специфицировали и синтезировали с помощью восьми дизъюнктов, содержащих 16 литералов, шесть связок и семь термов. Грубо говоря, ассемблер оказался примерно на порядок лаконичнее языка исчисления предикатов. Однако известно, что ассемблер далеко нс самый лаконичный язык! Современные языки программирования еще на порядок лаконичнее ассемблера (на одну операцию языка высокого уровня при трансляции порождается в среднем около 10 машинных команд). Получается, что формально специфицировать и автоматически синтезировать такую простую программу оказывается примерно в несколько сотен раз дороже, чем просто написать эту программу вручную.

Если также учесть, что среднего школьника можно обучить ассемблеру примерно за месяц, а научить читать, писать и понимать язык исчисления предикатов среднего стз’дента в университете — примерно за год, то получается, что автоматическое программирование в стиле разобранного примера в 1000 раз более дорогое удовольствие, чем традиционное ручное программирование. Следовательно, должны быть серьезные причины для применения методов автоматического синтеза программ.

В определенных ситуациях такие причины существуют. Например, автоматически синтезированная программа правильна по построению. Ее не нужно отлаживать и тестировать. Можно сказать, что синтезированная программа извлечена из доказательства своей правильности. Бывают такие специальные случаи программирования, когда никаких затрат не жалко, если можно гарантировать на 100%, что программа правильна. Тестирование не может гарантировать правильность на 100%. Кроме того, иногда тестирование оказывается дороже формального доказательства правильности или натурное тестирование принципиально затруднено. Например, системы управления оружием и боевые роботы — в этих приложениях можно пойти на любые затраты по доказательству правильности программ, если только это может помочь сэкономить на тестировании и избежать ошибок.

• [1] Чень Ч., Ли Р. Математическая логика и автоматическое доказательство теорем.
• [2] Назвать такое устройство компьютером язык не поворачивается.