/* 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
2018-10-03: Corrected "putIn" postcondition to use SUM not UNION
2022-04-18: Scala 3 compatibility check, minor comment changes

This case study presents the interface for a family of immutable Scala
implementations 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 an ADT in the family as an
immutable object with a method-chaining functional interface.

Note: See the accompanying documents for a description of the Cookie
Jar problem, bag concept, and specification notation.

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

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.
     A public 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) SUM {| 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

}