/* 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.

   However, beware that there are also errors in the code that you may
   have to fix to stop ESC/Java2 from complaining. (More generally, 
   feel free to improve the code to make it easier to specify in JML, 
   but _only_ do this if you think this makes the code better/easier 
   to understand.

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


   While developing your specs, it may be useful to use the keywords
      assert
   to add additional assertions in source code, to find out what 
   ESC/Java2 can - or cannot - prove at a given program point.
  
*/

class Bag {

  int[] contents;
  int n;

  /*@ invariant contents != null &&
      0 <= n && n <= contents.length;
@*/

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

  Bag() {
    n = 0;
    contents = new int[0];
  }

  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;
  }  

  /* Warning: you may have a hard time checking the method "add" below.
     ESC/Java2 may warn about a very subtle bug that can be hard to spot. 
     If you cannot find the problem after staring at the code for an hour, 
     feel free to stop.
   */

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

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

  void add(/*@ non_null @*/ int[] a) {
    this.add(new Bag(a));
  }

  Bag(/*@ non_null @*/ Bag b) {
    this();    
    this.add(b);    
  }

    //@requires 0 <= srcOff && srcOff+length <= src.length ;
    //@requires 0 <= destOff && destOff+length <= dest.length ;
    //@requires src != dest;

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