Methods for synthesizing predicate program pieces.pdf 1. Язык предикатного программирования Программа на языке P0 определяется следующей конструкцией: (:){}, аргументы и результаты - непересекающиеся наборы имён переменных. Предположим, что x, y и z обозначают разные непересекающиеся наборы переменных. Набор x может быть пустым, наборы y и z не пусты. Простейшим оператором является вызов предиката A(x : y). Операторами языка P0 являются следующие конструкции: B(x : z); C(z : y) -последовательный оператор, B(x : y) || C(x : z) - параллельный оператор и if (e) B(x : y) e/se C(x : y) - условный оператор. Операционную семантику программы H(x : y) определим в виде предиката: R(H)(x, y) = для значения набора x исполнение программы H всегда завершается и существует исполнение, при котором результатом вычисления является значение набора y [1]. Тотальная корректность (далее просто корректность) программы относительно спецификации в виде предусловия P(x) и постусловия Q(x,y) определяется формулой Vx (P(x) ^ [Vy R(H)(x,y) ^ Q(x,y)] & 3y R(H)(x,y)). 2. Задача синтеза Пусть Q(x, y) -некоторая формула, связывающая между собой аргументы x и результаты y. Целью синтеза является получение (возможно, недетерминированным образом) программы H(x : y), вычисляющей значение результатов y из аргументов x. Будем говорить, что синтезом формулы Q(x,y) является оператор H(x : y) и предусловие P(x) в виде формулы, и писать rQ(x,y)l = H(x : y), LQ(x,y)J = P(x), если существует программа H(x : y), корректная относительно спецификации в виде предусловия P(x) и постусловия Q(x,y). Предусловие при этом описывает контекст, в рамках которого происходит вычисление. Правила синтеза строятся на базе правил доказательства корректности в системе дедуктивной верификации [2]. Утверждение 1 (Condition Rule). Для некоторой формулы Q(x,y) истинны следующие тождества: [Q(x,y)l = г/ (e(x)) [e(x) ^ Q(x,y)] e/se |~!e(x) ^ Qfoyyb LQ(x,y)J = e(x)?Le(x) ^ Q(x,y)J : L!e(x) ^ Q(x,y)J. Утверждение 2 (Call Rule). Пусть Q(x,y) -некоторая формула. Если существуют такие формулы Q'(x, x') и /(x', y), что Vx, y (Q(x, y) ^ 3x' (Q'(x, x') & /(x', y))), F(x : y) = [/(x,y)l и истинно одно из следующих утверждений: 1) /(x',y) -рекурсивный вызов и Q'(x,x') & m(x') < m(x), где m - некоторая функция меры, заданная на аргументах формулы /; 2) /(x', y) - нерекурсивный вызов, то истинны тождества |~Q(x,y)l = |~Q'(x,x')l; F(x' : y), |_Q(x,y)J = |_Q'(x,y)J. 3. Пример Рассмотрим формулу, описывающую числа Фибоначчи: fib(i) := (i = 0 or i = 1) ? i : fib(i- 1) + fib(i - 2); q(i, r) := r = fib (i) ; Очевидной программой является реализация функции fib в виде условного оператора и двух рекурсивных вызовов. Такая программа будет неэффективна, так как рекурсия не является хвостовой. В предикатном программировании для приведения рекурсии к хвостовому виду используется метод обобщения исходной задачи. Введём дополнительные параметры-накопители current = /гЬ(j) и previous = = /ib(j - 1) для некоторого j ^ г. Формула для обобщённой задачи выглядит следующим образом: g(i, j, current, previous, last) := 1

Скачать электронную версию публикации