Две или три вещи, которые мы знаем о стеках
Спецификации АТД являются неявными. Имеются два вида 'неявности':
[x]. Метод АТД определяет неявно некоторое множество объектов, задавая применимые к ним функции. Из этого определения никогда не следует, что в нем перечислены все операции; часто, на пути к представлению, будут добавлены и другие.
[x]. Сами функции также определяются неявно. Вместо явных определений используются аксиомы, задающие свойства этих функций. Здесь тоже ничего не утверждается о полноте: когда вы, в конце концов, дойдете до реализации этих функций, они приобретут дополнительные свойства.
Эта неявность является ключевым аспектом абстрактных типов данных и, как следствие, - их будущих аналогов в построении ОО-ПО - классов. Когда мы определяем абстрактный тип данных или класс, мы всегда сообщаем кое-что об этом типе или классе, просто перечисляя те их свойства, которые знаем, и берем их в качестве определения. При этом никогда не предполагается, что других применимых свойств нет.
Неявность также предполагает открытость определений: всегда можно добавить новые свойства АТД или класса. Основным механизмом для выполнения таких расширений без разрушения уже существующего первоначального определения является наследование.
Этот 'неявный' подход имеет далеко идущие последствия. В пункте 'дополнительные темы' в конце этой лекции помещены еще некоторые комментарии о неявности.
Частичные функции
Спецификация всякого реалистичного примера, даже такого простого как стеки, неизбежно сталкивается с проблемами не всюду определенных операций: некоторые операции применимы не ко всем возможным элементам исходных множеств. Например, это имеет место для функций
Решение этой проблемы, использованное в приведенной выше спецификации, состоит в том, чтобы определить эти функции как частичные. Функция из исходного множества
inv(x)= 1/x.
Поскольку
Inv: R R
Чтобы указать, что функция частичная, используется перечеркнутая стрелка
Областью (определения) частичной функции типа
В спецификации АТД
В некоторых случаях функцию
Это будет новым применением частичных функций, отражающим ограничения реализации. В отличие от этого, объявление функций
Предусловия
Частичные функции являются неустранимым фактом процесса проектирования ПО, отражающим очевидное наблюдение: не каждая операция применима ко всем объектам. Но они также являются и потенциальным источником ошибок: если функция
Для этого всякая спецификация АТД, содержащая частичные функции, должна задавать их области. В этом и состоит роль раздела ПРЕДУСЛОВИЯ (PRECONDITIONS). Для АТД
Предусловия (preconditions)
[x].
[x].
В нем у каждой из функций в пункте 'требует' перечисляются условия, которым должны удовлетворять аргументы функции, чтобы входить в ее область.
Булевское выражение, которое определяет область функции, называется предусловием соответствующей частичной функции. В нашем случае предусловия обеих функций
| С точки зрения математики предусловие функции f - это характеристическая функция области f. Характеристической функцией подмножества Aмножества X называется полная функция ch: X |
