×

zbMATH — the first resource for mathematics

Automatic refinement to efficient data structures: a comparison of two approaches. (English) Zbl 1459.68228
Summary: 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 [P. Lammich, Lect. Notes Comput. Sci. 7998, 84–99 (2013; Zbl 1317.68216); A. Lochbihler, Lect. Notes Comput. Sci. 7998, 116–132 (2013; Zbl 1317.68219)]. 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.
MSC:
68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
68P05 Data structures
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Appel, A.W.: Efficient verified red-black trees. http://www.cs.princeton.edu/ appel/papers/redblack.pdf (2011)
[2] Aspvall, B.; Plass, MF; Tarjan, RE, A linear-time algorithm for testing the truth of certain quantified boolean formulas, Inf. Process. Lett., 8, 121-123, (1979) · Zbl 0398.68042
[3] Back, R.J.J., Akademi, A., Wright, J.V.: Refinement Calculus: A Systematic Introduction, 1st edn. Springer, New York (1998) · Zbl 0949.68094
[4] Ballarin, C., Locales: a module system for mathematical theories, J. Autom. Reason., 52, 123-153, (2014) · Zbl 1315.68218
[5] 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) · Zbl 1252.68250
[6] 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) · Zbl 1416.68151
[7] 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 · Zbl 1426.68162
[8] Chen, K., Hudak, P., Odersky, M.: Parametric type classes. In: LFP 1992, pp. 170-181. ACM, New York (1992)
[9] Cohen, C.; Dénès, M.; Mörtberg, A.; Gonthier, G. (ed.); Norrish, M. (ed.), Refinements for free!, No. 8307, 147-162, (2013), Heidelberg
[10] 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 · Zbl 06821849
[11] 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 · Zbl 1346.68175
[12] Esparza, J.; Lammich, P.; Neumann, R.; Nipkow, T.; Schimpf, A.; Smaus, JG; Sharygina, N. (ed.); Veith, H. (ed.), A fully verified executable LTL model checker, No. 8044, 463-478, (2013), Heidelberg
[13] Felgenhauer, B.; Thiemann, R., Reachability, confluence, and termination analysis with state-compatible automata, Inf. Comput., 253, 467-483, (2017) · Zbl 1362.68137
[14] Haftmann, F.; Krauss, A.; Kunčar, O.; Nipkow, T.; Blazy, S. (ed.); Paulin-Mohring, C. (ed.); Pichardie, D. (ed.), Data refinement in Isabelle/HOL, No. 7998, 100-115, (2013), Heidelberg · Zbl 1317.68212
[15] 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)
[16] 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) · Zbl 1284.68131
[17] Hoare, C., Proof of correctness of data representations, Acta Inf., 1, 271-281, (1972) · Zbl 0244.68009
[18] Huffman, B.; Kunčar, O.; Gonthier, G. (ed.); Norrish, M. (ed.), Lifting and transfer: a modular design for quotients in Isabelle/HOL, No. 8307, 131-146, (2013), Heidelberg · Zbl 1426.68284
[19] 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)
[20] Kanav, S.; Lammich, P.; Popescu, A.; Biere, A. (ed.); Bloem, R. (ed.), A conference management system with verified document confidentiality, No. 8559, 167-183, (2014), Heidelberg
[21] 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)
[22] Lammich, P.: Tree automata. Archive of Formal Proofs. http://www.isa-afp.org/entries/Tree-Automata.shtml, Formal proof development (2009)
[23] Lammich, P.; Blazy, S. (ed.); Paulin-Mohring, C. (ed.); Pichardie, D. (ed.), Automatic data refinement, No. 7998, 84-99, (2013), Heidelberg
[24] Lammich, P.: The CAVA automata library. Archive of Formal Proofs. http://www.isa-afp.org/entries/CAVA_Automata.shtml, Formal proof development (2014)
[25] 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) · Zbl 1416.68168
[26] Lammich, P.: Refinement to Imperative/HOL. In: Urban, C., Zhang, X. (eds.) ITP 2015, LNCS, vol. 9236, pp. 253-269. Springer, Heidelberg (2015) · Zbl 1465.68290
[27] Lammich, P.: Refinement based verification of imperative data structures. In: Avigad, J., Chlipala, A. (eds.) CPP 2016, pp. 27-36. ACM, New York (2016)
[28] Lammich, P.; Lochbihler, A.; Kaufmann, M. (ed.); Paulson, LC (ed.), The Isabelle collections framework, No. 6172, 339-354, (2010), Heidelberg · Zbl 1291.68357
[29] Lammich, P.; Tuerk, T.; Beringer, L. (ed.); Felty, A. (ed.), Applying data refinement for monadic programs to Hopcroft’s algorithm, No. 7406, 166-182, (2012), Heidelberg · Zbl 1360.68757
[30] Leroy, X., A formally verified compiler back-end, J. Autom. Reason., 43, 363-446, (2009) · Zbl 1185.68215
[31] 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) · Zbl 1352.68034
[32] Lochbihler, A.: Light-weight containers. Archive of Formal Proofs. http://www.isa-afp.org/entries/Containers.shtml, Formal proof development (2013) · Zbl 1317.68219
[33] Lochbihler, A.; Blazy, S. (ed.); Paulin-Mohring, C. (ed.); Pichardie, D. (ed.), Light-weight containers for Isabelle: efficient, extensible, nestable, No. 7998, 116-132, (2013), Heidelberg · Zbl 1317.68219
[34] Lochbihler, A.; Bulwahn, L.; Eekelen, M. (ed.); Geuvers, H. (ed.); Schmalz, J. (ed.); Wiedijk, F. (ed.), Animating the formalised semantics of a Java-like language, No. 6898, 216-232, (2011), Heidelberg · Zbl 1342.68294
[35] Marić, F., Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL, Theor. Comput. Sci., 411, 4333-4356, (2010) · Zbl 1208.68205
[36] Musser, DR; Stepanov, AA; Gianni, P. (ed.), Generic programming, No. 358, 13-25, (1989), Heidelberg
[37] Nipkow, T.; Blanchette, JC (ed.); Merz, S. (ed.), Automatic functional correctness proofs for functional search trees, No. 9807, 307-322, (2016), Heidelberg · Zbl 06644751
[38] Nipkow, T.; Paulson, LC; Hurd, J. (ed.); Melham, T. (ed.), Proof pearl: defining functions over finite sets, No. 3603, 385-396, (2005), Heidelberg · Zbl 1152.68529
[39] 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)
[40] Peyton Jones, S.: Bulk types with class. In: Haskell Workshop 1997 (1997)
[41] Plotkin, GD, A note on inductive generalization, Mach. Intell., 5, 153-163, (1970) · Zbl 0219.68045
[42] 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)
[43] Schimpf, A.; Merz, S.; Smaus, J., Construction of Büchi automata for LTL model checking verified in Isabelle/HOL, No. 5674, 424-439, (2009), Heidelberg · Zbl 1252.68196
[44] Sozeau, M.; Oury, N.; Ait Mohamed, O. (ed.); Muñoz, C. (ed.); Tahar, S. (ed.), First-class type classes, No. 5170, 278-293, (2008), Heidelberg
[45] Sternagel, C.; Thiemann, R.; Urban, C. (ed.); Zhang, X. (ed.), Deriving comparators and show functions in Isabelle/HOL, No. 9236, 421-437, (2015), Heidelberg · Zbl 1465.68063
[46] 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)
[47] 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)
[48] 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) · Zbl 1252.68265
[49] Wirth, N., Program development by stepwise refinement, Commun. ACM, 14, 221-227, (1971) · Zbl 0214.43005
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.