/* CookieJar ADT, Mutable Object-Oriented Version
   CSci 556: Multiparadigm Programming, Spring 2012
   CSci 555: Functional Programming, Spring 2016
   H. Conrad Cunningham, Professor
   Computer and Information Science
   University of Mississippi

1234567890123456789012345678901234567890123456789012345678901234567890

2010-Spring: Developed from mutable Ruby version
2012-Spring: Minor updates
2016-03-09:  Some cleanup of Scala code and comments
2018-10-03:  Corrected "putIn" precondition to use SUM instead of UNION
2022-04-18:  Scala 3 compatibility check, added Unit to procedures

This example presents a mutable 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).  I
assigned these exercises to the Spring 2010 Software Design and Scala
Programming class.  I also used this example in other classes
including the Spring 2012 CSci 556 Multiparadigm Programming class.

This program is an enhanced Scala version of the mutable,
object-oriented Ruby program the author developed for a class in Fall
2006.  This version uses a Scala trait to define the ADT and specifies
the mutator methods (putIn and eat) as procedure methods. The case
study includes several concrete classes that extend that trait. These
define mutable (stateful) objects.

I developed an alternative immutable implementation for the Spring
2016 offering of CSci 555 Functional Programming (which used Scala).

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. See the related document describing the bag notation.

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

For functions, the symbol Result 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. The notation Bag(obj) denotes the model
          for the object obj.

   INTERFACE INVARIANT:  Bag(this) != 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(this) == {| |}
  */


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

     PRE:  true
     POST: Bag(this) == Bag(this') SUM {| cookie |} 
  */ 

  def putIn(cookie: CookieType):C Unit


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

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

  def eat(cookie: CookieType): Unit

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

     PRE:   true
     POST:  (Result == (Bag(this) == {| |})) &&
            (Bag(this) == Bag(this'))
  */

  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:  (Result == (cookie IN Bag)) && (Bag(this) == Bag(this'))
  */

  def has(cookie: CookieType): Boolean

  /* Classes that implement CookieJar may want to override "toString"
     and/or "equals" appropriately.
  */

}