Document Open Access Logo

Proof Pearl: Purely Functional, Simple and Efficient Priority Search Trees and Applications to Prim and Dijkstra

Authors Peter Lammich , Tobias Nipkow

PDF
Thumbnail PDF

File

LIPIcs.ITP.2019.23.pdf
  • Filesize: 440 kB
  • 18 pages

Document Identifiers

Author Details

Peter Lammich
  • The University of Manchester, UK
Tobias Nipkow
  • Technical University Munich, Germany

Funding

  • Lammich, Peter: DFG Grant LA 3292/1 "Verifizierte Model Checker" and VeTSS grant "Formal Verification of Information Flow Security for Relational Databases"
  • Nipkow, Tobias: Supported by DFG Koselleck grant NI 491/16-1.

Cite As Get BibTex

Peter Lammich and Tobias Nipkow. Proof Pearl: Purely Functional, Simple and Efficient Priority Search Trees and Applications to Prim and Dijkstra. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 23:1-23:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) https://doi.org/10.4230/LIPIcs.ITP.2019.23

Abstract

The starting point of this paper is a new, purely functional, simple and efficient data structure combining a search tree and a priority queue, which we call a priority search tree. The salient feature of priority search trees is that they offer a decrease-key operation, something that is missing from other simple, purely functional priority queue implementations. As two applications of this data structure we verify purely functional, simple and efficient implementations of Prim’s and Dijkstra’s algorithms. This constitutes the first verification of an executable and even efficient version of Prim’s algorithm.

Subject Classification

ACM Subject Classification
  • Theory of computation → Data structures design and analysis
