SPARK - an idea for high integrity data structures

SPARK - an idea for high integrity data structures

[Phil Thornley]

I have had a hobby project for a while to create SPARK versions of
data structures, supported by partial proofs of correctness.

However, if the proofs are tackled in the most obvious way then the
effort required to show that the relevant data structure invariant is
maintained by each operation grows out of all proportion to the size
of the code being proved, and it would be easier to validate the code
directly than to validate all the proof artefacts (annotations and
rules) that are generated for the proof.

So I have recently tried an alternative approach that shows some
potential for completing the proofs without requiring disproportionate
effort.

The idea is to determine, for each path through an operation that
exports a value of the data structure, the relationship between the
imported value and exported value and to create a single proof rule
that encapsulates that transformation.  If the rule proves the
postcondition VC generated for the path then the code implements the
transformation.

This is clearly a less rigorous approach than proving that the code
maintains all the individual conditions within the invariant, but it
is much more practicable.

As an example of this approach I have completed the proofs for an
ordered list of integers and put this up on http://www.sparksure.com
(I have included a stack and a queue as well, but neither of these
require data structure invariants).

I am very interested in all comments that anybody might have about
this idea - either here on cla or via the email address on the
website.

Phil Thornley

Re: SPARK - an idea for high integrity data structures

[Matteo Bordin]

Hi Phil,

you may be interested in having a look at Hi-Lite:

http://www.open-do.org/projects/hi-lite/

and in particular this discussion:

http://lists.forge.open-do.org/pipermail/hi-lite-discuss/2010-June/000129.html

Cheers,

Matteo



On Jul 20, 2:40 pm, Phil Thornley <phil.jpthorn...@gmail.com> wrote:
> I have had a hobby project for a while to create SPARK versions of
> data structures, supported by partial proofs of correctness.
>
> However, if the proofs are tackled in the most obvious way then the
> effort required to show that the relevant data structure invariant is
> maintained by each operation grows out of all proportion to the size
> of the code being proved, and it would be easier to validate the code
> directly than to validate all the proof artefacts (annotations and
> rules) that are generated for the proof.
>
> So I have recently tried an alternative approach that shows some
> potential for completing the proofs without requiring disproportionate
> effort.
>
> The idea is to determine, for each path through an operation that
> exports a value of the data structure, the relationship between the
> imported value and exported value and to create a single proof rule
> that encapsulates that transformation.  If the rule proves the
> postcondition VC generated for the path then the code implements the
> transformation.
>
> This is clearly a less rigorous approach than proving that the code
> maintains all the individual conditions within the invariant, but it
> is much more practicable.
>
> As an example of this approach I have completed the proofs for an
> ordered list of integers and put this up onhttp://www.sparksure.com
> (I have included a stack and a queue as well, but neither of these
> require data structure invariants).
>
> I am very interested in all comments that anybody might have about
> this idea - either here on cla or via the email address on the
> website.
>
> Phil Thornley

Re: SPARK - an idea for high integrity data structures

[Phil Thornley]

On 20 July, 15:33, Matteo Bordin <matteo.bor...@gmail.com> wrote:

> you may be interested in having a look at Hi-Lite:
>
> http://www.open-do.org/projects/hi-lite/
>
> and in particular this discussion:
>
> http://lists.forge.open-do.org/pipermail/hi-lite-discuss/2010-June/00...

Thanks for that - a very relevant discussion! However I did notice
this in one of the contributions:
"Our major focus is to make user proofs easy. Whether or not we prove
the implementations of such containers is to be decided latter and not
our current focus."

But my main interest is in proving the implementations so fortunately
I'm not directly duplicating this work.

Cheers,

Phil

Re: SPARK - an idea for high integrity data structures

[Peter C. Chapin]

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

Re: SPARK - an idea for high integrity data structures

[Simon Wright]

"Peter C. Chapin" <pcc482719@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.

Re: SPARK - an idea for high integrity data structures

[Phil Thornley]

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

Re: SPARK - an idea for high integrity data structures

[Peter C. Chapin]

On 2010-07-21 08:40, Phil Thornley wrote:

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

I attended a webinar on SPARK Pro 9.0 and a question about generics was
asked there. The answer was, "we are actively working on it, but I can't
give a specific release date or version." Of course it isn't completely
clear just what "actively working on it" means. Still, it sounds
encouraging.

Perhaps the work on the Hi-Lite project is helping to drive generics
support in SPARK. That's just wild speculation.

Peter

Re: SPARK - an idea for high integrity data structures

[Matteo Bordin]

On Jul 21, 3:23 pm, "Peter C. Chapin" <pcc482...@gmail.com> wrote:
> On 2010-07-21 08:40, Phil Thornley wrote:
>
> > 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.
>
> I attended a webinar on SPARK Pro 9.0 and a question about generics was
> asked there. The answer was, "we are actively working on it, but I can't
> give a specific release date or version." Of course it isn't completely
> clear just what "actively working on it" means. Still, it sounds
> encouraging.
>
> Perhaps the work on the Hi-Lite project is helping to drive generics
> support in SPARK. That's just wild speculation.

Hi-Lite has an open technical mailing list, so feel free to subscribe.
BTW, the Hi-Lite repository is open and accessible on the Open-DO
Forge.

Matteo