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

Язык предикатного программирования P (P redicate programming language) [1] находится на границе между функциональными и логическими языками. Простейшим оператором языка является вызов предиката B(x: y), где B – имя предиката; x и y – различающиеся наборы переменных. Переменные набора x являются аргументами вызова, а y – результатами; в качестве аргументов допускаются выражения. Базисными операторами языка P являются: оператор суперпозиции B(x: z); C(z: y); параллельный оператор B(x: y) || C(x: z); условный оператор if ( b) B(x: y) else C(x: y), где b – выражение логического типа; x, y и z – различные наборы переменных.

Логическая семантика LS языка P [2] определяет для каждого оператора S предикат LS(S), истинный после исполнения оператора S. Логическая семантика операторов определяется следующим образом:

LS(B(x: y)) @ B(x, y);

LS(B(x: z); C(z: y)) @ $z. (B(x, z) & C(z, y));

LS(B(x: y) || C(x: z)) @ B(x, y) & C(x, z);

LS(if ( b) B(x: y) else C(x: y)) @

(b Þ B(x, y)) & (Øb Þ C(x, y)).

Предикатная программа состоит из набора определений предикатов вида:

A(x: y) º pre P(x) { S } post Q(x, y), (1)

где A – имя определяемого предиката, x – аргументы, а y – результаты предиката, S – оператор, P(x) – предусловие, Q(x, y) – постусловие. Предусловие должно быть истинно перед исполнением оператора S. а постусловие – после исполнения. Спецификация предиката A включает предусловие, постусловие и записывается в виде [P(x), Q(x, y)].

Однозначность оператора S, тотальность и однозначность спецификации [P(x), Q(x, y)] определяются, соответственно, формулами:

P(x) & LS(S)(x, y₁) & LS(S)(x, y₂) Þ y₁ = y_2;

P(x) Þ $y. Q(x, y);

P(x) & Q(x, y₁) & Q(x, y₂) Þ y₁ = y_2.

Корректность[3] определения предиката (1) со спецификацией [P(x), Q(x, y)] представляется формулой:

P(x) Þ [ LS(S)(x, y) Þ Q(x, y) ] & $y. LS(S)(x, y). (2)

Доказательство корректности для однозначных программ с однозначной и тотальной спецификацией можно проводить по более простой формуле:

P(x) & Q(x, y) Þ LS(S)(x, y). (3)

Отметим, что доказывать однозначность спецификации и программы не требуется[4]. Достаточно доказать тотальность спецификации. Формула (3) является достаточным условием формулы корректности (2).

Методы дедуктивной верификации и программного синтеза представим на примере оператора суперпозиции в следующем определении предиката:

A(x: y) º pre P(x) { B(x: z); C(z: y) } post Q(x, y). (4)

Предположим, что операторы B и C корректны относительно спецификаций [P_B(x), Q_B(x, z)] и [P_C(z), Q_C(z, y)] соответственно. Пусть спецификация [P(x), Q(x, y)] тотальна. Нетрудно доказать, что корректность предиката A гарантируется в случае истинности правил[5]:

Правило LS1. P(x) ├ P_B(x);

Правило LS2. P(x) & Q(x, y) & Q_B(x, z) ├

P_C(z) & Q_C(z, y).

На базе формулы (3) построена система правил доказательства корректности различных операторов языка P [3]. Правила для других операторов представлены в разделе 2.

Задача верификации. Пусть имеется определение (4). Операторы B и C корректны относительно своих спецификаций. Для доказательства корректности определения (4) требуется доказать тотальность спецификации [P(x), Q(x, y)] и истинность правил LS1 и LS2.

Задача синтеза. Требуется построить программу для предиката A(x: y), представленного спецификацией [P(x), Q(x, y)]. Допустим, доказана тотальность спецификации. Пусть для некоторых предикатов P_B(x), Q_B(x, z), P_C(z) и Q_C(z, y) удалось доказать истинность правил LS1 и LS2. Тогда для предиката A синтезируется определение (4) с включением в программу двух новых предикатов, а именно – B(x: z) со спецификацией [P_B(x), Q_B(x, z)] и C(z: y) со спецификацией [P_C(z), Q_C(z, y)]. Дальнейшей целью является синтез определений для B и C.

Верификация и синтез зеркальны. Если для предикатной программы сгенерируем формулы корректности, а затем по этим формулам проведем синтез, то получим эквивалентную программу. Наоборот, если на основе спецификации программы и набора формул синтезируем программу, а затем для программы сгенерируем формулы корректности, то получим эквивалентную систему формул. Однако результатом синтеза будет иная программа, чем при обычном программировании. Причина в том, что в процессе программирования неизбежно производится оптимизация программы. При оптимизации программы меняется ее логика, как правило, в сторону усложнения. Как следствие, верификация программы оказывается более сложной и трудоемкой задачей, чем её синтез.

Описываемые методы верификации и синтеза реализуются в системе предикатного программирования. Технология предикатного программирования определяет спецификацию, разработку (возможно, в режиме синтеза), верификацию и оптимизирующую трансформацию программ в классе задач дискретной и вычислительной математики. Набор трансформаций применяется к предикатной программе для получения эффективной программы на императивном расширении языка P с последующей конвертацией на любой из императивных языков, включая C, C++, ФОРТРАН и другие. Базовыми трансформациями являются:

· склеивание переменных, реализующее замену нескольких переменных одной;

· замена хвостовой рекурсии циклом;

· подстановка определения предиката на место его вызова;

· кодирование структурных объектов низкоуровневыми структурами с использованием массивов и указателей.

Дата добавления: 2015-06-27