Re: ANNOUNCE: SPARK toolset 6.1 now available

[rod@praxis-cs.co.uk (Rod Chapman)]

In answer to several points:

1) No - we don't currently allow 'Class anywhere, which means heterogeneous
lists are not supported directly in SPARK, although these may
be achieved by suitable hiding and abstraction.

2) SPARK does not currently include access type of any kind, since these
create some very difficult problems with the analysis of pointer effects
and aliasing.  If we can work out the analysis, then including some
support for general access types in future may in within scope.

3) Whether the restrictions implied by points 1) and 2) constitute
a "useful subset" of tagged types is really a matter of taste and outlook.
I guess time will tell if our users find the existing subset useful
for writing real programs of not...

Finally, in answer to Bob's point:

> If you have the entire program source code (which you should in a
> safety-critical context), then I don't see why a dispatching call is any
> more "uncertain" than a case statement.

But waiting until you have the "entire program" is _way_ too late!  One of
the major design goals of SPARK is to enable _constructive_ static
analysis of incomplete programs - hence the need for annotations
to strengthen the contracts in package specifications, for instance.

 - Rod Chapman, SPARK Team, Praxis Critical Systems.