01: package U2.T2.examples;
02:
03: /**
04: * This class maintains an internal array of size 10. The class
05: * invariant requires that all elements of the array should be
06: * non-negative. The class contains errors.
07: */
08: public class TestArray1 {
09:
10: private int[] a;
11:
12: /**
13: * Create an array of size 10, all elements initialized to 0.
14: */
15: public TestArray1() {
16: a = new int[10];
17: for (int i = 0; i < 10; i++)
18: a[i] = 0;
19: }
20:
21: /**
22: * Specifying that the elements of the internal array should be
23: * non-negative.
24: */
25: public boolean classinv() {
26: boolean ok = true;
27: for (int i = 0; i < 10 && ok; i++)
28: ok = a[i] >= 0;
29: return ok;
30: }
31:
32: /**
33: * Increases this array with the values given in b. This method
34: * has errors. Firstly it doesn't check that b size is at least
35: * 10. T2 should be able to find this error. Secondly, if b
36: * contains negative numbers, after the increase the internal
37: * array may violate the class invariant. Repair the first error,
38: * and see that T2 can also discover the second error.
39: */
40: public void increase(int b[]) {
41: int n = 10;
42: // if (b.length < n) n = b.length ;
43: for (int i = 0; i < n; i++)
44: a[i] = a[i] + b[i];
45: }
46:
47: /**
48: * Will increase all elements by some specified integer, if it is
49: * non-negative.
50: */
51: public void increase(int delta) {
52: if (delta > 0)
53: for (int i = 0; i < 10; i++)
54: a[i] = a[i] + delta;
55: }
56:
57: }
|