Полна ли моя спецификация?
Другой вопрос, который может вас тревожить: есть ли какой-нибудь способ убедиться в том, что спецификация описывает все нужные свойства объектов, для которых она предназначена? Студенты, которым требуется написать их первые спецификации (например, проделать упражнения в конце этой лекции), часто приходят с аналогичным вопросом: "Как узнать, что я уже специфицировал достаточно свойств и могу остановиться?"
В более общей форме вопрос звучит так: существует ли метод, позволяющий определять полноту спецификации АТД?
Если непосредственно задать вопрос в такой форме, то ответ будет простой - нет. Понятно, что для формальной спецификации сказать, что она полна - это утверждать, что она покрывает все необходимые свойства, но это имеет смысл только по отношению к некоторому эталонному документу, в котором все эти свойства перечислены. Тогда мы сталкиваемся с двумя равно неутешительными ситуациями:
Таким образом, в этой тривиальной форме вопрос о полноте неинтересен. Но имеется и более полезное понятие полноты, соответствующее значению этого слова в математической логике. Для математика некоторая теория является полной, если ее аксиомы и правила вывода являются достаточно мощными, чтобы доказать истинность или ложность любой формулы, выразимой в языке данной теории. Хотя такое понятие полноты является более ограниченным, но оно интеллектуально вполне удовлетворительно, поскольку показывает, что если теория позволяет нам выражать некоторое свойство, то она также дает возможность определить имеет ли это свойство место.
Особый интерес с точки зрения полноты представляют выражения-запросы, у которых самая внешняя функция является запросом. Вот примеры таких выражений:
empty (put (put (new, x1), x2)) item (put (put (new, x1), x2)) stackexp
Выражение-запрос задает значение, которое (если оно определено) принадлежит не определяемому АТД, а некоторому другому ранее определенному типу. Так, первое приведенное выше выражение имеет значение типа BOOLEAN, а второе и третье - тип G формального параметра для элементов стека, например если мы рассматриваем АТД STACK [INTEGER], то это будет тип INTEGER.
Выражения-запросы представляют внешние наблюдения, которые можно сделать о результатах некоторого вычисления, использующего экземпляры нового АТД. Если спецификация этого АТД хорошая, то она должна позволить нам установить определены ли эти результаты, и если да, то каковы они. Представляется, что спецификация стека обладает этим свойством, по крайней мере, для трех представленных в примере выражений, поскольку она позволяет установить, что все эти выражения определены, и с помощью аксиом можно получить их значения:
empty (put (put (new, x1), x2)) = False item (put (put (new, x1), x2)) = x2 stackexp = x4
Эти наблюдения, перенесенные на произвольные спецификации АТД, приводят к прагматическому понятию полноты, известному как достаточная полнота, она означает, что спецификация содержит достаточно сильные аксиомы, которые позволяют находить для любого выражения-запроса его результат в виде некоторого простого значения.
Приведем точное определение достаточной полноты. (Не расположенные к математике читатели могут пропустить остаток этого раздела).
Определение: достаточная полнота
Спецификация АТД T является достаточно полной тогда и только тогда, когда аксиомы ее теории позволяют для каждого выражения expr решить следующие задачи:
