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

Reviewed Paper In Proceedings

Author(s):Daniel Bruns
In:10th KeY Symposium
Year:2011
URL:http://digbib.ubka.uni-karlsruhe.de/volltexte/1000024828

Abstract

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.

Note

Extended Abstract

BibTeX

@InProceedings{Bruns11,
  author	= {Daniel Bruns},
  title		= {Specification of Red-black Trees: Showcasing Dynamic
		   Frames, Model Fields and Sequences},
  note		= {Extended Abstract},
  year		= 2011,
  booktitle	= {10th {\KeY} Symposium},
  editor	= {Ahrendt, Wolfgang and Bubel, Richard},
  address	= {Nijmegen, the Netherlands},
  language	= {english},
  month		= aug,
  url		= {http://digbib.ubka.uni-karlsruhe.de/volltexte/1000024828},
  urn		= {urn:nbn:de:swb:90-248287},
  abstract	= {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$^\ast$ (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.}
}