SPARK: A red-black tree with correctness proofs

From Phil Thornley of SparkSure fame we get a SPARK package implementing a red-black tree data structure:

A SPARK package implementing a red-black tree is now available and correctness proofs have been completed for the code. (SPARK correctness is, of course, partial correctness as there are no proofs of termination of the operations.)

In this version the Ada code is complete and all the mandatory SPARK annotations for information flow analysis are included, but the optional proof annotations within the operations in the package body have been excluded. (I have completed these, but they are not yet in a publishable form.)

You download the package here (ZIP) and you can read more about the SparkSure data structures here. The full release announcement is available here.

Leave a Reply