ADT Specifications Modification for Stacks

Question

I did this on my own i just want confirmation that it is right. I am supposed to Modify ADT Specifications for Stacks to account for operations suck as count (returning the number of elements in a stack) , change_top(replacing the top of a stack by a given element) and wipe_out(remove all elements). Also to include new axioms and preconditions as needed.

Here is what i have:

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

Isn't there a TA you could talk to? Anyway, change_top should be marked -/> since you gave it a precondition. Should wipe_out take a stack argument?

Axiom A5 isn't well formed, since count returns an integer, not a boolean. You need another axiom for count, and axioms for change_top and wipe_out.