jml_esc/Bag.java

   1
   2 /* ESC/Java2 Exercise:
   3
   4    This class implements a Bag of integers, using an array.
   5
   6    Add JML specs to this class, to stop ESC/Java2 from complaining.
   7
   8    NB there may be errors in the code that you have to fix to stop
   9    ESC/Java2 from complaining, as these complaints of ESC/Java2
  10    point to real bugs in the code. But keep changes to the code to
  11    a minimum of what is strictly needed.
  12    Mark any changes you have made in the code with a comment,
  13    eg to indicate that you replaced <= by <.
  14
  15
  16    The only JML keywords needed for this are
  17       requires
  18       invariant
  19       ensures
  20
  21    If you want, you can also use
  22       non_null
  23    as abbreviation.
  24
  25
  26    While developing your specs, it may be useful to use the keywords
  27       assert
  28    to add additional assertions in source code, to find out what
  29    ESC/Java2 can - or cannot - prove at a given program point.
  30
  31 */
  32
  33 class Bag {
  34
  35   int[] contents;
  36   int n;
  37
  38   Bag(int[] input) {
  39     n = input.length;
  40     contents = new int[n];
  41     arraycopy(input, 0, contents, 0, n);
  42   }
  43
  44   Bag() {
  45     n =0;
  46     contents = new int[0];
  47   }
  48
  49   void removeOnce(int elt) {
  50     for (int i = 0; i <= n; i++) {
  51       if (contents[i] == elt ) {
  52          n--;
  53          contents[i] = contents[n];
  54          return;
  55       }
  56     }
  57   }
  58
  59   void removeAll(int elt) {
  60     for (int i = 0; i <= n; i++) {
  61       if (contents[i] == elt ) {
  62          n--;
  63          contents[i] = contents[n];
  64       }
  65     }
  66   }
  67
  68   int getCount(int elt) {
  69     int count = 0;
  70     for (int i = 0; i <= n; i++)
  71       if (contents[i] == elt) count++;
  72     return count;
  73   }
  74
  75   /* Warning: you may have a hard time checking the method "add" below.
  76      ESC/Java2 may warn about a very subtle bug that can be hard to spot.
  77      If you cannot find the problem after staring at the code for an hour,
  78      feel free to stop.
  79    */
  80
  81   void add(int elt) {
  82     if (n == contents.length) {
  83        int[] new_contents = new int[2*n];
  84        arraycopy(contents, 0, new_contents, 0, n);
  85        contents = new_contents;
  86     }
  87     contents[n]=elt;
  88     n++;
  89   }
  90
  91   void add(Bag b) {
  92     int[] new_contents = new int[n + b.n];
  93     arraycopy(contents, 0, new_contents, 0, n);
  94     arraycopy(b.contents, 0, new_contents, n+1, b.n);
  95     contents = new_contents;
  96   }
  97
  98   void add(int[] a) {
  99     this.add(new Bag(a));
 100   }
 101
 102   // The example below is a bit nasty.
 103   // NB this is a constructor, not a method.
 104   //
 105   // Bag(Bag b) {
 106   //   this.add(b);
 107   // }
 108
 109   private static void arraycopy(int[] src,
 110                                 int   srcOff,
 111                                 int[] dest,
 112                                 int   destOff,
 113                                 int   length) {
 114     for( int i=0 ; i<length; i++) {
 115        dest[destOff+i] = src[srcOff+i];
 116     }
 117   }
 118
 119 }