РАЗДЕЛ 2
ПРОВЕРКА НЕПРОТИВОРЕЧИВОСТИ СПЕЦИФИКАЦИЙ
В настоящем разделе будут рассмотрены методы проверки непротиворечивости (выполнимости) формулы вида ?tf(t) языка L. Формула F = ?tf(t) непротиворечива, если множество WF задаваемых ею вход-выходных сверхслов не пусто, или, что то же самое, если автомат A(F) имеет непустое множество состояний. Проверка непротиворечивости как исходной спецификации, так и различных промежуточных спецификаций, получаемых в процессе синтеза алгоритма, имеет принципиальное значение для методологии доказательного проектирования. Соответствующая процедура используется в процессе проектирования не только для проверки внутренней непротиворечивости спецификации, но также для преобразования ее к виду, необходимому для применения других алгоритмов проектирования. Проверка непротиворечивости используется также для проверки корректности решений (изменений спецификации), принимаемых разработчиком при интерактивном процессе проектирования. Поэтому необходимы достаточно эффективные методы решения этой проблемы.
Описанный в разд. 1.2.2 способ построения автомата A(F) дает конструктивное решение проблемы выполнимости, однако такое решение не всегда удобно, поскольку связано, как правило, с весьма трудоемкой процедурой построения недетерминированного автомата с большим числом состояний. Ниже предлагается более удобный подход, сочетающий автоматные и логические методы и позволяющий проверять непротиворечивость спецификации, не строя соответствующего автомата [94, 95].
2.1. Общий подход к проверке непротиворечивости спецификации
Пусть Q(r, ?) - пространство состояний (см. разд. 1.2.2), ассоциируемое с формулой F = ?tf(t) глубины r, где ? - множество встречающихся в ней предикатных символов. На множестве Q(r, ?) определим отношения непосредственного следования N и непосредственного предшествования P так, что за каждым состоянием q = s0s1...sr непосредственно следуют 2|?| состояний вида s1...srs и каждому состоянию q непосредственно предшествуют 2|?| состояний вида ss1...sr?1, где s ? S?. Пусть Q1 ? Q(r, ?). Обозначим N(Q1) множество всех состояний, непосредственно следующих за состояниями из Q1, а P(Q1) - аналогичное множество для отношения P. Напомним, что формула f(t) рассматривается как представление множества Qf состояний из Q(r, ?), а именно, тех состояний, на которых она истинна. Пусть Q? и Q? - такие максимальные подмножества Qf, что Pf(Q?) = Q? и Nf(Q?) = Q?, где Pf и Nf - ограничения отношений P и N на множество Qf, тогда множество состояний автомата A(F) равно Q? ? Q? (автомат A(F) - максимальный циклический подавтомат автомата A?(F)). Очевидно, что для проверки непустоты множества состояний автомата A(F) достаточно построить одно из множеств - Q? или Q?. Таким образом, эта проверка может быть выполнена одним из следующих алгоритмов. Первый алгоритм состоит в построении последовательности множеств состояний: Q0 = Qf, Q1 = Q0 ? N(Q0), ..., Qi+1 = Qi ? N(Qi), ... до тех пор, пока для некоторого k не выполнится Qk?1 = Qk. Если при этом Qk ? ?, то множество состояний автомата A(F) также не пусто, и наоборот, Qk = ? свидетельствует о пустоте множества состояний автомата. Второй алгоритм использует отношение P и аналогичным образом строит последовательность: Q0 = Qf, Q1 = Q0 ? P(Q0), ..., Qi+1 = Qi ? P(Qi), ... Условия окончания и результат определяются так же, как и для первого алгоритма.
Рассмотрим некоторые реализации второго из приведенных алгоритмов при задании множеств состояний формулами из ?1.
Формулу f(t) ? ?1 будем называть нормализованной вправо, если максимальный ранг атомов в ней равен 0. Замену формулы f(t) нормализованной вправо формулой, полученной в результате соответствующего сдвига f(t), будем называть нормализацией вправо. Как было отмечено выше, можно считать, что f(t) в формуле ?tf(t) нормализована вправо.
Пусть r - глубина формулы f(t), ? = {p1, ..., pn} - множество содержащихся в ней предикатных символов и Q(r, ?) - пространство состояний для f(t). Обозначим S?(t?k) множество всех элементарных конъюнкций вида (t?k)& ... &(t?k), где k ? N, ? {pi, ?pi} pi? ? (i = 1, ..., n). Состояние q = s0 ... sr из Q(r, ?) задается формулой fq = s0(t?r) & ... & sr(t), где si(t?r+i) ? S?(t?r+i) и принимает значение 1 на векторе si ? S? (i = 0, ..., r).
Обозначим P(f1(t)) формулу, задающую множество всех состояний, непосредственно предшествующих состояниям из множества, задаваемого формулой f1(t). В соответствии с определениями отношения Р множество Р(q) всех состояний, непосредственно предшествующих состоянию q = s0...sr, задается формулой P(fq) = s0(t?r+1) & ... & sr?1(t). Поскольку пересечению множеств состояний соответствует конъюнкция задающих их формул, то для построения Q' достаточно уметь строить P(f1(t)) для произвольного множества состояний, задаваемого формулой f1(t). Способ построения P(f1(t)) зависит от вида формулы f1(t). Рассмотрим способы построения P(f1(t)) для представлений f1(t) в виде д.н.ф. и в виде к.н.ф.
1. f(t) задана в виде нормализованной вправо д.н.ф. и, следовательно, задает множество состояний из Q(r, ?), на которых она истинна.
Определение 2.1. Литера есть атом или его отрицание.
Определение 2.2. Конституентой единицы для множества пропозициональных переменных {p1, ..., pn} называется элементарная конъюнкция, содержащая для каждого i = 1, ..., n либо pi, либо ?pi.
Выше было показано, как получаются P(f1(t)) если f1(t) представляет собой конституенту единицы fq. Из приведенных выражений видно, что P(fq) получается из fq в результате удаления всех литер максимального (нулевого) ранга и сдвига полученной элементарной конъюнкции на 1 вправо. Нетрудно убедиться, что таким же образом P(f1(t)) получается, если f1(t) произвольная элементарная конъюнкция литер. При этом, если она не содержит литер нулевого ранга, то осуществляется только сдвиг на 1 вправо, если же f1(t) состоит только из литер нулевого ранга, то P(f1(t)) представляет собой тождественно истинную функцию. Пу