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

значения.

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

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

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

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

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

Содержательно, правило корректного веса утверждает, что стековое выражение корректно тогда и только тогда, когда в нем самом и в каждом из его подвыражений имеется не меньше операций put (вставляющих элементы в стек), чем операций remove (выталкивающих элементы с вершины стека). Если рассмотреть такое выражение как представление некоторого вычисления над стеком, то это означает, что мы никогда не будем пытаться вытолкнуть больше элементов, чем втолкнули. Напомним, что на этом этапе мы сосредоточились на функциях put и remove, оставив в стороне запросы item и empty.

Интуитивно сформулированное правило выглядит верным, но нам следует все же доказать, что оно имеет место. Удобно ввести еще одно вспомогательное правило и одновременно доказывать справедливость обоих этих правил:

Правило нулевого веса

Пусть e - это правильно построенное и корректное стековое выражение, не содержащее item или empty. Тогда empty (e) истинно тогда и только тогда, когда вес e равен 0.

Доказательство использует индукцию по уровню вложенности (максимальному числу вложенных пар скобок) выражения. Для удобства ссылок напомним аксиомы, относящиеся к функции empty:

Аксиомы стека

Для всех x: G, s: STACK [G]

[x]. (A3) empty (new)

[x]. (A4) not empty (put (s, x))

При уровне вложенности 0 (без скобок) выражение e должно совпадать с new, поэтому его вес равен 0 и оно корректно, так как у new нет никаких предусловий. Аксиома A3 утверждает, что empty (new) истинно. Это обеспечивает базис индукции как для правила корректного веса, так и для правила нулевого веса.

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

E1 · e = put (s, x)
E2 · e = remove (s)

где x имеет тип G, а уровень вложенности у s равен n. Пусть ws - это вес s.

В случае E1, поскольку put - всюду определенная функция, e корректно тогда и только тогда, когда s корректно, т. е. (по предположению индукции) тогда и только тогда, когда s и все его подвыражения имеют неотрицательные веса. Но это эквивалентно тому, что e и все его подвыражения имеют неотрицательные веса, что и доказывает правило корректного веса в этом случае. Кроме того, e имеет положительный вес ws+1, и (по аксиоме A4) является непустым, что доказывает правило нулевого веса.

В случае E2 выражение e корректно тогда и только тогда, когда выполняются два следующих условия:

EB1 _ s и все его подвыражения являются корректными.
EB2 _ not empty (s) (это предусловие для функции remove).