Альтернативы частичным функциям

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

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

Каждый тип T дополняется значением " ошибка". Обозначим его через wT. Тогда для всякой функции f сигнатура

f:... Типы входов... T

определяет, что всякое применение f к объекту, для которого соответствующее вычисление не может быть выполнено, выдаст значение wT.

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

Предположим, например, что рассматриваются стеки целых чисел - экземпляры типа STACK [INTEGER], где INTEGER - это АТД, экземпляры которого - целые числа. Хотя для нашего примера не требуется полностью выписывать спецификацию INTEGER, этот АТД должен моделировать основные операции (сложение, вычитание, " меньше чем" и т. п.), определенные на математическом множестве целых чисел. Аксиомы этого АТД должны выражать обычные свойства целых чисел. Вот одно из таких типичных свойств: для всякого целого n:

[Z1]

n + 1 n

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

wINTEGER + 1 = wINTEGER.

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

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

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

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

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

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

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

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

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

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

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

New