- Stack as an Abstract Data Type
- : Values
- : Interface
- : Example
- : Specification
- : Consequences
- : Relation to stacks in Sebesta
- : Implementations

- STACK::=following,

Net- 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

The operations are expressed as mathematical functions as follows:Name Description 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. - 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

- (above)|-data in a stack stays there until it is popped out.
Also
- (above)|-the data is stored and retrieved Last_In_First_Out(LIFO)
## Relation to stacks in Sebesta

Sebesta Math Operations Functions empty(S) empty(S) top(S) top(S) create(S) Afterwards S'=new. push(S,E) Afterwards S'=push(S,E). pop(S) Afterwards S'=pop(S). destroy(S) Implicit. A value returned by a function is used and then destroyed. ## 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:

example.push();

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/ ]

## 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.

(End of Net)

. . . . . . . . . ( end of section Stack as an Abstract Data Type) <<Contents | End>>