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.
In computer Science a Stack is an abstract data type with the following operations/functions
|new||creates a new stack that has no items in it.|
|pop||removes the top of the stack|
|push||puts a new item on top of the stack|
|top||returns the top element and leaves the stack unchanged|
|empty||returns true if the stack is empty, otherwise it returns false. In either case the stack is not changed.|
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.
This expression pushes three numbers onto an
Note.... this might be easier to read using infix operations:
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.
We can prove
By induction we can prove that the
|destroy(S)||Implicit. A value returned by a function is used and then destroyed.|
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:
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: [ http://csci.csusb.edu/dick/cs320/stacks/ ]
. . . . . . . . . ( end of section Stack as an Abstract Data Type) <<Contents | End>>