Independent SPARK Support

February 2012: A Red-Black Tree with correctness proofs

The initial release of the red-black tree code, along with the key rules for proving correctness of the code that modifies the tree structure, is now available. This uses the same method to derive the proof rules as the earlier work reported below.

The current set of files for this data structure is in this archive.

Presentation at The Ada Connection, Edinburgh, 23rd June 2011

As described in the presentation, the second version of the Ordered List package (described below) has had all the proof rules validated using the SPADE Proof Checker.

The complete set of files for this version is in this archive.

SPARK High Integrity Data Structures

This is experimental work to asses the use of the SPARK language and tools to create data structures that are supported by partial proofs of correctness.  We believe that the examples provided here may demonstrate a practicable approach to achieving this.

The main difficulty in completing proofs of correctness for linked data structures comes from showing that the data structure invariant is maintained by all the operations that export the data structure.
The most obvious method for doing this is to show that each condition within the invariant is maintained - but for even quite simple data structures, such as a singly linked list, the number of proof rules rapidly becomes disproportionate to the (quite simple) code.

The alternative approach used here is less formal, but the effort involved in creating (and therefore validating) the rules is much more proportionate to the size of the code.  The basic approach is to specify the overall action of any operation exporting the data structure and to use this to create proof rules that confirm that the code has correctly modified the data structure.

At present the data structures with completed proofs are:

  • Stacks (since every exposition of data structures must include a stack)
  • Queues (which introduce the use of an abstraction function)
  • Ordered Lists (which require both an abstraction function and a data structure invariant)
  • Binary Search Trees (with an abstraction function and a data structure invariant)

All examples use simple integers as the element stored in the data structure.

There are two versions of the ordered lists:

  • The first version uses a 'head' component in the list type to indicate the first element of the list - this simplifies individual actions, but requires different code and proof rules for the two cases of operating on the first item and on any other item.
  • The second version uses an additional element in the relevant array as the head item, which is always present, so there is no code specific to the first item of the list.  This reduces the size of the code and the number of proof rules but increases their complexity.

The examples can be downloaded from the Download page.

All comments are welcomed on these examples and on the approach adopted, please mail all comments to phil@sparksure.com.