Абстрактные типы данных (АТД)
5c8b6e8c

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


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

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

ТИПЫ (TYPES)

  • STACK [G]

    • ФУНКЦИИ (FUNCTIONS)

  • put: STACK [G] × G → STACK [G]

  • remove: STACK [G]
    STACK [G]

  • item: STACK [G]
    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)



    • Содержание раздела