CSci 450-01: Organization of Programming Languages
CSci 503-01: Fundamental Concepts in Languages
Fall 2014

Carrie's Candy Bowl Data Representations

Hashed Version

The first version of the module represents the CandyBowl ADT with a hash table that maps candyType keys 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 as

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

List Version

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

An ADT Implementation Invariant for CandyBowl bowl 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).