/* ICookieJar ADT Interface, Immutable Method-Chaining Functions
   CSci 555: Functional Programming, Spring 2016
   H. Conrad Cunningham, Professor
   Computer and Information Science
   University of Mississippi

1234567890123456789012345678901234567890123456789012345678901234567890

2016-03-22: Developed immutable Scala versions from 2010-12
            mutable Scala versions

This case study presents an immutable Scala implementation of the
CookieJar abstract data type (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 adapted this version from my mutable 2010 and
2012 Scala versions, which, in turn, I had adapted from my mutable
2006 Ruby version.

This version uses a Scala trait to define the ADT as an immutable
object with a method-chaining functional interface.

See the accompanying document that describes the Cookie Jar problem

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

See the accompanying document describing the bag concept.

In the specification, the name "this" refers to the current instance
and "Result" refers to the returned value of the function. A variable
marked with a prime ' is the value before a method executes and one
marked without a prime is the value afterward.

*/


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

   MODEL: The state of each ICookieJar instance jar is specified by an
          abstract variable Bag(jar), a mathematical bag. 

   INTERFACE INVARIANT:  Bag(this) != UNDEFINED

   Note: An invariant must apply to all instances of a data
   type--those passed as explicit or implicit arguments to methods
   (functions and procedures), created by constructors, or returned by
   mutator or accessor functions.  It must be made true by the data
   type (class) constructors and each public accessor or mutator
   function (method ) must preserve it. 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 ICookieJar[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(Result) == Bag(this) UNION {| cookie |}
           && Bag(this) == Bag(this')
  */ 

  def putIn(cookie: CookieType): ICookieJar[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(Result) == Bag(this) DIFF {| cookie |}
           && Bag(this) == Bag(this')
  */ 

  def eat(cookie: CookieType): ICookieJar[CookieType]

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

  def has(cookie: CookieType): Boolean

}