/* CookieJar ADT in Scala
   H. Conrad Cunningham
   Version #1:  15 March 2010
   Version #1a: 23 March 2010 Corrected postconditions on putIn & eat, added '

123456789012345678901234567890123456789012345678901234567890123456789012345678

This example presents a Scala implementation of the CookieJar ADT
described in exercises #4 and #5 on page 33 of Nell Dale and Henry
M. Walker's textbook _Abstract Data Types: Specifications,
Implementations, and Applications_ (D.C. Heath and Company, 1996).
These exercises were assigned to the Spring 2010 Software Design and
Scala Programming class.  Drafting code for this ADT was also a
question on Examination 1.

This program is an enhanced Scala version of a Ruby program the author
wrote in Fall 2006.  This version uses a trait to define the ADT and
gives several concrete classes that extend that trait.

MODEL: The model for CookieJar ADT is a mathematical bag.  A bag is an
collection of values in which each value may occur one or more times.

The bag notation used in this documentation includes:

  {| |} denotes empty bag

  {| 2, 3, 2, 1 |} denotes a bag with four elements including two 2's, 
    one 3, and one 1.  The order is not significant!  There may be one
    or more occurrences of an element.

  IN denotes the bag membership operation.  x IN B if there are one or
    more occurrences of the value x in bag B.

   UNION denotes bag union.  The resulting bag has the total number of
     occurrences of elements from the two bags.  {| 3, 1, 1, 3 |} UNION
     {| 1, 2 |] = [| 1,1,1,2,3,3 |} (Remember order is not significant.)

  DIFF denotes bag difference.  A DIFF B removes each occurrence of
    elements in B from A.  The resulting bag has the number of
    occurrence in bag A minus the number of occurrences in bag B.  If
    there are more occurrence in B than A, then the result has no
    occurrences. {| 1, 1, 2, 1 }} DIFF {| 2,1,1 |} = {| 1 |}

  OCCURRENCES denotes occurrence counting.  OCCURENCES(x,B) returns
    the number of times element x appears in bag B.

In postconditions, a variable like Bag' (with a ' appended to the
name) represents the value of the variable before the call.  The
symbol without the ' denotes the value of the variable at the return
from the call.

For some function func, the symbol func_return refers to the returned
value of the function.

*/


/* Trait CookieJar specifies the interface for concrete
   implementations of the CookieJar ADT.

   MODEL: The values of specification variable Bag, which is a
   mathematical bag.

   INTERFACE INVARIANT:  Bag != UNDEFINED

   Note: Remember that an interface invariant must be made true by the
   class constructors and each public method of the class must
   preserve it.  That is, it is both a precondition and postcondition
   on all mutator and accessor methods. An interface invariant refers
   only to the model, not to the data structures of any concrete
   implementation.

*/

trait CookieJar[CookieType] {

  /* The Dale and Walker book defines an operation Create that will be
     implemented as constructors of a class that extends CookieJar.  The
     constructor must satisfy the following specifications.

     PRE:   true
     POST:  Bag == {| |}
  */


  /* Method putIn adds cookie to the cookie jar.  Method putIn is
     called PutIn in the Dale and Walker book.  

     PRE:  true
     POST: Bag == Bag' UNION {| cookie |} 
  */ 

  def putIn(cookie: CookieType)


  /* Method eat removes cookie from the cookie jar.  Method eat is
     called Eat in the Dale and Walker book.

     PRE:  has(cookie) 
     POST: Bag == Bag' DIFF {| cookie |} 
  */ 

  def eat(cookie: CookieType)

      
  /* Method isEmpty returns true iff the bag is empty.  Method isEmpty
     is called IsEmpty in the Dale and Walker book.

     PRE:   true
     POST:  isEmpty_return == ( Bag == {| |} ) 
  */

  def isEmpty: Boolean


  /* Method "has" returns true iff cookie occurs in the cookie jar.
     Method "has" is called IsIn in the Dale and Walker book.

     PRE:   true
     POST:  has_return == (cookie IN Bag)
  */

  def has(cookie: CookieType): Boolean

}