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

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

Раздел ПРЕДУСЛОВИЯ (PRECONDITIONS) завершает простую спецификацию абстрактного типа данных STACK. Для удобства ссылок полезно собрать вместе разные компоненты спецификации, приведенные выше. Вот полная спецификация.

Спецификация стеков как АТД

ТИПЫ (TYPES)

[x]. STACK [G]

ФУНКЦИИ (FUNCTIONS)

[x]. put: STACK [G] ? G STACK [G]

[x]. remove: STACK [G] STACK [G]

[x]. item: STACK [G] G

[x]. empty: STACK [G] BOOLEAN

[x]. new: STACK [G]

АКСИОМЫ (AXIOMS)

Для всех x: G, s: STACK [G]

[x]. (A1) item (put (s, x)) = x

[x]. (A2) remove (put (s, x)) = s

[x]. (A3) empty (new)

[x]. (A4) not empty (put (s, x))

ПРЕДУСЛОВИЯ (PRECONDITIONS)

[x]. remove (s: STACK [G]) require not empty (s)

[x]. item (s: STACK [G]) require not empty (s)