Abstract
We present a prototype refactoring framework based on graph rewriting and bidirectional transformations that is designed to be generic, extensible, and declarative. Our approach uses a language-independent graph meta-model to represent proof developments in a generic way. We use graph rewriting to enrich the meta-model with dependency information and to perform refactorings, which are written as declarative rewrite rules. Our framework, called Polar, is implemented in the GrGen rewriting engine.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Arias, T.B.C., van der Spek, P., Avgeriou, P.: A practice-driven systematic review of dependency analysis solutions. Empirical Software Engineering 16(5), 544–586 (2011)
Aschbacher, M.: Highly complex proofs and implications of such proofs. Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences 363, 2401–2406 (2005)
Autexier, S., Dietrich, D., Hutter, D., Lüth, C., Maeder, C.: Smartties - management of safety-critical developments. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012, Part I. LNCS, vol. 7609, pp. 238–252. Springer, Heidelberg (2012)
Bancilhon, F., Spyratos, N.: Update semantics of relational views. ACM Trans. Database Syst. 6(4), 557–575 (1981)
Bell Canada. DATRIX abstract semantic graph reference manual (version 1.4). Technical report (2000)
Bourke, T., Daum, M., Klein, G., Kolanski, R.: Challenges and experiences in managing large-scale proofs. In: Jeuring, J., Campbell, J.A., Carette, J., Dos Reis, G., Sojka, P., Wenzel, M., Sorge, V. (eds.) CICM 2012. LNCS (LNAI), vol. 7362, pp. 32–48. Springer, Heidelberg (2012)
Chen, H., Liao, H.: A comparative study of view update problem. In: Data Storage and Data Engineering (DSDE), pp. 83–89 (2010)
de Lara, J., Bardohl, R., Ehrig, H., Ehrig, K., Prange, U., Taentzer, G.: Attributed graph transformation with node type inheritance. Theor. Comput. Sci. 376(3), 139–163 (2007)
Dietrich, D.: Assertion Level Proof Planning with Compiled Strategies. PhD thesis, Saarland University (2011)
Ferrante, J., Ottenstein, K.J., Warren, J.D.: The program dependence graph and its use in optimization. ACM Trans. Program. Lang. Syst. 9(3), 319–349 (1987)
Geiß, R., Batz, G.V., Grund, D., Hack, S., Szalkowski, A.: GrGen: A fast SPO-based graph rewriting tool. In: Corradini, A., Ehrig, H., Montanari, U., Ribeiro, L., Rozenberg, G. (eds.) ICGT 2006. LNCS, vol. 4178, pp. 383–397. Springer, Heidelberg (2006)
Gonthier, G.: The Four Colour Theorem: Engineering of a formal proof. In: Kapur, D. (ed.) ASCM 2007. LNCS (LNAI), vol. 5081, p. 333. Springer, Heidelberg (2008)
Gonthier, G., et al.: A machine-checked proof of the odd order theorem. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 163–179. Springer, Heidelberg (2013)
Gonthier, G., Mahboubi, A., Rideau, L., Tassi, E., Théry, L.: A Modular Formalisation of Finite Group Theory. Rapport de recherche RR-6156, INRIA (2007)
Gordon, M., Milner, R., Morris, L., Newey, M., Wadsworth, C.: A metalanguage for interactive proof in LCF. In: Proceedings of the 5th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL 1978, pp. 119–130. ACM, New York (1978)
Hales, T.C.: Introduction to the Flyspeck project. In: Coquand, T., Lombardi, H., Roy, M.-F. (eds.) Mathematics, Algorithms, Proofs. Dagstuhl Seminar Proceedings, vol. 05021 (2006)
Hofmann, M., Pierce, B., Wagner, D.: Edit lenses. In: ACM SIGPLAN Notices, vol. 47, pp. 495–508. ACM (2012)
Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., et al.: seL4: Formal verification of an OS kernel. In: Proceedings of the ACM SIGOPS 22nd Symposium on Operating Systems Principles, pp. 207–220. ACM (2009)
Mens, T., Eetvelde, N.V., Demeyer, S., Janssens, D.: Formalizing refactorings with graph transformations. Journal of Software Maintenance 17(4), 247–276 (2005)
Opdyke, W.F.: Refactoring object-oriented frameworks. PhD thesis, Champaign, IL, USA (1992)
Stevens, P.: A landscape of bidirectional model transformations. In: Lämmel, R., Visser, J., Saraiva, J. (eds.) GTTSE 2007. LNCS, vol. 5235, pp. 408–424. Springer, Heidelberg (2008)
Verbaere, M., Ettinger, R., de Moor, O.: JunGL: a scripting language for refactoring. In: Rombach, D., Soffa, M.L. (eds.) ICSE 2006: Proceedings of the 28th International Conference on Software Engineering, pp. 172–181. ACM Press, New York (2006)
Wenzel, M.T.: Isar - a generic interpretative approach to readable formal proof documents. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Théry, L. (eds.) TPHOLs 1999. LNCS, vol. 1690, pp. 167–184. Springer, Heidelberg (1999)
Whiteside, I.: Refactoring Proofs. PhD thesis, University of Edinburgh (2013)
Whiteside, I., Aspinall, D., Dixon, L., Grov, G.: Towards formal proof script refactoring. In: Davenport, J.H., Farmer, W.M., Urban, J., Rabe, F. (eds.) Calculemus/MKM 2011. LNCS (LNAI), vol. 6824, pp. 260–275. Springer, Heidelberg (2011)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dietrich, D., Whiteside, I., Aspinall, D. (2013). Polar: A Framework for Proof Refactoring. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2013. Lecture Notes in Computer Science, vol 8312. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-45221-5_52
Download citation
DOI: https://doi.org/10.1007/978-3-642-45221-5_52
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-45220-8
Online ISBN: 978-3-642-45221-5
eBook Packages: Computer ScienceComputer Science (R0)