.Open Stack as an Abstract Data Type
STACK::=following,
.Net
. Values
A stack is an object that stores a sequence of zero or more items.
The type of the stack is determined by the type of the item in sthe stack.
Symbolize the set of stacks by the word `Stack` and the set of
items by the word `Item`.
Item::Sets=given, `Set of items`.
Stack::Sets=goal, `Set of stacks`.
. Interface
In computer Science a Stack is an abstract data type with the following operations/functions
.Table Name Description
.Row new creates a new stack that has no items in it.
.Row pop removes the top of the stack
.Row push puts a new item on top of the stack
.Row top returns the top element and leaves the stack unchanged
.Row empty returns true if the stack is empty, otherwise it returns false. In either case the stack is not changed.
.Close.Table
The operations are expressed as mathematical functions as follows:
new:: Stack, --`new returns a new empty stack`
pop:: Stack <>->Stack, --`pop(S) returns S with out its head`
push:: (Stack >< Item) ->Stack, --`push(S,i) returns S with i on top`
top:: Stack <>->Item, --`top(S) is a copy of the top of S`
empty:: Stack ->Boolean. --`empty(S) is true iff S is empty`
The '<>->' arrow indicates that top and empty are partial functions.
In fact, pop(S) and top(S) are not defined when empty(S) is true.
. Example
This expression pushes three numbers onto an
empty stack:
example ::=push(push(push(new, 1), 2), 3).
Note.... this might be easier to read using infix operations:
new push 1 push 2 push 3.
. Specification
These are mathematical functions and so simpler to reason about than
computer instructions/procedures. All we need are the assumptions
that specify the properties of these operations, and we can reason
about them. More importantly we can use the following rules
to varify any code that claims to implement a stack.
|- (empty_new): empty(new) is true.
|- (empty_push): empty(push(S,i)) is always false.
|- (pop_push): pop(push(s,i))=s.
|- (top_push): top(push(x,i)=i.
. Consequences
We can prove
(top_push)|-top($example) = 3.
(pop_push, top_push)|-top(pop($example)) = 2.
(pop_push, pop_push, top_push)|-top(pop(pop($example))) = 1.
(pop_push, pop_push, pop_push, empty_new)|-empty(pop(pop(pop($example)))) = true.
By induction we can prove that the
()|- data in a stack stays there until it is popped out.
Also
()|- the data is stored and retrieved Last_In_First_Out(LIFO)
. Relation to stacks in Sebesta
.Table Sebesta Math
.Row Operations Functions
.Row empty(S) empty(S)
.Row top(S) top(S)
.Row create(S) Afterwards S'=new.
.Row push(S,E) Afterwards S'=push(S,E).
.Row pop(S) Afterwards S'=pop(S).
.Row destroy(S) Implicit. A value returned by a function is used and then destroyed.
.Close.Table
. Implementations
There are many ways of implementing the physical data structure that
hold the items in a stack. Different languages will implement the
functions as functions, procedures, messages, and predicates.
In some languages 'new' has to be given a different name because
'new' is a reserved name in those languages (C++, Ada,...).
In object-based languages the first argument (the stack) does not appear in the function/operation
declarations. Usually '.' is used to apply the operation to a particular stack:
.As_is example.push();
.As_is if( ! example.empty() ) example.pop();
In some languages it is easy to define a single stack with all the right operations, but
much harder to provide a means of creating a whole class of stacks.
Examples:
.See http://www/dick/cs320/stacks/
.Close.Net
.Close Stack as an Abstract Data Type