Page 256 - DCAP305_PRINCIPLES_OF_SOFTWARE_ENGINEERING

Principles of Software Engineering

Notes (VCs) using the SPARK examiner, and simplified the generated VCs using the SPARK simplifier.
We measured the number of VCs, the size of VCs, the maximum length of VCs, and the time that
the SPARK tools took to analyze the code. These data did not necessarily represent the actual
proof effort needed for the implementation proof, but they were an indication.
The times required for analysis with the SPARK tools after the various refactoring are shown as
Figure 12.4 (c). Some blocks are shown with no value because the VCs were too complicated to
be handled by the SPARK tools. After the first loop rerolling at block 1, the tools completed the
analysis but took 7 hours and 23 minutes on a 2.0 GHz machine. At block 2 with word packing
reversed, the analysis again became infeasible. It was not until block 8, when we had adjusted
the loop forms in the key schedule setup function that analysis by the SPARK tools became
feasible again. The required analysis time gradually decreased and reached 1 minute 42 seconds
for the final refectories program (a reduction of more than 99%).

The size of VCs showed the same declining trend. In block 1, 51.16 MB VCs were generated
and 2.59 MB VCs were left after simplification. For the final refectories code, 1.90 MB VCs were
generated and 86 KB were left after simplification (Figs 12.4(d) and 12.4(e)).

Figure 12.4: Metric Analysis with AES Verification Refactoring

(a) Lines of code (b) Average McCabe cyclamate complexities

1400 3
1200 2.5
1000
2
800
1.5
600
1
400
200 0.5
0 0
0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 0 1 2 3 4 5 6 7 8 91011121314

(c) SPARK analysis time (d) Size of generated VCs
MB
7:23:55 51.15 MB
0:07:00 6
0:06:00 5
0:05:00
4
0:04:00
3
0:03:00
2
0:02:00
0:01:00 1
0:00:00 0
0 1 2 3 4 5 6 7 8 91011121314 0 1 2 3 4 5 6 7 8 9 10 11 12 13 14
(e) Size of simplified VCs (f) Specification structure match ratio
MB MB
2.50 MB
0.2 100%
80%
0.15
60%
0.1
40%
0.05
20%
0 0%
0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 0 1 2 3 4 5 6 7 8 9 10 11 12 13 14

250 LOVELY PROFESSIONAL UNIVERSITY