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

Для доказательства достаточной полноты спецификации стека нужно придумать эффективное правило для решения указанных выше задач 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).

По предположению индукции условие EB2 означает, что вес s ws положителен или, что эквивалентно, вес e , равный ws - 1 , является неотрицательным. Следовательно, e удовлетворяет Правилу корректного веса. Чтобы доказать, что оно также удовлетворяет правилу нулевого веса, нужно показать, что e пусто тогда и только тогда, когда его вес равен 0. Так как вес s положителен, то s должно содержать по крайней мере одно вхождение put , которое также входит и в e . Рассмотрим самое внешнее вхождение put в e , это вхождение находится непосредственно внутри remove (так как remove находится на самом внешнем уровне у e ). Это означает, что у e имеется подвыражение (быть может, совпадающее с самим e ) вида

remove (put (stack_expression, g_expression)),

которое по аксиоме A2 можно сократить просто до stack_expression . После выполнения этой замены вес e уменьшится на 2, и получившееся выражение, имеющее то же значение, что и e , удовлетворяет по предположению индукции правилу нулевого веса. Это доказывает утверждение индукции в случае E2.

Это доказательство попутно показывает, что во всяком правильно построенном выражении, не содержащем функций-запросов item и empty , можно устранить все вхождения remove , т.е. получить, применяя всюду, где это возможно, аксиому A2, некоторую каноническую форму, в которую будут входить только put и new . Например, выражение:

put (remove (remove (put (put (remove (put (put (new, x1), x2)), x3), x4))), x5)

имеет то же значение, что и каноническая форма:

put (put (new, x1), x5).

Давайте дадим этому механизму имя и приведем его определение:

Правило канонического сокращения

Всякое правильно построенное и корректное стековое выражение, не содержащее функций-запросов item и empty, имеет эквивалентную каноническую форму, которая не содержит функции remove (т.е. состоит только из функций put и new>). Эта каноническая форма получается путем применения аксиомы стека A2 всегда, пока это возможно.