Automating Refinement of Circus Programs - Formal Methods: Foundations and Applications - page 287

Phase POs Before POs Current Run-time Before Run-time Current

NBStep1 1 1 0 . 0sec 0 . 1sec

NBStep2 44 4 2 . 3sec 1 . 1sec

NBStep3 101 8 9 . 1sec 2 . 4sec

NBStep4 163 15 17 . 9sec 3 . 9sec

NBStep5 6

19 . 9sec 4 . 7sec

198 18

NBStep7 243 24 21 . 1sec 5 . 9sec

Fig. 1. Comparison of the number of generated provisos for NB

conditions. Table 1 summarises the results obtained for the tactics NBStep1 to
NBStep7 of the refinement strategy. ( NBStep5 and NBStep6 have been merged
into one tactic). Each row entails the invocation of the preceding tactics too; for
instance, the second row refers to the execution of both NBStep1 and NBStep2 .
We report on the number of remaining provisos as well as the execution time of
the tactics measured by the timing facilities of Poly/ML.
The results show that assumptions are reduced by approximately 90%. This
remains fairly constant across tactics, and invariant with the growth in size. We
may expect a similar reduction in runtime, but it is offset by the effort required
to discharge the provisos. Despite, we see that overall this effort is recovered, and
the gain increases with the complexity of the generated refinement theorems. For
example, after NBStep2 we only have a small speed-up, and for NBStep1 even a
slight loss. The speed-up, however, becomes larger in the next two phases.
To check if this trend continues with more complex examples, we have slightly
amended the Diff process. This has resulted in larger ProofPower-Z terms and
the need for more elementary steps to transform the program. In this case,
the original implementation takes 61 sec to execute phases NBStep1 to NB-
Step5 6 and generates a theorem with 259 assumptions. In comparison, the new
technique requires 7 . 2 sec producing 24 assumptions, giving a further speed-up
increase to 8.5. After once more elaborating the complexity of the example spec-
ification, the former approach requires 154 . 4 sec and produces 301 assumptions
whereas the new ArcAngel C

implementation only takes 10 . 9 sec. Although we still
have a similar 90% reduction in assumptions, the speed-up has now increased
to 14.1.
The above suggests that with growing complexity of the ArcAngel C tactics

and specifications, the speed-up may further increase, even so non-linearly.

Reasons for this may be that certain operations on theorems are slowed down
in a non-proportional way when theorems become larger. It should be pointed
out that the system we compare with already includes the simplification to the
mechanisation reducing type provisos that we discussed in Section 3.1.
Our results increase confidence that, with the new technique and tool support,
it is possible now to apply the entire refinement strategy and obtain a result
within a reasonable amount of time.

Circus