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.
40 contents
= new int[n
];
41 arraycopy(input
, 0, contents
, 0, n
);
46 contents
= new int[0];
49 void removeOnce(int elt
) {
50 for (int i
= 0; i
<= n
; i
++) {
51 if (contents
[i
] == elt
) {
53 contents
[i
] = contents
[n
];
59 void removeAll(int elt
) {
60 for (int i
= 0; i
<= n
; i
++) {
61 if (contents
[i
] == elt
) {
63 contents
[i
] = contents
[n
];
68 int getCount(int elt
) {
70 for (int i
= 0; i
<= n
; i
++)
71 if (contents
[i
] == elt
) count
++;
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,
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
;
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
;
102 // The example below is a bit nasty.
103 // NB this is a constructor, not a method.
109 private static void arraycopy(int[] src
,
114 for( int i
=0 ; i
<length
; i
++) {
115 dest
[destOff
+i
] = src
[srcOff
+i
];