/* ESC/Java2 Exercise:
-
+
This class implements a Bag of integers, using an array.
Add JML specs to this class, to stop ESC/Java2 from complaining.
The only JML keywords needed for this are
- requires
- invariant
- ensures
-
+ requires
+ invariant
+ ensures
+
If you want, you can also use
- non_null
+ non_null
as abbreviation.
While developing your specs, it may be useful to use the keywords
- assert
+ assert
to add additional assertions in source code, to find out what
ESC/Java2 can - or cannot - prove at a given program point.
-
+
*/
class Bag {
- int[] contents;
- int n;
-
- Bag(int[] input) {
- n = input.length;
- contents = new int[n];
- arraycopy(input, 0, contents, 0, n);
- }
-
- Bag() {
- n =0;
- contents = new int[0];
- }
-
- 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;
- }
-
- /* Warning: you may have a hard time checking the method "add" below.
- ESC/Java2 may warn about a very subtle bug that can be hard to spot.
- If you cannot find the problem after staring at the code for an hour,
- feel free to stop.
- */
-
- void add(int elt) {
- if (n == contents.length) {
- int[] new_contents = new int[2*n];
- arraycopy(contents, 0, new_contents, 0, n);
- contents = new_contents;
- }
- contents[n]=elt;
- n++;
- }
-
- void add(Bag b) {
- int[] new_contents = new int[n + b.n];
- arraycopy(contents, 0, new_contents, 0, n);
- arraycopy(b.contents, 0, new_contents, n+1, b.n);
- contents = new_contents;
- }
-
- void add(int[] a) {
- this.add(new Bag(a));
- }
-
- // The example below is a bit nasty.
- // NB this is a constructor, not a method.
- //
- // Bag(Bag b) {
- // this.add(b);
- // }
-
- 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];
- }
- }
-
+ /*@ non_null @*/ int[] contents;
+ int n; //@ invariant n <= contents.length && n >= 0;
+
+ Bag(int[] input) {
+ if(input == null)
+ input = new int[0];
+ n = input.length;
+ contents = new int[n];
+ arraycopy(input, 0, contents, 0, n);
+ }
+
+ Bag() {
+ contents = new int[0];
+ n = 0;
+ }
+ //
+ // The example below is a bit nasty.
+ // NB this is a constructor, not a method.
+ //
+ Bag(Bag b) {
+ //CHANGED: Initialize object with empty bag, then check for
+ // null and then add.
+ this();
+ if(b == null)
+ b = new Bag();
+ this.add(b);
+ }
+
+
+
+ void removeOnce(int elt) {
+ // CHANGED: off by one error
+ for (int i = 0; i < n; i++) {
+ if (contents[i] == elt ) {
+ n--;
+ contents[i] = contents[n];
+ return;
+ }
+ }
+ }
+
+ void removeAll(int elt) {
+ // CHANGED: off by one error
+ for (int i = 0; i < n; i++) {
+ if (contents[i] == elt ) {
+ n--;
+ contents[i] = contents[n];
+ }
+ }
+ }
+
+ int getCount(int elt) {
+ int count = 0;
+ // CHANGED: off by one error
+ for (int i = 0; i < n; i++)
+ if (contents[i] == elt) count++;
+ return count;
+ }
+
+ /* Warning: you may have a hard time checking the method "add" below.
+ ESC/Java2 may warn about a very subtle bug that can be hard to spot.
+ If you cannot find the problem after staring at the code for an hour,
+ feel free to stop.
+ */
+
+ void add(int elt) {
+ //CHANGED: Check that contents may be empty still
+ if (contents.length == 0){
+ contents = new int[1];
+ } else if (n == contents.length) {
+ int[] new_contents = new int[2*n];
+ arraycopy(contents, 0, new_contents, 0, n);
+ contents = new_contents;
+ }
+ contents[n]=elt;
+ n++;
+ }
+
+ void add(Bag b) {
+ // CHANGED: add null check
+ if(b != null){
+ int[] new_contents = new int[n + b.n];
+ arraycopy(contents, 0, new_contents, 0, n);
+ //CHANGED: off by one error on n
+ arraycopy(b.contents, 0, new_contents, n, b.n);
+ contents = new_contents;
+ }
+ }
+
+ void add(int[] a) {
+ this.add(new Bag(a));
+ }
+
+ //@ requires srcOff >= 0 && destOff >= 0 && length >= 0;
+ //@ requires src != null && dest != null;
+ //@ requires srcOff + length <= src.length;
+ //@ requires 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];
+ }
+ }
+
}
repositories / ss1617.git / blobdiff