Links und Funktionen
Sprachumschaltung

Navigationspfad
Sie sind hier: Startseite / Lehre / SS 2014 / Formale Spezifikation und Verifikation / Materialien / Beispiel für ESC Java2 (Bag.java -- mit Annotationen)


Inhaltsbereich

Beispiel für ESC Java2 (Bag.java -- mit Annotationen)

Java source code icon Bag.java — Java source code, 1 KB (1917 bytes)

Dateiinhalt

/* ESC/Java2 Exercise 

   Original source:  http://www.cs.ru.nl/E.Poll/talks/jml_tutorial/Bag.java

*/

class Bag {

  int[] contents;
  int n;  
  //@ invariant contents != null;
  //@ invariant 0 <= n && n <= contents.length;

  //@ requires input != null;
  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 + 1]; 
       arraycopy(contents, 0, new_contents, 0, n);
       contents = new_contents;
    }
    contents[n]=elt;
    n++;
  }

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

  //@ requires b != null;
  Bag(Bag b) {
	  contents = new int[1];
	  n =0;
    this.add(b);    
  }


  /*@ requires src != null && dest != null;
    @ requires 0 <= srcOff && srcOff + length <= src.length;
    @ requires 0 <= destOff && destOff + length <= dest.length;
   */
  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];
    }
  }
  
}

Artikelaktionen


Funktionsleiste