Understanding and maintaining tactics graphically OR how we are learning that a diagram can be worth more than 10K LoC
DOI:
https://doi.org/10.6092/issn.1972-5787/6298Keywords:
proof maintenance, theorem proving, graphical tactic languageAbstract
The use of a functional language to implement proof strategies as proof tactics in interactive theorem provers, often provides short, concise and elegant implementations. Whilst being elegant, the use of higher order features and combinator languages often results in a very procedural view of a strategy, which may deviate significantly from the high-level ideas behind it. This can make a tactic hard to understand and hence difficult to to debug and maintain for experts and non-experts alike: one often has to tear apart complex combinations of lower level tactics manually in order to analyse a failure in the overall strategy.
In an industrial technology transfer project, we have been working on porting a very large and complex proof tactic into PSGraph, a graphical language for representing proof strategies. The goal of this work is to improve understandability and maintainability of tactics. Motivated by some initial successes with this, we here extend PSGraph with additional features for development and debugging. Through the re-implementation and refactoring of several existing tactics, we demonstrates the advantages of PSGraph compared with a typical sentential tactic language with respect to debugging, readability and maintenance. In order to act as guidance for others, we give a fairly detailed comparison of the user experience with the two approaches. The paper is supported by a web page providing further details about the implementation as well as interactive illustrations of the examples.
References
Mark Adams. Refactoring proofs with tactician. In Domenico Bianculli, Radu Calinescu, and Bernhard Rumpe, editors, Software Engineering and Formal Methods: SEFM 2015. Revised Selected Papers, pages 53–67, Berlin, Heidelberg, 2015. Springer. 34, 50
Rob Arthan. Now f is continuous (exercise!). Journal of Formalized Reasoning, 9(1):33–52, 2016. 44, 45
Rob Arthan and Roger Bishop Jones. Z in HOL in ProofPower. BCS FACS FACTS, 2005-1. http://www.bcs.org/upload/pdf/facts200503.pdf. 2, 3
David Aspinall and Cezary Kaliszyk. Towards formal proof metrics. In Perdita Stevens and Andrzej Wasowski, editors, Fundamental Approaches to Software Engineering: 19th International Conference, FASE 2016, pages 325–341, Berlin, Heidelberg, 2016. Springer. 49
Richard Bornat and Bernard Sufrin. Jape: A calculator for animating proof-on-paper. In CADE-14, pages 412–415. Springer, 1997. 49
Alan Bundy. A science of reasoning. In International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, pages 10–17. Springer, 1998. 49
R. Burstall. Proveeasy: Helping people learn to do proofs. ENTCS, 31(0):16 – 32, 2000. 49
Lucas Dixon and Jacques D. Fleuriot. IsaPlanner: A Prototype Proof Planner in Isabelle. In CADE-19, volume 2741 of LNCS, pages 279–283. Springer, 2003. 49
Lucas Dixon and Aleks Kissinger. Open Graphs and Monoidal Theories. CoRR, abs/1011.4114, 2010. 10
Hartmut Ehrig, Karsten Ehrig, Ulrike Prange, and Gabriele Taentzer. Fundamentals of Algebraic Graph Transformation. Monographs in Theoretical Computer Science. Springer, 2006. 10
Georges Gonthier. A computer-checked proof of the four colour theorem, 2005. 49
Michael J. C. Gordon, Robin Milner, and Christopher P. Wadsworth. Edinburgh LCF, volume 78 of Lecture Notes in Computer Science. Springer, 1979. 3
Mike Gordon. From LCF to HOL: a short history. In Gordon D. Plotkin, Colin Stirling, and Mads Tofte, editors, Proof, Language, and Interaction, Essays in Honour of Robin Milner, pages 169–186. The MIT Press, 2000. 3, 6
G. Grov, A. Kissinger, and Y. Lin. A Graphical Language for Proof Strategies. In LPAR, pages 324–339. Springer, 2013. 2, 51
G. Grov, A. Kissinger, and Y. Lin. Tinker, Tailor, Solver, Proof. In UITP 2014, volume 167 of ENTCS, pages 23–34. Open Publishing Association, 2014. 2, 12
Jim Grundy. Window inference in the HOL system. In International Workshop on HOL Theorem Proving System and Its Applications, pages 177–189. IEEE, 1991. 49
Thomas Hales, Mark Adams, Gertrud Bauer, Dat Tat Dang, John Harrison, Truong Le Hoang, Cezary Kaliszyk, Victor Magron, Sean McLaughlin, Thang Tat Nguyen, et al. A formal proof of the kepler conjecture. arXiv preprint arXiv:1501.02155, 2015. 49
John Harrison. HOL light: An overview. In Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel, editors, Theorem Proving in Higher Order Logics, 22nd Inter- national Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings, volume 5674 of LNCS, pages 60–66. Springer, 2009. 2, 3
G ́erard Huet. The zipper. Journal of functional programming, 7(05):549–554, 1997. 49
Lars Hupel. Interactive simplifier tracing and debugging in isabelle. In Stephen M. Watt, James H. Davenport, Alan P. Sexton, Petr Sojka, and Josef Urban, editors, CICM, pages 328–343, Cham, 2014. Springer. 50
Joe Hurd. OpenTheory: Package management for higher order logic theories. In Gabriel Dos Reis and Laurent Th ́ery, editors, PLMMS ’09: Proceedings of the ACM SIGSAM 2009 International Workshop on Programming Languages for Mechanized Mathematics Systems, pages 31–37, August 2009. 51
A. Kissinger and V. Zamdzhiev. Quantomatic: A Proof Assistant for Diagrammatic Reason- ing. In CADE-25, volume 9195 of LNCS, pages 326–336. Springer, 2015. 13
Gerwin Klein. Proof engineering considered essential. In FM 2014: Formal Methods, pages 16–21. Springer, 2014. 49
Gerwin Klein, June Andronick, Kevin Elphinstone, Toby Murray, Thomas Sewell, Rafal Kolanski, and Gernot Heiser. Comprehensive formal verification of an os microkernel. ACM Transactions on Computer Systems (TOCS), 32(1):2, 2014. 49
Jill H Larkin and Herbert A Simon. Why a diagram is (sometimes) worth ten thousand words. Cognitive science, 11(1):65–100, 1987. 2
Yibo Liang, Yuhui Lin, and Gudmund Grov. ‘the tinker’ for rodin. In Michael Butler, Klaus- Dieter Schewe, Atif Mashkoor, and Miklos Biro, editors, Abstract State Machines, Alloy, B, TLA, VDM, and Z: 5th International Conference, ABZ 2016, Linz, Austria, May 23-27, 2016, Proceedings, pages 262–268. Springer, 2016. 2
T Libal, M Riener, and M Rukhaia. Advanced Proof Viewing in ProofTool. In UITP 2014, volume 167 of EPTCS, pages 35–47. Open Publishing Association, 2014. 49
Y. Lin, G. Grov, and R. Arthan. Debugging and refactoring tactics graphically – paper resources. http://ggrov.github.io/tinker/jfr16/. Accessed: July 2016. 3, 13, 41, 51
Yuhui Lin, Gudmund Grov, Colin O’Halloran, and Priiya G. A super industrial application of PSGraph. To appear in ABZ 2016. 2, 22, 49, 51
Yuhui Lin, Pierre Le Bras, and Gudmund Grov. Developing and debugging proof strategies by tinkering. In Marsha Chechik and Jean-Fran ̧cois Raskin, editors, Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 573–579, Berlin, Heidelberg, 2016. Springer. 2, 12, 13
Makarius Wenzel and many others. The Isabelle/Isar Reference Manual. http://isabelle.in.tum.de/dist/Isabelle2013-2/doc/isar-ref.pdf. 2, 3
C. O’Halloran. Automated Verification of Code Automatically Generated from Simulink. ASE, 20(2):237–264, 2013. 2
Maris A Ozols, Anthony Cant, and Katherine A Eastaughffe. Xisabelle: A system description. In CADE-14, pages 400–403. Springer, 1997. 49
Karol Pak. The algorithms for improving and reorganizing natural deduction proofs. Studies in Logic, Grammar and Rhetoric, 22(35):95–112, 2010. 49
Lawrence C. Paulson. A higher-order implementation of rewriting. Sci. Comput. Program., 3(2):119–149, 1983. 4
Gill Prout, Rob Arthan, Roger Jones, and Roger Stokes. The Front End Filter Project: specification and verification of a secure database system. http://www.lemma-one.com/ ProofPower/fef/fef.html. 35, 36
J ̈org H. Siekmann, Stephan M. Hess, Christoph Benzmu ̈ller, Lassaad Cheikhrouhou, Armin Fiedler, Helmut Horacek, Michael Kohlhase, Karsten Konrad, Andreas Meier, Erica Melis, Martin Pollet, and Volker Sorge. LOUI: Lovely OMEGA User Interface. Formal Asp. Comput, 11(3):326–342, 1999. 49
Konrad Slind and Michael Norrish. A brief overview of HOL4. In Theorem Proving in Higher Order Logics (TPHOLs), volume 5170 of LNCS. Springer, 2008. 2, 3
MarkStaples,RossJeffery,JuneAndronick,TobyMurray,GerwinKlein,andRafalKolanski. Productivity for proof engineering. In Proceedings of the 8th ACM/IEEE International Symposium on Empirical Software Engineering and Measurement, page 15. ACM, 2014. 49
I. Whiteside, D. Aspinall, L. Dixon, and G. Grov. Towards Formal Proof Script Refactoring. In CICM’11, volume 6824 of LNCS, pages 260–275. Springer, 2011. 50
Iain Whiteside. Refactoring Proofs. PhD thesis, University of Edinburgh, 2013. 50
Downloads
Published
How to Cite
Issue
Section
License
Copyright (c) 2016 YuHui Lin, Gudmund Grov, Rob Arthan
Copyrights and publishing rights of all the texts on this journal belong to the respective authors without restrictions.
This journal is licensed under a Creative Commons Attribution 3.0 Unported License (full legal code).
See also our Open Access policy
