Re: Silly and stupid post-condition or not ?

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

In article <wccsjipfhlb.fsf@shell01.TheWorld.com>, 
bobduff@shell01.TheWorld.com says...
> 
> Phil Thornley <phil.jpthornley@gmail.com> writes:
> 
> > The original SPARK Rationale says: "All Ada features which require 
> > dynamic storage allocation were ruled out, for several reasons. The 
> > specification and modelling of access type manipulations, which can 
> > involve aliasing, is extremely difficult; for programs using access 
> > types it may also be very difficult to achieve security ..., let alone 
> > verification."
> 
> Yes, aliasing makes analysis very difficult.  But...
> 
> > Remember that everything in a SPARK program must have a name, and that 
> > it is quite easy to implement dynamic storage for a single type by a 
> > simple array (access value <-> array index).
> 
> Yes, you can simulate pointers (access values) using arrays and
> indices.  This introduces the same aliasing issues, and the same
> dangling pointer (dangling index) issues.  A(X) can in general
> alias A(Y), and a compiler or analysis tool would like to prove
> X=Y, or prove X/=Y.

Yes - that's exactly what you *have* to do (not like) when you update 
two or more elements of an array (or prove your conclusion for either 
possibility of course).

> It seems like the aliasing issue is harder with indices, because you
> can do arithmetic one them, whereas you can't do arithmetic
> on pointers (in Ada).

I don't think that's a substantial point, the X and the Y can be 
expressions and that doesn't change anything.

>
> (I don't see why this has anything to do with having names.
> And not "everything" must have a name, but I know what you mean.)
>
> >... Furthermore when dealing
> > with dynamically sized data structures the invariant typically needs to
> > include predicates for the storage space that is not currently in use as
> > well as the storage that is.
>
> I'm not sure what you mean by that.  Could you give an example?

My code is managing the list of free elements, as well as the elements 
in the data structure, so I need to show that every array element that 
should be in the free list is there and that there isn't any element in 
the free list that is also in the data structure. If I'm using access 
values then I'm relying on the correctness of the compiled code/Ada run-
time handling of a storage pool, which probably has a lower level of 
integrity than I'm claiming for my code.

But the main point I was making is that there doesn't seem to be any 
major benefits to the SPARK user from adding access values to the 
language.

>
> ...
> SPARK may be great for certain types of systems, but I wouldn't
> want to write (say) a compiler in SPARK.

(Personally I wouldn't want to write a compiler at all .....)

Phil