×

zbMATH — the first resource for mathematics

An assertional proof of red-black trees using Dafny. (English) Zbl 07187046
Summary: Red-black trees are convenient data structures for inserting, searching, and deleting keys with logarithmic costs. However, keeping them balanced requires careful programming, and sometimes to deal with a high number of cases. In this paper, we present a functional version of a red-black tree variant called left-leaning, due to R. Sedgewick, which reduces the number of cases to be dealt with to a few ones. The code is rather concise, but reasoning about its correctness requires a rather large effort. We provide formal preconditions and postconditions for all the functions, prove their termination, and that the code satisfies its specifications. The proof is assertional, and consists of interspersing enough assertions among the code in order to help the verification tool to discharge the proof obligations. We have used the Dafny verification platform, which provides the programming language, the assertion language, and the verifier. To our knowledge, this is the first assertional proof of this data structure, and also one of the few ones including deletion.
MSC:
68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Adelson-Velskii, U.M., Landis, E.M.: An algorithm for the organization of information. In: Soviet Mathematics Doklady pp. 1259-1263 (1962)
[2] Andersson, A.: Balanced search trees made simple. In: Dehne F., Sack JR., Santoro N., Whitesides S. (eds) Algorithms and Data Structures. WADS 1993. Lecture Notes in Computer Science, vol 709, pp 60-71. Springer, Berlin (1993)
[3] Appel, A.W.: Efficient verified red-black trees p. http://www.cs.princeton.edu/ appel/papers/redblack.pdf (2011)
[4] Arge, L., Sedgewick, R., Seidel, R.: 08081 Abstracts collection-data structures. In: Arge, L., Sedgewick, R., Seidel, R. (eds.) Data Structures, 17.02.-22.02.2008, Dagstuhl Seminar Proceedings, vol. 08081. Internationales Begegnungs- und Forschungszentrum für Informatik (IBFI), Schloss Dagstuhl, Germany (2008). http://drops.dagstuhl.de/opus/volltexte/2008/1532/
[5] Bayer, R., Symmetric binary b-trees: data structure and maintenance algorithms, Acta Inf., 1, 290-306 (1972) · Zbl 0233.68009
[6] Bayer, R.; McCreight, EM, Organization and maintenance of large ordered indices, Acta Inf., 1, 173-189 (1972) · Zbl 0226.68008
[7] Bertot, Y.; Casteran, P., Interactive Theorem Proving and Program Development Coq’Art: The Calculus of Inductive Constructions (2004), New York: Springer, New York · Zbl 1069.68095
[8] Bobot, F., Filliâtre, J.C., Marché, C., Melquiond, G., Paskevich, A.: The Why3 platform. Version 0.86.1. University Paris-Sud, CNRS, Inria (2015)
[9] Bobot, F., Filliâtre, J.C., Marché, C., Paskevich, A.: Why3: shepherd your herd of provers. In: Boogie 2011: First International Workshop on Intermediate Verification Languages, pp. 53-64. Wroclaw, Poland (2011). https://hal.inria.fr/hal-00790310
[10] Cormen, TH; Leiserson, CE; Rivest, RL; Stein, C., Introduction to Algorithms (2001), Cambridge: MIT Press, Cambridge
[11] de Moura, L.M., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008 Proceedings. Lecture Notes in Computer Science, vol. 4963, pp. 337-340. Springer, New York (2008). 10.1007/978-3-540-78800-3-24
[12] Filliâtre, J., Letouzey, P.: Functors for proofs and programs. In: Schmidt, D.A. (ed.) Programming Languages and Systems, 13th European Symposium on Programming, ESOP 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004, Barcelona, Spain, March 29-April 2, 2004, Proceedings. Lecture Notes in Computer Science, vol. 2986, pp. 370-384. Springer, New York (2004). 10.1007/978-3-540-24725-8-26 · Zbl 1126.68475
[13] Guibas, L.J., Sedgewick, R.: A dichromatic framework for balanced trees. In: 19th Annual Symposium on Foundations of Computer Science, Ann Arbor, Michigan, USA, 16-18 October 1978, pp. 8-21. IEEE Computer Society (1978). 10.1109/SFCS.1978.3
[14] Guttag, JV; Horning, JJ; Garland, SJ; Jones, KD; Modet, A.; Wing, JM, Larch: Languages and Tools for Formal Specification. Texts and Monographs in Computer Science (1993), New York: Springer, New York
[15] Herbert, L.; Leino, K.; Quaresma, J.; Meyer, B.; Nordio, M., Using dafny, an automatic program verifier, Tools for Practical Software Verification, 156-181 (2012), Berlin: Springer, Berlin
[16] Jones, CB, Systematic Software Development Using VDM (1991), Upper Saddle River: Prentice Hall, Upper Saddle River
[17] Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning—16th International Conference, LPAR-16, Dakar, Senegal, April 25-May 1, 2010, Revised Selected Papers. Lecture Notes in Computer Science, vol. 6355, pp. 348-370. Springer, New York (2010). 10.1007/978-3-642-17511-4-20 · Zbl 1253.68095
[18] Leino, K.R.M.: Developing verified programs with Dafny. In: Brosgol, B., Boleng, J., Taft, S.T. (eds.) ACM Conference on High Integrity Language Technology, HILT’12, pp. 9-10. ACM (2012)
[19] Leino, KRM; Lucio, P., An assertional proof of the stability and correctness of natural mergesort, ACM Trans. Comput. Log., 17, 1, 6:1-6:22 (2015) · Zbl 1367.68080
[20] Nipkow, T.: Automatic functional correctness proofs for functional search trees. In: Blanchette, J., Merz, S. (eds) Interactive Theorem Proving. ITP 2016. Lecture Notes in Computer Science, vol. 9807, pp. 307-322. Springer, Cham (2016) · Zbl 06644751
[21] Nipkow, T.; Paulson, L.; Wenzel, M., Isabelle/HOL. A Proof Assistant for Higher-Order Logic (2002), New York: Springer, New York
[22] Okasaki, C., Red-black trees in a functional setting, J. Funct. Program., 9, 4, 471-477 (1999) · Zbl 0949.68518
[23] Polikarpova, N., Tschannen, J., Furia, C.A.: A fully verified container library. In: Bjørner, N., de Boer, F.S. (eds.) FM 2015: Formal Methods—20th International Symposium, Oslo, Norway, June 24-26, 2015 Proceedings. Lecture Notes in Computer Science, vol. 9109, pp. 414-434. Springer, New York (2015). 10.1007/978-3-319-19249-9-26
[24] Reade, CMP, Balanced trees with removals: an exercise in rewriting and proof, Sci. Comput. Program., 18, 181-204 (1992) · Zbl 0769.68032
[25] Sedgewick, R.; Wayne, K., Algorithms (2011), Boston: Addison-Wesley, Boston
[26] Stepney, S., Cooper, D., Woodcock, J.: More powerful Z data refinement: pushing the state of the art in industrial refinement. In: Bowen, J.P., Fett, A., Hinchey, M.G. (eds.) ZUM ’98: The Z Formal Specification Notation, 11th International Conference of Z Users, Berlin, Germany, September 24-26, 1998 Proceedings. Lecture Notes in Computer Science, vol. 1493, pp. 284-307. Springer, New York (1998). 10.1007/978-3-540-49676-2-20
[27] Weiss, MA, Data Structures and Problem Solving Using Java (1998), Boston: Addison Wesley, Boston
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.