From: "Peter C. Chapin" <pcc482719@gmail.com>
Subject: Re: SPARK - an idea for high integrity data structures
Date: Tue, 20 Jul 2010 15:07:18 -0400
Date: 2010-07-20T15:07:18-04:00 [thread overview]
Message-ID: <4c45f3e7$0$2388$4d3efbfe@news.sover.net> (raw)
In-Reply-To: <9ac8feb3-5b79-41b1-a124-df211039c1bc@c10g2000yqi.googlegroups.com>
On 2010-07-20 08:40, Phil Thornley wrote:
> I have had a hobby project for a while to create SPARK versions of
> data structures, supported by partial proofs of correctness.
I can't comment right now on the approaches you mentioned, but I think
in general it's a great idea to work up some SPARK versions of classic
data structures (with proofs at some reasonable level). An open source
high integrity collections library would be a great contribution, it
seems to me.
Alas right now SPARK's limitations regarding generics seems like a bit
of a show stopper. Users would have to manually specialize each data
structure and re-do the proofs. Of course that would be easier than
building the code from scratch.
I know Praxis is working on generics support in SPARK. Once that was
ready it probably wouldn't be too hard for the original author of a high
integrity collections library to generalize the code as appropriate. At
least that would be my hope.
Peter
next prev parent reply other threads:[~2010-07-20 19:07 UTC|newest]
Thread overview: 8+ messages / expand[flat|nested] mbox.gz Atom feed top
2010-07-20 12:40 SPARK - an idea for high integrity data structures Phil Thornley
2010-07-20 14:33 ` Matteo Bordin
2010-07-20 19:02 ` Phil Thornley
2010-07-20 19:07 ` Peter C. Chapin [this message]
2010-07-20 19:18 ` Simon Wright
2010-07-21 12:40 ` Phil Thornley
2010-07-21 13:23 ` Peter C. Chapin
2010-07-22 10:14 ` Matteo Bordin
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox