Модификация спецификаций ADT для стеков

Question

Я сделал это самостоятельно, я просто хочу подтверждение, что это правильно. Я должен изменить спецификации ADT для стеков, чтобы учесть операции suck как count (возвращающий количество элементов в стеке), change_top (заменяющий вершину стека заданным элементом) и wipe_out (удаляющий все элементы). Также для включения новых аксиом и предварительных условий по мере необходимости.

Вот что у меня есть:

TYPES

•   STACK[G]


FUNCTIONS
•   put: STACK[G] x G -> STACK[G]
•   remove: STACK[G]-/> STACK[G]
•   item: STACK[G] -/> G
•   empty: STACK[G] -> BOOLEAN
•   new: STACK[G]
•   count: STACK[G] -> INTEGER
•   change_top: STACK[G] x G -> STACK[G]
•   wipe_out: STACK[G]


AXIOMS

For any 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))
•   A5 - count(new)


PRECONDITIONS

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

Answer 1

Разве нет ТА, с которым ты мог бы поговорить?В любом случае, change_top должно быть помечено -/>, поскольку вы дали ему предварительное условие.Должен ли wipe_out принимать аргумент стека?

Аксиома A5 не правильно сформирована, поскольку count возвращает целое число, а не логическое значение.Вам нужна еще одна аксиома для count и аксиомы для change_top и wipe_out.