pop(push(stk, i)) = stk
top(push(stk, i)) = i
isnew(newstack) = true
isnew(push(stk, i)) = false

top(newstack) = error
pop(newstack) = error

+--------------+------------------------------+
| osservazioni | costruttore di s'            |
+--------------+------------------------------+
|              | newstack | push(s, i)        |
+--------------+----------+-------------------+
| isnew(s')    | TRUE     | FALSE             |
| top(s')      | ERROR    | i                 |
| pop(s')      | ERROR    | s                 |
+--------------+----------+-------------------+

declare q, q':queue; i:item

+--------------+-----------------------------------------------------------+
| osservazioni | costruttore di q'                                         |
+--------------+-----------------------------------------------------------+
|              | newq     | addq(q, i)                                     |
+--------------+----------+------------------------------------------------+
| isnew(q')    | TRUE     | FALSE                                          |
| frontq(q')   | ERROR    | if isnew(q) then i else frontq(q)              |
| deleteq(q')  | ERROR    | if isnew(q) then newq else addq(deleteq(q), i) |
+--------------+----------+------------------------------------------------+

push(s, i) = s'       L'oggetto viene inserito al primo posto shiftando tutti gli altri
pop(s) = s'           Elimina il primo elemento dalla pila
top(s)=i              Restituisce(senza modificare la pila) il primo elemento della pila

pop( push(s,i) ) = s      La pop elimina il primo elemento della pila, cioè quello che è stato appena inserito!
top( push(s,i) ) = i      La top restituisce il primo elemento della pila, cioè quello che è stato appena inserito!

addq(q, i) = q'       L'oggetto viene inserito in ultima posizione, cioe' viene accodato alla coda
deleteq(q) = q'       Viene eliminato l'elemento in prima posizione
frontq(q) = i         Viene restituito l'elemento in prima posizione
isnewq(q) = b         Predica se la coda e' vuota

Se la q e' vuota allora q' avra' solo l'elemento i, altrimenti si evoca frontq su q
frontq( addq(q,i) ) = if isnewq(q) then i else frontq(q)

Se la q e' vuota allora q' avra' solo l'elemento i quindi deleteq cancellera' l'unico elemento, altrimenti bisogna rimuovere il primo elemento di q ed aggiugerli i
deleteq( addq(q,i) ) = if isnew(q) then newq else addq(deleteq(q), i)