Re: Silly and stupid post-condition or not ?

[Robert A Duff <bobduff@shell01.TheWorld.com>]

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.

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

> "Of course, the extent to which Ada must be simplified for high-
> integrity programming will be a matter of opinion: ...

Indeed.  

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

- Bob