Выражение аксиом

Выражение аксиом

Из соответствия между АТД функциями и компонентами класса можно вывести соответствие между утверждениями класса и семантическими свойствами АТД.

[x]. Предусловие для специфицированной в АТД функции появляется как предусловие программы, соответствующей данной функции.

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

[x]. Аксиомы, включающие только запросы, появятся как постусловия соответствующих функций или как инвариант. Последнее обычно имеет место, если более чем одна функция включена в аксиому, или, по меньшей мере, один из запросов реализован в виде атрибута.

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

В этот момент следует вернуться назад и сравнить аксиомы АТД STACK с утверждениями класса STACK4 (включая и те, которые даны для класса STACK2).