UNBOUNDED STACK
Operations
NewStack :
Æ StackPush: Stack
¥ Item Æ StackPop: Stack
Æ StackTop: Stack
Æ ItemIsEmpty: 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