Skip to main contentCal State San Bernardino / [CNS] / [Comp Sci Dept] / [R J Botting] /[CS320 Course Materials] [Text Version] stacks/stack.html Tue Jun 19 10:05:09 PDT 2007

Contents


    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
        NameDescription
        newcreates a new stack that has no items in it.
        popremoves the top of the stack
        pushputs a new item on top of the stack
        topreturns the top element and leaves the stack unchanged
        emptyreturns 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

        SebestaMath
        OperationsFunctions
        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>>

End