ENGR 692-6 Ruby and Software Development
Fall 2006

2018-10-03: Replace bag UNION by bag SUM

Solution to Homework # 1

---
#4 on page 33 of handout "Abstract Specification Techniques"

structure CookieJar (of CookieType)
interface 
    Create                      -> CookieJar
    IsEmpty(CookieJar)          -> Boolean
    PutIn(CookieJar,CookieType) -> CookieJar
    IsIn(CookieJar,CookieType)  -> Boolean
    Eat(CookieJar,CookieType)   -> CookieJar
  end

axioms for all Cookie1 and Cookie2 in CookieType, Jar in CookieJar, let

    IsEmpty(Create) = True

    IsEmpty(PutIn(Jar,Cookie1) = False

    IsIn(Create,Cookie1) = False

    IsIn(PutIn(Jar,Cookie2),Cookie1) =
        IF Cookie1 = Cookie2 
            THEN True
            ELSE IsIn(Jar,Cookie1)
        END IF
        
    Eat(Create,Cookie1) = Error

    Eat(PutIn(Jar,Cookie2),Cookie1) =
        IF Cookie1 = Cookie2
            THEN Jar
            ELSE PutIn(Eat(Jar,Cookie1),Cookie2)
        END IF

  end
end CookieJar


---
#5 on page 33 of handout "Abstract Specification Techniques"

Notation:
    {| |} 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.

    SUM denotes bag union.  The resulting bag has the total number of
         occurrences of elements from the two bags.
         {| 3, 1, 1, 3 |} SUM {| 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 |}

    Alternatively, we could define INSERT and DELETE operations and use them
        to define PutIn and Eat.

Operations:

    Create(VAR Jar:JarType)
    Pre:   True
    Post:  Jar = {| |}   
    Note:  Creates an empty bag.

    IsEmpty(Var Jar:JarType): Boolean
    Pre:   Jar' <> UNDEFINED
    Post:  IsEmpty = (Jar = {| |}) 
    Note:  Assumes bag is defined. Returns True iff bag is empty.

    PutIn(VAR Jar:JarType, Cookie:CookieType)
    Pre:   Jar' <> UNDEFINED
    Post:  Jar = Jar' SUM {| Cookie |}
    Note:  Assumes bag is defined.  Inserts new Cookie occurrence.

    IsIn(VAR Jar:JarType, Cookie:CookieType): Boolean
    Pre:   Jar' <> UNDEFINED
    Post:  IsIn = (Cookie IN Jar)
    Note:  Assumes bag is defined. Returns True iff Cookie occurs in bag.

    Eat(VAR Jar:JarType, Cookie:CookieType)
    Pre:   IsIn(Jar',Cookie)
    Post:  Jar = Jar' DIFF {| Cookie |}
    Note:  Assumes Cookie occurs in bag.  Removes one occurrence of Cookie.
    Alternative Post:  Jar' = Jar SUM {| Cookie |}