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

[Z1]

n + 1 n

Пусть теперь n будет результатом запроса верхнего элемента пустого стека, т. е. значением выражения item (new), где new - это пустой стек целых чисел. При этом запросе n должно получить специальное значение w INTEGER . Что же тогда должно быть значением выражения n+1 ? Если у нас в распоряжении имеются в качестве значений только обычные целые числа и w INTEGER , то в качестве ответа мы вынуждены выбрать w INTEGER :

wINTEGER + 1 = wINTEGER.

Это единственный допустимый выбор. Если присвоить w INTEGER+1 любое другое значение, "нормальное" число q , то это означает, что после попытки доступа к вершине пустого стека и получения в качестве результата ошибочного значения мы можем волшебным образом устранить всякую память об этой ошибке, просто прибавив к результату единицу!

Но, при выборе w INTEGER в качестве значения n + 1 при n равном w INTEGER , нарушается указанное выше свойство Z1. В общем случае, выражение w INTEGER+p будет равно w INTEGER для любого p . Это означает, что для измененного типа данных ( INTEGER , дополненные ошибочным элементом) требуется новая система аксиом, объясняющая, что всякая операция над целыми числами возвращает значение w INTEGER , если хоть один из ее аргументов равен w INTEGER . Аналогичные изменения потребуются для каждого типа.

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

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

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

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

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

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

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

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