The first version of the module represents the CandyBowl ADT with a
hash table that maps candyTypes to the count of the pieces of that
type.  In addition, special key SIZE maps to the count of the total
number of pieces in the table.

An ADT Implementation Invariant for CandyBowl "bowl" can be stated
 
  (ForAll c: validCandyType(c) :: 
      if bowl[c] ~= nil then bowl[c] == howMany(bowl,c))
      else howMany(bowl,c) = 0)  and
  bowl[SIZE] == howMany(bowl) 

where validCandyType(c) == (c ~= nil and c ~= SIZE), for all c.


---


INVARIANTS FOR CandyBowl INSTANCES

This version of the CandyBowl ADT module has the same interface as the
hashed version but uses a different internal data representation.
This version uses with an unsorted, list-style table of candyTypes.

The interface invariants, preconditions, and postconditions are the
same as those specified in the hashed version of the module.  The
implementation variant changes to match the concrete data
representation uses.

An ADT Interface Invariant for CandyBowl "bowl" can be stated as

      (ForAll c: validCandyType(c) :: howMany(bowl,c) >= 0)
  and (Sum c,n: n == howMany(bowl,c) :: n) == howMany(bowl)

where validCandyType(c) has an appropriate definition.

An ADT Implementation Invariant for CandyBowl "bowl" using the
list-based representation can be stated as
 
  (ForAll i : 1 <= i <= #bowl :: validCandyType(bowl[i]))  and
  (ForAll c : validCandyType(c) ::
    howMany(bowl,c) == (Sum i : 1 <= i < #bowl and bowl[i] == c :: 1))

where validCandyType(c) == (c ~= nil).

We also need to refine the model as discussed in the section BETTER
APPROACH TO SEMANTICS in the hashed version of CandyBowl.

As currently implemented, all the required functions except "isEmpty"
are dependent upon the implementation.  Extended functions "putcp",
"takecp", "toBowl", and "combine2" are not.

For some function, the problem does not specify whether a function can
modify its input arguments.