Re: Silly and stupid post-condition or not ?

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

Phil Thornley <phil.jpthornley@gmail.com> writes:

> In article <wccsjipfhlb.fsf@shell01.TheWorld.com>, 
> bobduff@shell01.TheWorld.com says...
>> 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 meant that things like "X := X + 1;" changes what X points at.
That's allowed for indices, but not for pointers.

Suppose you want to know what might be modified by procedure P,
and P takes a parameter X that's a (pointer to a) linked list.
I'm not necessarily talking about SPARK, here.  I (or some tool)
can reason that P can only modify what X points at (transitively).
But if X is an index, and we're using some array as a hand-made
"heap", it's as if every heap object points to every other heap
object (including ones on the free list!), because P can say
X+1, X+2, X-1, etc.  OTOH, I suppose making it a private type helps.

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

I see.  Thanks.

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

True, although there are user-defined storage pools in Ada
(not in SPARK).

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

Writing a bootstrapped compiler is the coolest thing in
the world.  ;-)

- Bob