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

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

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

ТИПЫ (TYPES)

• STACK [G]

ФУНКЦИИ (FUNCTIONS)

• put: STACK [G] x G -> STACK [G]
• 
• 
• empty: STACK [G] -> BOOLEAN
• new: STACK [G]

АКСИОМЫ (AXIOMS)

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

• (A1) item (put (s, x)) = x
• (A2) remove (put (s, x)) = s
• (A3) empty (new)
• (A4) not empty (put (s, x))

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

• remove (s: STACK [G]) require not empty (s)
• item (s: STACK [G]) require not empty (s)