(a) Bounded Stack ADT

  BSTACK OPERATORS:

  new: -> BSTACK 
 push: BSTACK X INT -> BSTACK 
  pop: BSTACK -> BSTACK 
  top: BSTACK -> INT
 size: BSTACK -> INT

A stack is empty if size(BSTACK)==0.

Canonical constructors (minimum subset of operators that return 
a BSTACK that are necessary to construct all possible stacks):

  new(), push(BSTACK,INT)

Using Guttag Heuristic, we form axioms by using canonical 
constructors as arguments for remaining operators:

             pop(new()) = new()
   pop(push(BSTACK,INT)) = ite( size(BSTACK )==max, pop(BSTACK), BSTACK )
             top(new()) = ERROR, NO VALUES ON STACK
   top(push(BSTACK,INT)) = ite( size(BSTACK )==max, top(BSTACK), INT )
            size(new()) = 0
  size(push(BSTACK,INT)) = ite( size(BSTACK )==max, size(BSTACK), size(BSTACK)+1 )
  

(b) DT Induction to prove the following property of Bounded Stack ADT:

  forall B in BSTACK: 0 <= sizeof(B) <= max

  in other words, for all bounded stacks prove that the number of elements in
  the stack must be within [0,max].

  DT INDUCTION:

  Divide the set of axioms into three groups: f (functions that
  return type BSTACK, but do not contain arguments of type BSTACK), g (functions
  that return type BSTACK, and do contain arguments of type BSTACK), and h
  (all remaining functions).

  f = { new() }
  g = { push(), pop() }
  h = { top(), size() }

  P(B) is the boolean property we are trying to prove for a particular 
  instance B of BSTACK:

    P(B) = forall B in BSTACK: 0 <= sizeof(B) <= max

  SHOW BASE CASE IS TRUE:

    P(f) is TRUE.
    P(new()) = for all new() in BSTACK: 0 <= sizeof(new()) <= max
             = for all new() in BSTACK: 0 <= 0 <= max  // SIZE OF NEW STACK IS ZERO
             = TRUE

  INDUCTIVE HYPOTHESIS: ASSUME P(B) IS VALID:

    P(B) = forall B in BSTACK: 0 <= sizeof(B) <= max
         = TRUE

  SHOW THAT BASE CASE AND INDUCTIVE HYPOTHESIS IMPLIED P(g(B)) IS VALID:

    P(push(B,I)) = for all push(B,I) in BSTACK: 0 <= sizeof(push(B,I)) <= max

      By inductive hypothesis, sizeof(B) is in [0,max]. sizeof(push(B,I)) can only
      be sizeof(B)+1 or max depending respectively on whether I was added 
      sucessfully or if I was not added because stack was full. 
      A full stack implies that sizeof(B)=max and sizeof(B) did not increase 
      because the push failed.

      1st case: sizeof(B) != max, so sizeof(B) is in [0,max-1], so after push,
                sizeof(B)+1 is still in [0,max].
      2nd case: sizeof(B) == max, so sizeof(B) is in [0,max] and the size
                is not incremented since the push fails on a full stack.
      
      Both cases are TRUE, so P(push(B,I)) is TRUE.

    P(pop(B)) = for all pop(B) in BSTACK: 0 <= sizeof(pop(B)) <= max

      By inductive hypothesis, sizeof(B) is in [0,max]. sizeof(pop(B)) can only be
      sizeof(B)-1 or 0 depending respectively on whether stack was not empty
      and top element was removed or if stack was empty and the size is zero
      and there is no element to remove.

      1st case: sizeof(B) > 0, sizeof(B) is in [1,max], so after pop,
                sizof(B)-1 is in [0,max].
      2nd case: sizeof(B) == 0, sizeof(B) is in [0,max], so after pop,
                0 is in [0,max].

      Both cases are TRUE, so P(pop(B)) is TRUE.

  BY DT INDUCTION, we can conclude that P(x)=TRUE for all B in BSTACK