Stackexp - ранее определенное сложное выражение

Empty (put (new, x))

Item (new) - если это кажется странным, то см. комментарии ниже.

Put (new, x)

New

Однако выражения put (x) и put (x, new) не являются правильно построенными, так как они не соответствуют правилу: put всегда должно иметь два аргумента - первый типа STACK [G] и второй типа G.

Третий пример в рамке item (new) не задает никакого осмысленного вычисления, поскольку аргумент new не удовлетворяет предусловию для item. Хотя это выражение и правильно построено, оно не является корректным. Вот точное определение этого понятия.

Определение: корректное выражение АТД

Пусть f(x1,..., xn) - правильно построенное выражение, содержащее одну или более функций некоторого АТД. Это выражение является корректным тогда и только тогда, когда все его аргументы xi являются (по рекурсии) корректными и их значения удовлетворяют предусловию f, если оно имеется.

Не следует путать "корректное" и "правильно построенное". "Правильно построенное" - это структурное свойство, указывающее на то, что функции, входящие в выражение, имеют правильное число аргументов соответствующих типов, а корректность, которой могут обладать лишь правильно построенные выражения, означает, что данное выражение задает осмысленное вычисление. Как мы видели, выражение put (x) не является правильно построенным (и поэтому бессмысленно спрашивать, корректно ли оно), а выражение item (new) правильно построено, но некорректно.

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

Особый интерес с точки зрения полноты представляют выражения-запросы, у которых самая внешняя функция является запросом. Вот примеры таких выражений:

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 решить следующие задачи:

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

[x]. (S2) Если expr - выражение-запрос и в пункте S1 установлена его корректность, то представить значение expr в виде, не включающем никаких значений типа T.

В S2 выражение expr имеет вид f(x1,..., xn), где f - функция вида запрос такая, как empty и item для стеков. S1 говорит о том, что у expr есть значение, но этого недостаточно, нам хотелось бы знать, каково это значение, представленное в терминах значений других типов (в примере со стеком это значения типов BOOLEAN и G). Если аксиомы настолько сильны, что всегда позволяют ответить на этот вопрос, то спецификация является достаточно полной.

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

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

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

Дата добавления: 2014-01-07