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.

SPARK GPL 2011 Released

If you’re in the game of producing secure and high integrity software, SPARK just might be what you’re looking for, and with the newly released SPARK GPL 2011 Edition it’s simple to try your hands at SPARK.

At the libre.adacore.com website, there’s a few community created SPARK projects available. These might be worth checking out for some examples on how to use SPARK. Another option is the AdaCore05 YouTube channel, where there are quite a few SPARK related videos to enjoy.

SPARK is developed by altran praxis.

AdaCore @ YouTube

I’m on of those people who enjoy tech-talks on video, so when I found out that AdaCore have a channel @ YouTube, it made my day.

Yes, I’m that easy to please. :o)

It’s a fairly busy channel, with regular updates. Some of the subjects dealt with are:

And of course lots more. Be sure to check it out!

SPARKRules Version 1.0

SparkSure has made the latest version of their SPARKRules software available:

SPARKRules is a utility program for managing proof libraries – which can contain user rule files and proof review files. SPARKRules allows user rules to be defined once and copied to Simplifier user rule files as required and supports the storage of proof review files in a separate library. The directories generated by the Examiner for the Simplifier are therefore not required for the storage of any permanent data.

You can read the full release announcement here.