Information Technology Reference
In-Depth Information
Ta b l e 2 .
Abstract repair actions suggested by DREAM for Singly Linked List
Err. # Abstract Repair Action(s)
1 [] (in post-state).header = [FIRST NODE] (in pre-state)
2 DREAM Not Working: Call SAT
3 FIRSTNODE] (in post-state).next = [header.next.next] (in pre-state)
4[LASTNODE] (in post-state).next = [null]
5[LASTNODE] (in post-state).next = [header.next.next.next] (in pre-state)
6 FIRSTNODE] (in post-state).elt = [header.elt] (in pre-state)
7 FIRSTNODE] (in post-state).elt = [header.elt] (in pre-state)
[](in post-state).size = [size] - 1 (in post-state)
8 FIRSTNODE] (in post-state).next = [null]
[] (in post-state).header = [header.next] (in post-state)
[header.next] (in post-state).elt = [header.elt] (in post-state)
[FIRST NODE] (in post-state).elt = [null]
9
[header.next] (in pre-state).next = [null]
[header.next] (in pre-state).elt = [null]
[] (in post-state).size = [size] - 1 (in post-state)
Ta b l e 3 .
Time taken to repair erroneous Singly Linked Lists (ms). OH means Out of Heap.
Cobbler/DREAM
Cobbler
DREAM
(Size = 10)
(Size = 500)
(Size = 500)
Repair
1
320
799
1119
287034
125638
412672
24
0
0
1 77
78
5291x
2
915
8846
9761
241701
446
OH
Not Working: Call SAT
N/A
3
166
417
583
127434
240674
368108
14
38
0
39 37 114
3229x
4
128
381
509
81428
52
OH
6
0
0
1 41
42
N/A
5
130
292
422
52621
61751
114372
6
0
0
6 40
46
2486x
6
145
410
555
55691
142061
197752
7
42
0
44 32 118
1676x
7
126
319
445
52356
133512
185868
6
19
0
21 32
72
2582x
8
131
259
390
51766
234913
286679
6
16
1
17 32
66
4344x
9
228
797
1025
92219
298215
390434
8
64
1
69 69 203
1923x
repair time. For DREAM, first the repair actions are abstracted (column Abs.) using
concrete repair actions taken by Cobbler on the data structure of ten nodes. Then, using
the data structure of 500 nodes, a Java check is performed to find that the specification is
violated. This Java check is a manual translation of the specification from Alloy to Java
using the Minshar technique which can be automated using the Minshar tool. When this
initial check fails, DREAM repair performs concretization (the Con. column) followed
by the application of concretized actions (the App. column). Unlike Cobbler which only
suggests correct fixes, the result of applying a set of abstract repair actions by DREAM
should be checked to see if the abstractions can indeed resolve the problem. Therefore,
