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         /*@ non_null @*/ int[] contents;
  36         int n; //@ invariant n <= contents.length && n >= 0;
  37
  38         Bag(int[] input) {
  39                 if(input == null)
  40                         input = new int[0];
  41                 n = input.length;
  42                 contents = new int[n];
  43                 arraycopy(input, 0, contents, 0, n);
  44         }
  45
  46         Bag() {
  47                 contents = new int[0];
  48                 n = 0;
  49         }
  50         //
  51         // The example below is a bit nasty.
  52         // NB this is a constructor, not a method.
  53         //
  54         Bag(Bag b) {
  55                 //CHANGED: Initialize object with empty bag, then check for
  56                 //         null and then add.
  57                 this();
  58                 if(b == null)
  59                         b = new Bag();
  60                 this.add(b);
  61         }
  62
  63
  64
  65         void removeOnce(int elt) {
  66                 // CHANGED: off by one error
  67                 for (int i = 0; i < n; i++) {
  68                         if (contents[i] == elt ) {
  69                                 n--;
  70                                 contents[i] = contents[n];
  71                                 return;
  72                         }
  73                 }
  74         }
  75
  76         void removeAll(int elt) {
  77                 // CHANGED: off by one error
  78                 for (int i = 0; i < n; i++) {
  79                         if (contents[i] == elt ) {
  80                                 n--;
  81                                 contents[i] = contents[n];
  82                         }
  83                 }
  84         }
  85
  86         int getCount(int elt) {
  87                 int count = 0;
  88                 // CHANGED: off by one error
  89                 for (int i = 0; i < n; i++)
  90                         if (contents[i] == elt) count++;
  91                 return count;
  92         }
  93
  94         /* Warning: you may have a hard time checking the method "add" below.
  95            ESC/Java2 may warn about a very subtle bug that can be hard to spot.
  96            If you cannot find the problem after staring at the code for an hour,
  97            feel free to stop.
  98            */
  99
 100         void add(int elt) {
 101                 //CHANGED: Check that contents may be empty still
 102                 if (contents.length == 0){
 103                         contents = new int[1];
 104                 } else if (n == contents.length) {
 105                         int[] new_contents = new int[2*n];
 106                         arraycopy(contents, 0, new_contents, 0, n);
 107                         contents = new_contents;
 108                 }
 109                 contents[n]=elt;
 110                 n++;
 111         }
 112
 113         void add(Bag b) {
 114                 // CHANGED: add null check
 115                 if(b != null){
 116                         int[] new_contents = new int[n + b.n];
 117                         arraycopy(contents, 0, new_contents, 0, n);
 118                         //CHANGED: off by one error on n
 119                         arraycopy(b.contents, 0, new_contents, n, b.n);
 120                         contents = new_contents;
 121                 }
 122         }
 123
 124         void add(int[] a) {
 125                 this.add(new Bag(a));
 126         }
 127
 128         //@ requires srcOff >= 0 && destOff >= 0 && length >= 0;
 129         //@ requires src != null && dest != null;
 130         //@ requires srcOff + length <= src.length;
 131         //@ requires destOff + length <= dest.length;
 132         private static void arraycopy(int[] src,
 133                         int   srcOff,
 134                         int[] dest,
 135                         int   destOff,
 136                         int   length) {
 137                 for(int i=0 ; i<length; i++) {
 138                         dest[destOff+i] = src[srcOff+i];
 139                 }
 140         }
 141
 142 }