Формализация спецификаций

Формализация спецификаций

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

Приведенные содержательные описания явно недостаточны - put вталкивает элемент на "вершину" стека, remove выталкивает элемент, находящийся на вершине. Нам нужно точно знать, как клиенты могут использовать эти операции и что они для этого должны делать.

Спецификация АТД предоставит эту информацию. Она состоит из четырех разделов, разъясняемых в следующих разделах:

[x]. ТИПЫ

[x]. ФУНКЦИИ

[x]. АКСИОМЫ

[x]. ПРЕДУСЛОВИЯ

Для спецификации АТД в этих разделах будут использоваться простая математическая нотация.

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