01: package U2.T2.examples;
02:
03: /**
04: * This class shows that T2 can handle multi dimensional arrays. It
05: * has no fields, only methods. It contains errors.
06: */
07: public class TestArray2 {
08:
09: /**
10: * Find the maximum element of a two dimensional array, assuming
11: * the array is non-empty. It contains error: if the array
12: * contains all negative elements, which are all less than -1, it
13: * will return -1 as the maximum element.
14: */
15: public int findMax(int[][] a) {
16: int m = -1;
17: for (int i = 0; i < a.length; i++) {
18: if (a[i] == null)
19: continue;
20: int r = -1;
21: for (int j = 0; j < a[i].length; j++)
22: if (a[i][j] > r)
23: r = a[i][j];
24: if (r > m)
25: m = r;
26: }
27: ;
28: return m;
29: }
30:
31: /**
32: * The method encoding the specification of findMax.
33: */
34: public int findMax_spec(int[][] a) {
35: boolean empty = true;
36: if (a != null)
37: for (int i = 0; i < a.length && empty; i++) {
38: if (a[i] == null)
39: continue;
40: empty = a[i].length <= 0;
41: }
42: ;
43: // specify the pre-condition, namely that a should be
44: // non-empty:
45: assert !empty : "PRE";
46:
47: int m = findMax(a);
48:
49: // And the post-condition, that the returned maximum should be
50: // an element of a:
51: boolean ok = false;
52: for (int i = 0; i < a.length && !ok; i++) {
53: if (a[i] == null)
54: continue;
55: for (int j = 0; j < a[i].length && !ok; j++)
56: ok = m == a[i][j];
57: }
58: ;
59: assert ok : "POST";
60: return m;
61: }
62:
63: }
|