ADT規格修改爲堆棧

Question

我做了我自己的我只是想確認它是正確的。我應該修改堆棧的ADT規範，以解釋count爲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

是不是有一個TA，你可以跟？無論如何，change_top應該標記爲-/>，因爲您已給它一個先決條件。​​應該採用堆棧參數嗎？

公理A5形式不正確，因爲count返回一個整數，而不是布爾值。你需要另一個公理count，以及change_top和​​的公理。