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

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.