01: package U2.T2.examples;
02:
03: import java.util.*;
04:
05: /**
06: * A variant of SortedList, so a class implementing a sorted list. But
07: * this one has a temporal property:
08: *
09: * !open /\ s=S /\ max=M unless open, for all S,M
10: *
11: * This spec is approved by T2 (it can't found violation).
12: */
13: public class TSortedList {
14:
15: private LinkedList<Comparable> s;
16: private Comparable max;
17: public boolean open = true;
18:
19: public TSortedList() {
20: s = new LinkedList<Comparable>();
21: }
22:
23: public boolean classinv() {
24: return temporal_spec();
25: }
26:
27: public void insert(Comparable x) {
28:
29: if (!open)
30: return;
31:
32: int i = 0;
33: for (Comparable y : s) {
34: if (y.compareTo(x) > 0)
35: break;
36: i++;
37: }
38: s.add(i, x);
39:
40: // injected error in the original SortedList is removed.
41: // if (max==null || x.compareTo(max) < 0) max = x ;
42: if (max == null || x.compareTo(max) > 0)
43: max = x;
44: }
45:
46: public Comparable get() {
47: if (!open)
48: return null;
49: Comparable x = max;
50: s.remove(max);
51: if (s.isEmpty())
52: max = null;
53: else
54: max = s.getLast();
55: return x;
56: }
57:
58: public Comparable get_spec() {
59:
60: assert !s.isEmpty() : "PRE";
61:
62: Comparable ret = get();
63:
64: assert !open || s.isEmpty() || ret.compareTo(s.getLast()) >= 0 : "POST";
65:
66: return ret;
67: }
68:
69: private static final int STATE_INIT = 0;
70:
71: private LinkedList<Comparable> aux_s_frozen;
72: private Comparable aux_max_frozen;
73: private boolean aux_open_frozen;
74: private int aux_state = STATE_INIT; // initialialize state
75:
76: private void save_state() {
77: aux_s_frozen = new LinkedList(s);
78: aux_max_frozen = max;
79: aux_open_frozen = open;
80: }
81:
82: private boolean temporal_spec() {
83: if (aux_state == STATE_INIT) {
84: save_state();
85: aux_state++;
86: return true;
87: } else {
88: boolean ok = aux_open_frozen
89: || (aux_s_frozen.equals(s) && aux_max_frozen == max)
90: || open;
91:
92: save_state();
93: return ok;
94: }
95: }
96:
97: }
|