KIT | KIT-Bibliothek | Impressum
Open Access Logo
URN: urn:nbn:de:swb:90-248287

Specification of Red-black Trees: Showcasing Dynamic Frames, Model Fields and Sequences

Bruns, Daniel

Complex data structures still pose a major challenge in specification and verification of object-oriented programs. Leino and Moskal have proposed a suite of benchmarks for verification tools, nicknamed "VACID-0". In contrast to similar papers, the tasks of VACID-0 do not only include verification in terms of an observable behavior but also of internal workings of algorithms and data structures. The arguably most difficult target are so-called red-black black trees. In this contribution, we present an implementation and specification in Java/JML* (i.e., KeY's extension to JML with dynamic frames). It makes use of several new features: first and foremost the dynamic frame theory, model fields, the sequence ADT, as well as some newly supported features from standard JML.

Zugehörige Institution(en) am KIT Institut für Theoretische Informatik (ITI)
Publikationstyp Proceedingsbeitrag
Jahr 2011
Sprache Englisch
Identifikator KITopen ID: 1000024828
Erschienen in Proceedings of the 10th KeY Symposium, August 26-27. Hrsg.: W. Ahrendt
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft KITopen Landing Page