Основы объектно-ориентированного программирования

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

Пункт S2 оптимистически говорит об одном значении expr, а что, если аксиомы приводят к двум или более значениям? Это сделало бы спецификацию бесполезной. Чтобы устранить такую ситуацию нам нужно еще одно свойство, называемое в математической логике непротиворечивостью:

Определение: непротиворечивость АТД

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

Эти два свойства являются взаимно дополнительными. Нам хотелось бы для каждого выражения-запроса выводить ровно одно значение: хотя бы одно (достаточная полнота), но не более одного (непротиворечивость).

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

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

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

Несмотря на это, часто удается доказать достаточную полноту и непротиворечивость конкретной спецификации АТД. Чтобы удовлетворить любопытство читателей-любителей математики, в заключение этой лекции мы приведем доказательство того, что спецификация 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 задается следующим свойством:

Правило корректного веса

Правильно построенное стековое выражение e, не содержащее ни item, ни empty, является корректным тогда и только тогда, когда его вес неотрицателен и каждое его подвыражение является (по индукции) корректным.

Здесь "вес" выражения представляет число элементов в соответствующем стеке, это значение также совпадает с разностью между числом вложенных вхождений функций put и remove. Приведем точное определение этого понятия:

Определение: вес

Вес правильно построенного стекового выражения, не содержащего ни item, ни empty, определяется по индукции следующим образом:

[x]. (W1) Вес выражения new равен 0.

[x]. (W2) Вес выражения put (s, x) равен ws + 1, где ws - это вес s.

[x]. (W3) Вес выражения remove (s) равен ws- 1, где ws - это вес s.