堆栈的ADT规范修改

Question

我自己做的，我只是想确认它是正确的。我应该修改堆栈的 ADT 规范，以解决计数（返回堆栈中的元素数量）、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

没有可以聊的TA吗？无论如何， change_top 应该标记为 -/> 因为你给了它一个前提条件。 wipe_out 应该采用堆栈参数吗？

Axiom A5 的格式不正确，因为 count 返回一个整数，而不是布尔值。您需要另一个用于 count 的公理，以及用于 change_top 和 wipe_out 的公理。