Stack as an Abstract Data Type

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

   1. Item::Sets=given, Set of items.
   2. Stack::Sets=goal, Set of stacks.

      Interface

      In computer Science a Stack is an abstract data type with the following operations/functions

      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.

      The operations are expressed as mathematical functions as follows:
   3. new:: Stack, --new returns a new empty stack
   4. pop:: Stack <>->Stack, --pop(S) returns S with out its head
   5. push:: (Stack >< Item) ->Stack, --push(S,i) returns S with i on top
   6. top:: Stack <>->Item, --top(S) is a copy of the top of S
   7. 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:
   8. example::=push(push(push(new, 1), 2), 3).

      Note.... this might be easier to read using infix operations:

   9. 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.
      
   10. |- (empty_new): empty(new) is true.
       
   11. |- (empty_push): empty(push(S,i)) is always false.
       
   12. |- (pop_push): pop(push(s,i))=s.
       
   13. |- (top_push): top(push(x,i)=i.

       Consequences

       We can prove
       
   14. (top_push)|-top(example) = 3.
       
   15. (pop_push, top_push)|-top(pop(example)) = 2.
       
   16. (pop_push, pop_push, top_push)|-top(pop(pop(example))) = 1.
       
   17. (pop_push, pop_push, pop_push, empty_new)|-empty(pop(pop(pop(example)))) = true.

       By induction we can prove that the
       

   18. (above)|-data in a stack stays there until it is popped out. Also
       
   19. (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/ ]

   
   (End of Net)
   
   

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