Выражение аксиом
Из соответствия между АТД функциями и компонентами класса можно вывести соответствие между утверждениями класса и семантическими свойствами АТД.
- Предусловие для специфицированной в АТД функции появляется как предусловие программы, соответствующей данной функции.
- Аксиома, включающая команду, и, возможно, одну или более функций запросов, появится как постусловие соответствующей процедуры.
- Аксиомы, включающие только запросы, появятся как постусловия соответствующих функций или как инвариант. Последнее обычно имеет место, если более чем одна функция включена в аксиому, или, по меньшей мере, один из запросов реализован в виде атрибута.
- Аксиомы, включающие функцию создатель, появятся в постусловии соответствующей процедуры создания.
В этот момент следует вернуться назад и сравнить аксиомы АТД STACK с утверждениями класса STACK4 (включая и те, которые даны для класса STACK2).
