UNBOUNDED STACK

 

 

Operations

NewStack : Æ Stack

Push: Stack ¥ Item Æ Stack

Pop: Stack Æ Stack

Top: Stack Æ Item

IsEmpty: Stack Æ Boolean

 

 

Equations s: Stack; i: Item

Pop(NewStack) = Error*

Pop(Push(s, i)) = s

Top(NewStack) = Error+

Top(Push(s, i)) = i

IsEmpty(NewStack) = true

IsEmpty(Push(s, i)) = false

 

* alternatively: Pop(NewStack) = NewStack

+ alternatively: Top(Newstack) = Null_Item