Google Groups no longer supports new Usenet posts or subscriptions. Historical content remains viewable.
Dismiss

ANN: SPARK: A red-black tree with correctness proofs

51 views
Skip to first unread message

Phil Thornley

unread,
Feb 24, 2012, 4:06:59 AM2/24/12
to

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.)

The archive can be downloaded from the Data Structures page at:
http://www.sparksure.com/

The readme for the release is:
http://www.sparksure.com/resources/rb_tree_V0_1_ReadMe.txt

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.)

The tree elements store a single integer value. A skelton implementation
of an Ordered_Set package is included to show how the tree package can
be used to create ordered containers for arbitrary element types. The
only additional requirement is for a Key function for the element type,
returning an integer value, where equivalent elements are defined as
those that have the same value for Key.

If you find this code useful then please let me know (there is an email
address with the material in the archive). In particular I am keen to
know whether anyone would like to have the annotations and rules that
complete the correctness proofs.


Cheers,

Phil Thornley

Thomas Løcke

unread,
Feb 24, 2012, 10:24:03 AM2/24/12
to
On 02/24/2012 10:06 AM, Phil Thornley wrote:
> The readme for the release is:
> http://www.sparksure.com/resources/rb_tree_V0_1_ReadMe.txt


I get a 404 for the ReadMe.txt.


--
Thomas Lųcke | tho...@12boo.net | http://12boo.net

Yannick Duchêne (Hibou57)

unread,
Feb 24, 2012, 10:52:34 AM2/24/12
to
Le Fri, 24 Feb 2012 16:24:03 +0100, Thomas Løcke <t...@ada-dk.org> a écrit:

> On 02/24/2012 10:06 AM, Phil Thornley wrote:
>> The readme for the release is:
>> http://www.sparksure.com/resources/rb_tree_V0_1_ReadMe.txt
>
>
> I get a 404 for the ReadMe.txt.

Parked domain like page for me.


--
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University

Simon Wright

unread,
Feb 24, 2012, 11:06:42 AM2/24/12
to
Thomas Løcke <t...@ada-dk.org> writes:

> On 02/24/2012 10:06 AM, Phil Thornley wrote:
>> The readme for the release is:
>> http://www.sparksure.com/resources/rb_tree_V0_1_ReadMe.txt
>
>
> I get a 404 for the ReadMe.txt.

The readme is in the archive.

Phil Clayton

unread,
Feb 24, 2012, 11:01:24 AM2/24/12
to
Everything downloads all right from
http://www.sparksure.com/resources/rb_tree_V0_1.zip

Phil Thornley

unread,
Feb 24, 2012, 12:16:20 PM2/24/12
to
In article <4f47ab93$0$281$1472...@news.sunsite.dk>, t...@ada-dk.org
says...
>
> On 02/24/2012 10:06 AM, Phil Thornley wrote:
> > The readme for the release is:
> > http://www.sparksure.com/resources/rb_tree_V0_1_ReadMe.txt
>
>
> I get a 404 for the ReadMe.txt.

Hmmm, I don't know how that happened. it was there and then it wasn't,
so my apologies.

It's there now - I've just checked.

Cheers,

Phil
0 new messages