Sie befinden Sich nicht im Netzwerk der Universität Paderborn. Der Zugriff auf elektronische Ressourcen ist gegebenenfalls nur via VPN oder Shibboleth (DFN-AAI) möglich. mehr Informationen...
An Assertional Proof of Red–Black Trees Using Dafny
Ist Teil von
Journal of automated reasoning, 2020-04, Vol.64 (4), p.767-791
Ort / Verlag
Dordrecht: Springer Netherlands
Erscheinungsjahr
2020
Link zum Volltext
Quelle
SpringerLink (Online service)
Beschreibungen/Notizen
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.