Abstract Data Type : STACK

Example : abstract stack (functional)

For example, a complete functional-style definition of a stack ADT could use the three operations:

• push: takes a stack state and an arbitrary value, returns a stack state;

• top: takes a stack state, returns a value;

• pop: takes a stack state, returns a stack state;

with the following axioms:

• top(push(s,x)) = x (pushing an item onto a stack leaves it at the top)

• pop(push(s,x)) = s (pop undoes the effect of push)

In a functional-style definition there is no need for a create operation. Indeed, there is no notion of "stack instance". The stack states can be thought of as being potential states of a single stack structure, and two stack states that contain the same values in the same order are considered to be identical states. This view actually mirrors the behavior of some concrete implementations, such as linked lists with hash cons.

Instead of create(), a functional definition of a stack ADT may assume the existence of a special stack state, the empty stack, designated by a special symbol like Λ or "()"; or define a bottom() operation that takes no aguments

and returns this special stack state. Note that the axioms imply that

• push(Λ,x) ≠ Λ

In a functional definition of a stack one does not need an empty predicate: instead, one can test whether a stack is empty by testing whether it is equal to Λ.

Note that these axioms do not define the effect of top(s) or pop(s), unless s is a stack state returned by a push.

Since push leaves the stack non-empty, those two operations are undefined (hence invalid) when s = Λ. On the other hand, the axioms (and the lack of side effects) imply that push(s,x) = push(t,y) if and only if x = y and s = t.

As in some other branches of mathematics, it is customary to assume also that the stack states are only those whose existence can be proved from the axioms in a finite number of steps. In the stack ADT example above, this rule means that every stack is a finite sequence of values, that becomes the empty stack (Λ) after a finite number of pops.

By themselves, the axioms above do not exclude the existence of infinite stacks (that can be poped forever, each time yielding a different state) or circular stacks (that return to the same state after a finite number of pops). In particular, they do not exclude states s such that pop(s) = s or push(s,x) = s for some x. However, since one cannot

obtain such stack states with the given operations, they are assumed "not to exist".

My Profille