Skip to main content
main-content
Top

Hint

Swipe to navigate through the articles of this issue

03-10-2019

An Assertional Proof of Red–Black Trees Using Dafny

Journal:
Journal of Automated Reasoning
Author:
Ricardo Peña
Important notes
Work partially funded by the Spanish Ministry of Economy and Competitiveness, State Research Agency and the European Regional Development Fund under the grant TIN2017-86217-R (MINECO/AEI/FEDER, EU) and by Comunidad de Madrid as part of the program S2018/TCS-4339 (BLOQUES-CM) co-funded by EIE Funds of the EU.

Publisher's Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

Abstract

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.

Please log in to get access to this content

To get access to this content you need the following product:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 69.000 Bücher
  • über 500 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Umwelt
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Testen Sie jetzt 30 Tage kostenlos.

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 58.000 Bücher
  • über 300 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Testen Sie jetzt 30 Tage kostenlos.

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 50.000 Bücher
  • über 380 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Umwelt
  • Maschinenbau + Werkstoffe




Testen Sie jetzt 30 Tage kostenlos.

Literature
About this article

Premium Partner

    Image Credits