/* ESC/Java2 Exercise: 
   
   This class implements a Bag of integers, using an array.

   Add JML specs to this class, to stop ESC/Java2 from complaining.
   NB there are also a couple errors in the code that you have to 
   fix to stop ESC/Java2 from complaining. 

   The only JML keywords needed for this are
      requires
      invariant 
      ensures 
  
   If you want, you can also use
      non_null

   You can sometimes get a useful suggestion from the tool
   by using the -suggest flag, ie.
      escjava2 -suggest Bag.java


   Once ESC/Java2 no longer complains, try to add some interesting 
   postconditions to methods, using the keyword 
     ensures
   and loop invariants, using the keyword
     loop_invariant

*/

class Bag {

  int[] contents;
  int n;

  Bag(int[] input) {
    n = input.length;
    contents = new int[n];
    arraycopy(input, 0, contents, 0, n);
  }

  void removeOnce(int elt) {
    for (int i = 0; i <= n; i++) {  
      if (contents[i] == elt ) {
         n--;
         contents[i] = contents[n];
         return;
      }
    }
  }

  void removeAll(int elt) {
    for (int i = 0; i <= n; i++) {   
      if (contents[i] == elt ) {
         n--;
         contents[i] = contents[n];
      }
    }
  }

  int getCount(int elt) {
    int count = 0;
    for (int i = 0; i <= n; i++) 
      if (contents[i] == elt) count++; 
    return count;
  }

  void add(int elt) {
    if (n == contents.length) {
       int[] new_contents = new int[2*n]; 
       arraycopy(contents, 0, new_contents, 0, n);
       contents = new_contents;
    }
    contents[n]=elt;
    n++;
  }

  void add(Bag b) {
    int[] new_contents = new int[n+b.n];
    arraycopy(contents, 0, new_contents, 0, n);
    arraycopy(b.contents, 0, new_contents, n+1, b.n);
    contents = new_contents; 
  }

  Bag(Bag b) {
    this.add(b);    
  }


  private static void arraycopy(int[] src,
                                int   srcOff,
                                int[] dest,
                                int   destOff,
                                int   length) {
    for( int i=0 ; i<length; i++) {
       dest[destOff+i] = src[srcOff+i];
    }
  }
  
}