/**
 * Refinement mapping from Bag.spec to Bag.java
 * 
 * Project <A HREF = "http://gloss.di.fc.ul.pt/congu/"> ConGu </A>.
 * 
 * @author Gloss
 * @version $Id: Bag.rfn 1766 2010-09-16 17:03:41Z pc $
 */

refinement<E>

    Element is E

    Bag[Element] is  Bag<E> {
        clear: --> Bag[Element]                         is Bag();
        add: Bag[Element] e:Element --> Bag[Element]    is void add(E e);
        contains: Bag[Element] e:Element                is boolean contains(E e);
        remove: Bag[Element] e:Element --> Bag[Element] is void remove(E e);
        howMany: Bag[Element] e:Element --> int         is int howMany(E e);
        isEmpty: Bag[Element]                           is boolean isEmpty();
    }

end refinement