ADT Spécifications Modification pour les piles

Question

Je l'ai fait moi-même je veux juste la confirmation que c'est juste. Je suis supposé modifier les spécifications ADT pour les piles pour tenir compte des opérations sucées comme count (renvoyant le nombre d'éléments dans une pile), change_top (remplaçant le haut d'une pile par un élément donné) et wipe_out (supprime tous les éléments). Également inclure de nouveaux axiomes et des conditions préalables au besoin.

Voici ce que j'ai:

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

est-il pas un TA vous pourriez parler? Quoi qu'il en soit, change_top devrait être marqué -/> puisque vous lui avez donné une condition préalable. Est-ce que wipe_out doit prendre un argument de pile?

Axiom A5 n'est pas bien formé, car count renvoie un entier et non un booléen. Vous avez besoin d'un autre axiome pour count, et des axiomes pour change_top et wipe_out.