Полна ли моя спецификация?

Полна ли моя спецификация?

Другой вопрос, который может вас тревожить: есть ли какой-нибудь способ убедиться в том, что спецификация описывает все нужные свойства объектов, для которых она предназначена? Студенты, которым требуется написать их первые спецификации (например, проделать упражнения в конце этой лекции), часто приходят с аналогичным вопросом: "Как узнать, что я уже специфицировал достаточно свойств и могу остановиться?"

В более общей форме вопрос звучит так: существует ли метод, позволяющий определять полноту спецификации АТД?

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

[x]. Если эталонный документ является неформальным (например, документом с требованиями на естественном языке или просто текстом упражнения), то отсутствие формальности предотвращает всякую попытку систематической проверки соответствия спецификации всем требованиям, описанным в этом документе.

[x]. Если же эталонный документ является формальным, и мы можем, используя его, проверить полноту нашей спецификации, то это просто отодвигает проблему дальше: как можно убедиться в полноте самого эталонного документа?

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

Как можно перенести эту идею на спецификации АТД? Здесь "язык теории" - это множество правильно построенных выражений, т.е. тех выражений, которые можно построить, используя функции АТД, применяемые к аргументам соответствующих типов. Например, используя спецификацию АТД STACK и считая, что x является правильно построенным выражением типа G, можно указать следующие правильно построенные выражения:

new

put (new, x)

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

empty (put (new, x))

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

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

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

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

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

Поделитесь на страничке

Следующая глава >

Похожие главы из других книг

3.6. Использование предиката присоединить и спецификация деталей

Из книги Программирование на языке Пролог автора Клоксин У.

3.6. Использование предиката присоединить и спецификация деталей Предикат присоединить, обрабатывающий списки, используется для создания нового списка, являющегося результатом соединения двух других списков. Например, верен следующей факт:присоединить([а,b,с], [3,2,1],


Спецификация кэширования

Из книги Разгони свой сайт автора Мациевский Николай

Спецификация кэширования В спецификации RFC-2616 HTTP-кэшированию посвящена целая глава. В ней подробно рассматривается, что означают отдельные заголовки. Давайте остановимся на ключевых моментах.Заголовок Expires устанавливает время актуальности информации. Для ресурсов,


Спецификация

Из книги ИНФОРМАЦИОННАЯ ТЕХНОЛОГИЯ. ПРОГРАММНЫЕ КОНСТРУКТИВЫ И УСЛОВНЫЕ ОБОЗНАЧЕНИЯ ДЛЯ ИХ ПРЕДСТАВЛЕНИЯ автора Госстандарт России

Спецификация Расширения post-check и pre-check для Cache-Control определены следующим образом.post-checkОпределяет интервал времени в секундах, после которого ресурс должен быть проверен на актуальность. Эта проверка может быть выполнена и после того, как пользователь загрузит страницу из


5 СПЕЦИФИКАЦИЯ КОНСТРУКТИВОВ

Из книги Информационная технология ПРОЦЕСС СОЗДАНИЯ ДОКУМЕНТАЦИИ ПОЛЬЗОВАТЕЛЯ ПРОГРАММНОГО СРЕДСТВА автора Автор неизвестен


Н.3 Спецификация указателя

Из книги ПРОГРАММНОЕ ОБЕСПЕЧЕНИЕ ВСТРОЕННЫХ СИСТЕМ. Общие требования к разработке и документированию автора Госстандарт России


R.7.1.3 Спецификация typedef

Из книги автора

R.7.1.3 Спецификация typedef Описания со спецификацией typedef задают идентификаторы, которые позднее могут использоваться для обозначения основных или производных типов. Спецификация typedef недопустима в определении-функции (§R.8.3).имя-typedef: идентификаторВ пределах области


R.7.1.4 Спецификация шаблона типа

Из книги автора

R.7.1.4 Спецификация шаблона типа Спецификация шаблона типа используется для задания семейства типов или функций (см.


R.7.1.5 Спецификация friend

Из книги автора

R.7.1.5 Спецификация friend Спецификация friend используется для задания доступа к членам класса (см.


R.7.1.6 Спецификация типа

Из книги автора

R.7.1.6 Спецификация типа К спецификации типа относятся:спецификация-типа: имя-простого-типа спецификация-класса спецификация-перечисления спецификация-сложного-типа :: имя-класса const volatileПри описании объекта служебные слова const и volatile можно добавить к любой законной


Полная спецификация

Из книги автора

Полная спецификация Раздел ПРЕДУСЛОВИЯ (PRECONDITIONS) завершает простую спецификацию абстрактного типа данных STACK. Для удобства ссылок полезно собрать вместе разные компоненты спецификации, приведенные выше. Вот полная спецификация.Спецификация стеков как АТДТИПЫ (TYPES)[x]. STACK


Спецификация минимальной функциональной совместимости

Из книги автора

Спецификация минимальной функциональной совместимости В 1996 г. институт NIST совместно с рядом поставщиков продуктов, лидирующих на рынке PKI - AT&T, IREBBN, Motorola Certicom, Nortel (Entrust), Cylink, Spyrus, DynCorp и VeriSign, - выступил с инициативой разработки спецификации минимальной функциональной