Keywords
  • Priority queue
  • Dijkstra’s algorithm
  • Prim’s algorithm
  • verification
  • Isabelle

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Jean-Raymond Abrial, Dominique Cansell, and Dominique Méry. Formal Derivation of Spanning Trees Algorithms. In Didier Bert, Jonathan P. Bowen, Steve King, and Marina Waldén, editors, ZB 2003: Formal Specification and Development in Z and B, Third International Conference of B and Z Users, Turku, Finland, June 4-6, 2003, Proceedings, volume 2651 of Lecture Notes in Computer Science, pages 457-476. Springer, 2003. URL: https://doi.org/10.1007/3-540-44880-2_27.
  2. Stefan Berghofer and Tobias Nipkow. Executing Higher Order Logic. In P. Callaghan, Z. Luo, J. McKinna, and R. Pollack, editors, Types for Proofs and Programs (TYPES 2000), volume 2277 of LNCS, pages 24-40. Springer, 2002. Google Scholar
  3. Sascha Böhme, K. Rustan M. Leino, and Burkhart Wolff. HOL-Boogie - An Interactive Prover for the Boogie Program-Verifier. In Otmane Ait Mohamed, César Muñoz, and Sofiène Tahar, editors, Theorem Proving in Higher Order Logics, pages 150-166, Berlin, Heidelberg, 2008. Springer Berlin Heidelberg. Google Scholar
  4. Arthur Charguéraud. Characteristic Formulae for the Verification of Imperative Programs. In Proceedings of the 16th ACM SIGPLAN International Conference on Functional Programming, ICFP '11, pages 418-430, New York, NY, USA, 2011. ACM. URL: https://doi.org/10.1145/2034773.2034828.
  5. Ching-Tsun Chou. A Formal Theory of Undirected Graphs in Higher-Order Logic. In Thomas F. Melham and Juanito Camilleri, editors, Higher Order Logic Theorem Proving and Its Applications, 7th International Workshop, Valletta, Malta, September 19-22, 1994, Proceedings, volume 859 of Lecture Notes in Computer Science, pages 144-157. Springer, 1994. URL: https://doi.org/10.1007/3-540-58450-1_40.
  6. Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest, and Clifford Stein. Introduction to Algorithms. MIT Press, 2009. Google Scholar
  7. E. W. Dijkstra. A note on two problems in connexion with graphs. Numerische Mathematik, 1(1):269-271, December 1959. URL: https://doi.org/10.1007/BF01386390.
  8. Jean-Christophe Filliâtre. Dijkstra’s shortest path algorithm. From the Toccata gallery, URL: http://toccata.lri.fr/gallery/dijkstra.en.html.
  9. Jean-Christophe Filliâtre and Andrei Paskevich. Why3 - Where Programs Meet Provers. In ESOP, volume 7792. Springer, March 2013. URL: https://hal.inria.fr/hal-00789533.
  10. Walter Guttmann. Relation-Algebraic Verification of Prim’s Minimum Spanning Tree Algorithm. In Augusto Sampaio and Farn Wang, editors, Theoretical Aspects of Computing - ICTAC 2016 - 13th International Colloquium, Taipei, Taiwan, ROC, October 24-31, 2016, Proceedings, volume 9965 of Lecture Notes in Computer Science, pages 51-68, 2016. URL: https://doi.org/10.1007/978-3-319-46750-4_4.
  11. Florian Haftmann and Tobias Nipkow. Code Generation via Higher-Order Rewrite Systems. In M. Blume, N. Kobayashi, and G. Vidal, editors, Functional and Logic Programming (FLOPS 2010), volume 6009 of LNCS, pages 103-117. Springer, 2010. Google Scholar
  12. Ralf Hinze. A Simple Implementation Technique for Priority Search Queues. In Benjamin C. Pierce, editor, Proceedings of the Sixth ACM SIGPLAN International Conference on Functional Programming (ICFP '01), Firenze (Florence), Italy, September 3-5, 2001., pages 110-121. ACM, 2001. URL: https://doi.org/10.1145/507635.507650.
  13. Ralf Hinze and Ross Paterson. Finger Trees: A Simple General-purpose Data Structure. Journal of Functional Programming, 16(2):197-217, 2006. Google Scholar
  14. URL: http://isabelle.in.tum.de/library/HOL/HOL-Data_Structures/RBT.html.
  15. Peter Lammich. Refinement based verification of imperative data structures. In Jeremy Avigad and Adam Chlipala, editors, CPP 2016, pages 27-36. ACM, 2016. Google Scholar
  16. Peter Lammich and Tobias Nipkow. Priority Search Trees. Archive of Formal Proofs, 2019. Formal proof development. URL: http://isa-afp.org/entries/Priority_Search_Trees.html.
  17. Peter Lammich and Tobias Nipkow. Purely Functional, Simple, and Efficient Implementation of Prim and Dijkstra. Archive of Formal Proofs, 2019. , Formal proof development. URL: http://isa-afp.org/entries/Prim_Dijkstra_Simple.html.
  18. Peter Lammich and Thomas Tuerk. Applying Data Refinement for Monadic Programs to Hopcroft’s Algorithm. In Proc. of ITP, volume 7406 of LNCS, pages 166-182. Springer, 2012. Google Scholar
  19. Edward M. McCreight. Priority Search Trees. SIAM J. Comput., 14(2):257-276, 1985. URL: https://doi.org/10.1137/0214021.
  20. Tobias Nipkow and Gerwin Klein. Concrete Semantics with Isabelle/HOL. Springer, 2014. URL: http://concrete-semantics.org.
  21. Tobias Nipkow, Lawrence Paulson, and Markus Wenzel. Isabelle/HOL - A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer, 2002. Google Scholar
  22. Benedikt Nordhoff, Stefan Körner, and Peter Lammich. Finger Trees. In Gerwin Klein, Tobias Nipkow, and Lawrence Paulson, editors, Archive of Formal Proofs. http://afp.sf.net/entries/Tree-Automata.shtml, October 2010. Formal proof development.
  23. Benedikt Nordhoff and Peter Lammich. Dijkstra’s Shortest Path Algorithm. Archive of Formal Proofs, January 2012. , Formal proof development. URL: http://isa-afp.org/entries/Dijkstra_Shortest_Path.html.
  24. Lars Noschinski. A Graph Library for Isabelle. Mathematics in Computer Science, 9(1):23-39, 2015. URL: https://doi.org/10.1007/s11786-014-0183-z.
  25. Chris Okasaki. Purely Functional Data Structures. Cambridge University Press, 1998. Google Scholar
  26. R. C. Prim. Shortest connection networks and some generalizations. The Bell System Technical Journal, 36(6):1389-1401, November 1957. URL: https://doi.org/10.1002/j.1538-7305.1957.tb01515.x.
  27. Matthieu Sozeau. Program-ing Finger Trees in Coq. SIGPLAN Not., 42(9):13-24, October 2007. URL: https://doi.org/10.1145/1291220.1291156.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact