Доказательство достаточной полноты

(Этот раздел и остаток этой лекции содержат дополнительный материал и их результаты не нужны для остальной части книги).

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

Несмотря на это, часто удается доказать достаточную полноту и непротиворечивость конкретной спецификации АТД. Чтобы удовлетворить любопытство читателей-любителей математики, в заключение этой лекции мы приведем доказательство того, что спецификация STACK на самом деле является достаточно полной. Доказательство ее непротиворечивости будет оставлено в качестве упражнения.

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

[x]. (S1) Определить, является ли e корректным.

[x]. (S2) Если в пункте S1 установлена корректность e и его внешними функциями являются item или empty (т.е. функции-запросы), то представить значение e с помощью значений типов BOOLEAN и G без ссылок на значения типа STACK [G] или на функции из спецификации STACK.

Для начала мы рассмотрим только правильно построенные выражения, не включающие ни одну из двух функций-запросов item и empty, т. е. выражения, построенные только из функций new, put и remove. Таким образом, на этом этапе нас будет интересовать лишь задача S1 (установить определено ли выражение). Функции-запросы и S2 будут рассмотрены далее.

Правило для решения задачи S1 задается следующим свойством: