4 This class implements a Bag of integers, using an array.
6 Add JML specs to this class, to stop ESC/Java2 from complaining.
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 <.
16 The only JML keywords needed for this are
21 If you want, you can also use
26 While developing your specs, it may be useful to use the keywords
28 to add additional assertions in source code, to find out what
29 ESC/Java2 can - or cannot - prove at a given program point.
35 /*@ non_null @*/ int[] contents
;
36 int n
; //@ invariant n <= contents.length && n >= 0;
42 contents
= new int[n
];
43 arraycopy(input
, 0, contents
, 0, n
);
47 contents
= new int[0];
51 // The example below is a bit nasty.
52 // NB this is a constructor, not a method.
55 //CHANGED: Initialize object with empty bag, then check for
65 void removeOnce(int elt
) {
66 // CHANGED: off by one error
67 for (int i
= 0; i
< n
; i
++) {
68 if (contents
[i
] == elt
) {
70 contents
[i
] = contents
[n
];
76 void removeAll(int elt
) {
77 // CHANGED: off by one error
78 for (int i
= 0; i
< n
; i
++) {
79 if (contents
[i
] == elt
) {
81 contents
[i
] = contents
[n
];
86 int getCount(int elt
) {
88 // CHANGED: off by one error
89 for (int i
= 0; i
< n
; i
++)
90 if (contents
[i
] == elt
) count
++;
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,
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
;
114 // CHANGED: add null check
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
;
125 this.add(new Bag(a
));
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
,
137 for(int i
=0 ; i
<length
; i
++) {
138 dest
[destOff
+i
] = src
[srcOff
+i
];