Towards Formal Proof Metrics

David Aspinall, Cezary Kaliszyk

19th International Conference on Fundamental Approaches to Software Engineering, LNCS 9633, pp. 325-341, 2016.


Recent years have seen increasing success in building large formal proof developments using interactive theorem provers (ITPs). Some proofs have involved many authors, years of effort, and resulted in large, complex interdependent sets of proof “source code” files. Developing these in the first place, and maintaining and extending them afterwards, is a considerable challenge. It has prompted the idea of Proof Engineering as a new sub-field, to find methods and tools to help. It is natural to try to borrow ideas from Software Engineering for this.

In this paper we investigate the idea of defining proof metrics by analogy with software metrics. We seek metrics that may help to monitor and compare formal proof developments, which might be used to guide good practice, locate likely problem areas, or suggest refactorings. Starting from metrics that have been proposed for object-oriented design, we define analogues for formal proofs. We show that our metrics enjoy reasonable properties, and we demonstrate their behaviour with some practical experiments, showing changes over time as proof developments evolve, and making comparisons across between different ITPs.


  PDF |    doi:10.1007/978-3-662-49665-7_19


author = {David Aspinall and Cezary Kaliszyk},
title = {Towards Formal Proof Metrics},
booktitle = {19th International Conference on Fundamental Approachesto Software Engineering
(FASE 2016)},
pages = {325--341},
year = {2016},
editor = {Perdita Stevens and Andrzej Wasowski},
series = {Lecture Notes in Computer Science},
volume = {9633},
publisher = {Springer},
doi = {10.1007/978-3-662-49665-7_19},
Nach oben scrollen