* ANN: SPARK: A red-black tree with correctness proofs
@ 2012-02-24 9:06 Phil Thornley
2012-02-24 15:24 ` Thomas Løcke
0 siblings, 1 reply; 6+ messages in thread
From: Phil Thornley @ 2012-02-24 9:06 UTC (permalink / raw)
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
^ permalink raw reply [flat|nested] 6+ messages in thread
* Re: ANN: SPARK: A red-black tree with correctness proofs
2012-02-24 9:06 ANN: SPARK: A red-black tree with correctness proofs Phil Thornley
@ 2012-02-24 15:24 ` Thomas Løcke
2012-02-24 15:52 ` Yannick Duchêne (Hibou57)
` (2 more replies)
0 siblings, 3 replies; 6+ messages in thread
From: Thomas Løcke @ 2012-02-24 15:24 UTC (permalink / raw)
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 | thomas@12boo.net | http://12boo.net
^ permalink raw reply [flat|nested] 6+ messages in thread
* Re: ANN: SPARK: A red-black tree with correctness proofs
2012-02-24 15:24 ` Thomas Løcke
@ 2012-02-24 15:52 ` Yannick Duchêne (Hibou57)
2012-02-24 16:01 ` Phil Clayton
2012-02-24 16:06 ` Simon Wright
2012-02-24 17:16 ` Phil Thornley
2 siblings, 1 reply; 6+ messages in thread
From: Yannick Duchêne (Hibou57) @ 2012-02-24 15:52 UTC (permalink / raw)
Le Fri, 24 Feb 2012 16:24:03 +0100, Thomas Løcke <tl@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
^ permalink raw reply [flat|nested] 6+ messages in thread
* Re: ANN: SPARK: A red-black tree with correctness proofs
2012-02-24 15:52 ` Yannick Duchêne (Hibou57)
@ 2012-02-24 16:01 ` Phil Clayton
0 siblings, 0 replies; 6+ messages in thread
From: Phil Clayton @ 2012-02-24 16:01 UTC (permalink / raw)
Everything downloads all right from
http://www.sparksure.com/resources/rb_tree_V0_1.zip
^ permalink raw reply [flat|nested] 6+ messages in thread
* Re: ANN: SPARK: A red-black tree with correctness proofs
2012-02-24 15:24 ` Thomas Løcke
2012-02-24 15:52 ` Yannick Duchêne (Hibou57)
@ 2012-02-24 16:06 ` Simon Wright
2012-02-24 17:16 ` Phil Thornley
2 siblings, 0 replies; 6+ messages in thread
From: Simon Wright @ 2012-02-24 16:06 UTC (permalink / raw)
Thomas Løcke <tl@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.
^ permalink raw reply [flat|nested] 6+ messages in thread
* Re: ANN: SPARK: A red-black tree with correctness proofs
2012-02-24 15:24 ` Thomas Løcke
2012-02-24 15:52 ` Yannick Duchêne (Hibou57)
2012-02-24 16:06 ` Simon Wright
@ 2012-02-24 17:16 ` Phil Thornley
2 siblings, 0 replies; 6+ messages in thread
From: Phil Thornley @ 2012-02-24 17:16 UTC (permalink / raw)
In article <4f47ab93$0$281$14726298@news.sunsite.dk>, tl@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
^ permalink raw reply [flat|nested] 6+ messages in thread
end of thread, other threads:[~2012-02-24 17:16 UTC | newest]
Thread overview: 6+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2012-02-24 9:06 ANN: SPARK: A red-black tree with correctness proofs Phil Thornley
2012-02-24 15:24 ` Thomas Løcke
2012-02-24 15:52 ` Yannick Duchêne (Hibou57)
2012-02-24 16:01 ` Phil Clayton
2012-02-24 16:06 ` Simon Wright
2012-02-24 17:16 ` Phil Thornley
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox