Prev: Determining value of record discriminant
Next: The Ada Connection - 20-24 June 2011, Edinburgh, UK
From: Simon Wright on 20 Jul 2010 15:18
"Peter C. Chapin" <pcc482719(a)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.
From: Phil Thornley on 21 Jul 2010 08:40
On 20 July, 20:18, Simon Wright <si...(a)pushface.org> wrote:
> "Peter C. Chapin" <pcc482...(a)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
From: Peter C. Chapin on 21 Jul 2010 09:23
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
From: Matteo Bordin on 22 Jul 2010 06:14
On Jul 21, 3:23 pm, "Peter C. Chapin" <pcc482...(a)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
First  |  Prev  | 
Pages: 1 2
Prev: Determining value of record discriminant
Next: The Ada Connection - 20-24 June 2011, Edinburgh, UK