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)
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
.