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

@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		= {https://publikationen.bibliothek.kit.edu/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.}
}