Re: SPARK - an idea for high integrity data structures

[Phil Thornley <phil.jpthornley@gmail.com>]

On 20 July, 20:18, Simon Wright <si...@pushface.org> wrote:
> "Peter C. Chapin" <pcc482...@gmail.com> writes:
>
> > 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.
>
> An alternative might be to use an external macro processor to generate
> appropriate code complete with annotations. I guess that would depend on
> whether the proofs (a) didn't depend on the contained type, (b) didn't
> need (much) human intervention.

There are occasional hints about generics, and I guess that the
pressure for these is increasing. OTOH I know that some work on this
had already been done five years ago, so I'm not holding my breath.

There are a couple of options for a usable version of these data
structures before we get generics - it would be quite easy to add an
arbitrary data component, so that the proofs never depended on the
actual definition of that component and they would rerun with whatever
any user required as the type for that data.

Another option, which avoids changing anything in the data structure
code, is to make the client code responsible for storing the actual
data, and just to supply a key for storage/retrieval in the data
structure.  The operations then have output parameters that tell the
client code the index for the data in the array that the client
maintains.

I have both of these possibilities in mind if these exercises are
successfull - but am aware that they both place a constraint on the
data structure code: that no element in the data structure is ever
copied from one position to another.  For the first option this could
be grossly inefficient, if the data is large, and it would be invalid
for the second option.  (This means e.g. that I can't use the easy way
of deleting an internal node of a binary tree, it has to be done by
changing multiple tree links.)

Cheers,

Phil