public /*@  pure @*/ class BagModel
{
/*@   // the number of instances of element e in this bag (may be 0)
  @   public model int count(int e);
  @
  @   // the total number of instances of all elements in this bag
  @   public model int instances();
  @
  @   // the number of different elements that have some instances in this bag
  @   public model int elements();
  @
  @   // a copy of this bag with n instances of e added
  @   requires n >= 0;
  @   public model BagModel add(int e, int n);
  @
  @   // a copy of this bag with n instances of e removed
  @   // (n may be bigger than the number of instances of e in this bag)
  @   requires n >= 0;
  @   public model BagModel remove(int e, int n);
  @
  @   axiom 
  @     (\forall BagModel b, b2; b != null && b2 != null;
  @       (b.equals(b2) <==> (\forall int e; ; b.count(e) == b2.count(e))));
  @        
  @   axiom 
  @     (\forall BagModel b; b != null;
  @       (\forall int e, n, n0;
  @         n >= 0 && n0 == (n <= b.count(e) ? n : b.count(e));
  @
  @         new BagModel().count(e) == 0 &&
  @         b.add(e, n).count(e)    == b.count(e)+n &&  
  @         b.remove(e, n).count(e) == b.count(e)-n0 &&
  @
  @         b.instances() == (\sum int e0; true; b.count(e0)) &&
  @         b.elements()  == (\num_of int e0; b.count(e0) > 0; true)
  @     ));
  @
  @   axiom // actually implied by above
  @     (\forall BagModel b; b != null;
  @       (\forall int e, n, n0; 
  @         n >= 0 && n0 == (n <= b.count(e) ? n : b.count(e));
  @
  @         new BagModel().instances() == 0 &&
  @         b.add(e, n).instances()    == b.instances()+n &&
  @         b.remove(e, n).instances() == b.instances()-n0 &&
  @
  @         new BagModel().elements() == 0 &&
  @         (b.count(e) == 0 && n > 0 ==> 
  @           b.add(e, n).elements() == b.elements()+1) &&
  @         (b.count(e) > 0 || n == 0 ==>
  @           b.add(e, n).elements() == b.elements()) &&
  @         (n >= b.count(e) ==> 
  @           b.remove(e,n).elements() == b.elements()-1) &&
  @         (n <  b.count(e) ==> 
  @           b.remove(e,n).elements() == b.elements())
  @     ));
  @*/
}