KIT | KIT-Bibliothek | Impressum | Datenschutz

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.

Open Access Logo

Volltext §
DOI: 10.5445/IR/1000024828
Cover der Publikation
Zugehörige Institution(en) am KIT Institut für Theoretische Informatik (ITI)
Publikationstyp Proceedingsbeitrag
Publikationsjahr 2011
Sprache Englisch
Identifikator urn:nbn:de:swb:90-248287
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