Описание процесса верификации логических программ

Полагаем, что предложения множества S имеют вид

r() <=> D,

где r() – предикат (определяемое), D – формула (определяющее).

Процесс верификации состоит в построении доказательства, на i -ом шаге которого строится новое определение для r() согласно утверждения:

((S |= (r() <=> Di-1), (S |= (Di-1 <=> Di) => (S |= (r() <=> Di), i=1¸n.

Цель доказательства – получить, что Dn = B1 V B2 V … Bm,

Где Bi имеет синтаксис тела процедуры.

Т.е. достаточно вывести формулы r():- Bi.

Если окажется, что выведено множество процедур программы (P, G), то будет доказано, что (P, G) полностью правильна.

Замечание. Подобный процесс выполняется для каждого предиката множества Р.

Классический пример Грина верификации программы.

Дана программа.

P1: подмножество(X, Y):- пустое(X, Y). % X является подмножеством Y если X пустое (встроенный, Æ)

P2: подмножество(T: X’, Y):- T Î Y, подмножество(X’, Y). % T: X’ ={ T }ÈX’== (cons T X’).

P3: T Î T: z. % T – произвольный элемент, X’ – множество.

P4: T Î U: z.:- T Î z.

G:?подмножество(w: a: Æ, a: b: c: Æ) % Æ - пустое множество, константа.

Программа описывает знания системы о решении задачи: Для каких w множество { w, a } является подмножеством для { a, b, c }.

Выберем спецификацию из предложений вида

S1: подмножество(X, Y) <=> ("U) ((UÎ X) => (UÎ Y).

S2: (UÎ X) <=> ($ T $ X’) (X = T: X’, (U = T V U Î X’)).

S3: пустое(X) <=> Ø ($ T $ X’) (X = T: X’).

Предполагается, что имеется встроенное точное описание отношения равенства.

Выведем процедуры Р.

Поскольку

D0: подмножество(X, Y) <=> ("U) ((UÎ X) => (UÎ Y),

на основании S2 получим новое определение

D1: подмножество(X, Y) <=> ("U) ($ T /*такое что если*/ $ X’) (X = T: X’, (U = T V U Î X’) => (UÎ Y)).

Попытаемся выделить какое-либо определение в правой части D1, совпадающее с одним из определяющих.

Очевидно, что можно выделить из определяющих S3:

D2: подмножество(X, Y) <=> Ø ($ T $ X’) (X = T: X’) V ($ T $ X’) ((X = T: X’, ("U) ((U = T V U Î X’) => (U Î Y)))

с помощью правила ((B V C) ® A) ~ ((B ® A) L (C® A), которое выводится следующим образом:

Ø(B V C) V A ~ (ØB L ØC) V A ~ (ØB V A) L (ØC V A) ~ ((B ® A) L (C® A).

Очевидно, что новое определение D3 примет вид:

D3: подмножество(X, Y) <=> пустое(X) V ($ T $ X’) ((X = T: X’, ("U) ((U = T V U Î X’) => (U Î Y))).

На основании S1, S2 новое определение примет вид:

D4: подмножество(X,Y)<=>пустое(X) V ($ T $ X’) ((X = T: X’, T Î Y, подмножество(X’, Y)).

Получили, что D4 имеет вид:

D4: подмножество(X, Y) <=> B1 V B2.

D4 порождает 2 процедуры:

P1: подмножество(X, Y):- пустое(X).

P2: подмножество(X, Y):- X = T: X’, T Î Y, подмножество(X’, Y).

Из последнего предложения с учетом знака равенства X = T: X’ получим:

P2: подмножество(T: X’, Y):- T Î Y, подмножество(X’, Y).

Аналогично выводятся процедуры Р3 и Р4.

Пусть D0 имеет вид

D0: (UÎ X) <=> ($ T $ X’) (X = T: X’, (U = T V U Î X’))

на основании правила (A L (B V C)) ~ ((A L B) V (A L C)) преобразования D0 в D1.

D1: (UÎ X) <=> ($ T $ X’) (X = T: X’, U = T) V (X = T: X’, U Î X’):

(UÎ X) <=> X = T: X’, U = T, (UÎ X) <=> X = T: X’, U Î X’.

Учитывая знак равенства получим

P3: T Î T: X’

P4: U Î T: X’:- U Î X’.

Таким образом, процедуры P1, P2, P3, P4 получены на основании выбранной спецификации,

что позволяет утверждать, что (P, G) полностью правильная программа.

Если учесть, что выбрана система резолютивного вывода, то на основании ее корректности и полноты можно утверждать, что (P, G, C) – полностью правильное исполнение относительно S.

Замечание. На разработку верификаторов накладываются теоретические ограничения.

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

Т.о., стоит задача классификации логических программ.

Приведенные критерии следует рассматривать как условия синтеза, необходимые правильным программам. При этом процедуры выводятся из спецификации.