Abstract
We consider the problem of formally verifying an algorithm in a proof assistant and generating efficient code. Reasoning about correctness is best done at an abstract level, but efficiency of the generated code often requires complicated data structures. Data refinement has been successfully used to reconcile these conflicting requirements, but usability calls for automatic tool support. In the context of Isabelle/HOL, two frameworks for automating data refinement have been proposed (Lammich, in: Blazy, Paulin-Mohring, Pichardie (eds) ITP 2013, LNCS, vol 7998, Springer, Heidelberg, pp 84–99, 2013; Lochbihler, in: Blazy, Paulin-Mohring, Pichardie (eds) ITP 2013, LNCS, vol 7998, Springer, Heidelberg, pp 116–132, 2013). In this paper, we present and compare the two frameworks and their underlying ideas in depth. Thereby, we identify the challenges of automating data refinement, highlight the similarities and differences of the two approaches, and show their strengths and limitations both from the implementer’s and the user’s perspectives. A case study demonstrates how to combine both frameworks, benefiting from the strengths of each.
Article PDF
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.Avoid common mistakes on your manuscript.
References
Appel, A.W.: Efficient verified red-black trees. http://www.cs.princeton.edu/~appel/papers/redblack.pdf (2011)
Aspvall, B., Plass, M.F., Tarjan, R.E.: A linear-time algorithm for testing the truth of certain quantified boolean formulas. Inf. Process. Lett. 8(3), 121–123 (1979)
Back, R.J.J., Akademi, A., Wright, J.V.: Refinement Calculus: A Systematic Introduction, 1st edn. Springer, New York (1998)
Ballarin, C.: Locales: a module system for mathematical theories. J. Autom. Reason. 52(2), 123–153 (2014). https://doi.org/10.1007/s10817-013-9284-7
Berghofer, S., Reiter, M.: Formalizing the logic-automaton connection. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009, LNCS, vol. 5674, pp. 147–163. Springer, Heidelberg (2009)
Blanchette, J.C., Hölzl, J., Lochbihler, A., Panny, L., Popescu, A., Traytel, D.: Truly modular (co)datatypes for Isabelle/HOL. In: ITP 2014, pp. 93–110 (2014)
Brunner, J., Lammich, P.: Formal verification of an executable LTL model checker with partial order reduction. In: Rayadurgam, S., Tkachuk, O. (eds.) NFM 2016. LNCS, vol. 9690, pp. 307–321. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-40648-0_23
Chen, K., Hudak, P., Odersky, M.: Parametric type classes. In: LFP 1992, pp. 170–181. ACM, New York (1992)
Cohen, C., Dénès, M., Mörtberg, A.: Refinements for free!. In: Gonthier, G., Norrish, M. (eds.) CPP 2013, LNCS, vol. 8307, pp. 147–162. Springer, Heidelberg (2013)
Cohen, C., Rouhling, D.: A refinement-based approach to large scale reflection for algebra. In: Journées Francophones des Langages Applicatifs (JFLA 2017) (2017). Technical report HAL-01414881. https://hal.inria.fr/hal-01414881
Delaware, B., Pit-Claudel, C., Gross, J., Chlipala, A.: Fiat: deductive synthesis of abstract data types in a proof assistant. In: Proceedings of POPL, pp. 689–700. ACM, New York (2015). https://doi.org/10.1145/2676726.2677006
Esparza, J., Lammich, P., Neumann, R., Nipkow, T., Schimpf, A., Smaus, J.G.: A fully verified executable LTL model checker. In: Sharygina, N., Veith, H. (eds.) CAV 2013, LNCS, vol. 8044, pp. 463–478. Springer, Heidelberg (2013)
Felgenhauer, B., Thiemann, R.: Reachability, confluence, and termination analysis with state-compatible automata. Inf. Comput. 253, 467–483 (2017). https://doi.org/10.1016/j.ic.2016.06.011
Haftmann, F., Krauss, A., Kunčar, O., Nipkow, T.: Data refinement in Isabelle/HOL. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013, LNCS, vol. 7998, pp. 100–115. Springer, Heidelberg (2013)
Haftmann, F., Lochbihler, A., Schreiner, W.: Towards abstract and executable multivariate polynomials in Isabelle. Isabelle workshop 2014. http://www.infsec.ethz.ch/people/andreloc/publications/haftmann14iw.pdf (2014)
Haftmann, F., Nipkow, T.: Code generation via higher-order rewrite systems. In: Blume, M., Kobayashi, N., Vidal-Oriola, G. (eds.) FLOPS 2010, LNCS, vol. 6009, pp. 103–117. Springer, Heidelberg (2010)
Hoare, C.: Proof of correctness of data representations. Acta Inf. 1(4), 271–281 (1972)
Huffman, B., Kunčar, O.: Lifting and transfer: a modular design for quotients in Isabelle/HOL. In: Gonthier, G., Norrish, M. (eds.) CPP 2013, LNCS, vol. 8307, pp. 131–146. Springer, Heidelberg (2013)
Immler, F.: Verified reachability analysis of continuous systems. In: Baier, C., Tinelli, C. (eds.) TACAS 2015, LNCS, vol. 9035, pp. 37–51. Springer, Heidelberg (2015)
Kanav, S., Lammich, P., Popescu, A.: A conference management system with verified document confidentiality. In: Biere, A., Bloem, R. (eds.) CAV 2014, LNCS, vol. 8559, pp. 167–183. Springer, Heidelberg (2014)
Klein, G., Nipkow, T.: A machine-checked model for a Java-like language, virtual machine and compiler. ACM Trans. Progr. Lang. Syst. 28, 619–695 (2006)
Lammich, P.: Tree automata. Archive of Formal Proofs. http://www.isa-afp.org/entries/Tree-Automata.shtml, Formal proof development (2009)
Lammich, P.: Automatic data refinement. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013, LNCS, vol. 7998, pp. 84–99. Springer, Heidelberg (2013)
Lammich, P.: The CAVA automata library. Archive of Formal Proofs. http://www.isa-afp.org/entries/CAVA_Automata.shtml, Formal proof development (2014)
Lammich, P.: Verified efficient implementation of Gabow’s strongly connected component algorithm. In: Klein, G., Gamboa, R. (eds.) ITP 2014, LNCS, vol. 8558, pp. 325–340. Springer, Heidelberg (2014)
Lammich, P.: Refinement to Imperative/HOL. In: Urban, C., Zhang, X. (eds.) ITP 2015, LNCS, vol. 9236, pp. 253–269. Springer, Heidelberg (2015)
Lammich, P.: Refinement based verification of imperative data structures. In: Avigad, J., Chlipala, A. (eds.) CPP 2016, pp. 27–36. ACM, New York (2016)
Lammich, P., Lochbihler, A.: The Isabelle collections framework. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010, LNCS, vol. 6172, pp. 339–354. Springer, Heidelberg (2010)
Lammich, P., Tuerk, T.: Applying data refinement for monadic programs to Hopcroft’s algorithm. In: Beringer, L., Felty, A. (eds.) ITP 2012, LNCS, vol. 7406, pp. 166–182. Springer, Heidelberg (2012)
Leroy, X.: A formally verified compiler back-end. J. Autom. Reason. 43(4), 363–446 (2009)
Lochbihler, A.: A machine-checked, type-safe model of Java concurrency: language, virtual machine, memory model, and verified compiler. Ph.D. thesis, Karlsruher Institut für Technologie, Fakultät für Informatik (2012)
Lochbihler, A.: Light-weight containers. Archive of Formal Proofs. http://www.isa-afp.org/entries/Containers.shtml, Formal proof development (2013)
Lochbihler, A.: Light-weight containers for Isabelle: efficient, extensible, nestable. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013, LNCS, vol. 7998, pp. 116–132. Springer, Heidelberg (2013)
Lochbihler, A., Bulwahn, L.: Animating the formalised semantics of a Java-like language. In: van Eekelen, M., Geuvers, H., Schmalz, J., Wiedijk, F. (eds.) ITP 2011, LNCS, vol. 6898, pp. 216–232. Springer, Heidelberg (2011)
Marić, F.: Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL. Theor. Comput. Sci. 411(50), 4333–4356 (2010)
Musser, D.R., Stepanov, A.A.: Generic programming. In: Gianni, P. (ed.) ISSAC 1988, LNCS, vol. 358, pp. 13–25. Springer, Heidelberg (1989)
Nipkow, T.: Automatic functional correctness proofs for functional search trees. In: Blanchette, J.C., Merz, S. (eds.) ITP 2016, LNCS, vol. 9807, pp. 307–322. Springer, Heidelberg (2016)
Nipkow, T., Paulson, L.C.: Proof pearl: defining functions over finite sets. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005, LNCS, vol. 3603, pp. 385–396. Springer, Heidelberg (2005)
Nordhoff, B., Lammich, P.: Dijkstra’s shortest path algorithm. Archive of Formal Proofs. http://www.isa-afp.org/entries/Dijkstra_Shortest_Path.shtml, Formal proof development (2012)
Peyton Jones, S.: Bulk types with class. In: Haskell Workshop 1997 (1997)
Plotkin, G.D.: A note on inductive generalization. Mach. Intell. 5(1), 153–163 (1970)
Schimpf, A., Lammich, P.: Converting linear-time temporal logic to generalized Büchi automata. Archive of Formal Proofs. http://www.isa-afp.org/entries/LTL_to_GBA.shtml, Formal proof development (2014)
Schimpf, A., Merz, S., Smaus, J.: Construction of Büchi automata for LTL model checking verified in Isabelle/HOL. TPHOLs 2009, LNCS, vol. 5674, pp. 424–439. Springer, Heidelberg (2009)
Sozeau, M., Oury, N.: First-class type classes. In: Ait Mohamed, O., Muñoz, C., Tahar, S. (eds.) TPHOLs 2008, LNCS, vol. 5170, pp. 278–293. Springer, Heidelberg (2008)
Sternagel, C., Thiemann, R.: Deriving comparators and show functions in Isabelle/HOL. In: Urban, C., Zhang, X. (eds.) ITP 2015, LNCS, vol. 9236, pp. 421–437. Springer, Heidelberg (2015)
Sternagel, C., Thiemann, R., Winkler, S., Zankl, H.: CeTA—a tool for certified termination analysis. CoRR abs/1208.1591. http://arxiv.org/abs/1208.1591 (2012)
Thiemann, R.: Implementing field extensions of the form Q[sqrt(b)]. Archive of Formal Proofs. http://www.isa-afp.org/entries/Real_Impl.shtml, Formal proof development (2014)
Thiemann, R., Sternagel, C.: Certification of termination proofs using CeTA. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009, LNCS, vol. 5674, pp. 452–468. Springer, Heidelberg (2009)
Wirth, N.: Program development by stepwise refinement. Commun. ACM 14(4), 221–227 (1971)
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Lammich, P., Lochbihler, A. Automatic Refinement to Efficient Data Structures: A Comparison of Two Approaches. J Autom Reasoning 63, 53–94 (2019). https://doi.org/10.1007/s10817-018-9461-9
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10817-018-9461-9