From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=0.7 required=5.0 tests=BAYES_00,FORGED_GMAIL_RCVD,
	FREEMAIL_FROM,REPLYTO_WITHOUT_TO_CC autolearn=no autolearn_force=no
	version=3.4.4
X-Google-Thread: 103376,26089aa3008dcac2,start
X-Google-NewGroupId: yes
X-Google-Attributes: gida07f3367d7,domainid0,public,usenet
X-Google-Language: ENGLISH,ASCII-7-bit
Received: by 10.68.213.68 with SMTP id nq4mr1696042pbc.2.1330074430948;
        Fri, 24 Feb 2012 01:07:10 -0800 (PST)
Path: 
 h9ni3168pbe.0!nntp.google.com!news1.google.com!goblin1!goblin.stu.neva.ru!txtfeed2.tudelft.nl!tudelft.nl!txtfeed1.tudelft.nl!dedekind.zen.co.uk!zen.net.uk!hamilton.zen.co.uk!reader02.news.zen.co.uk.POSTED!not-for-mail
From: Phil Thornley <phil.jpthornley@gmail.com>
Newsgroups: comp.lang.ada
Subject: ANN: SPARK: A red-black tree with correctness proofs
Date: Fri, 24 Feb 2012 09:06:59 -0000
Message-ID: <MPG.29b1639183a1f49f989687@news.zen.co.uk>
Reply-To: phil.jpthornley@gmail.com
MIME-Version: 1.0
User-Agent: MicroPlanet-Gravity/3.0.4
Organization: Zen Internet
NNTP-Posting-Host: 6c35d836.news.zen.co.uk
X-Trace: 
 DXC=bc]0`;AK]iPZhEmRS@T;C_YjZGX^207P[`<MJMoM3PF]nG1;R[DE_WW6JNOYoB;SJ^ieiN_8A5:XU5V1]K[n<V^Q
X-Complaints-To: abuse@zen.co.uk
Content-Type: text/plain; charset="us-ascii"
Content-Transfer-Encoding: 7bit
Date: 2012-02-24T09:06:59+00:00
List-Id: <comp.lang.ada>


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