Re: Silly and stupid post-condition or not ?

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

In article <wccliohots1.fsf@shell01.TheWorld.com>, 
bobduff@shell01.TheWorld.com says...
> 
> 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.
> 

Proofs don't really know anything about variables, only values. If a 
particular variable can take multiple values along a single execution 
path then either those values are defined by their expressions (which 
therefore replace the variable in the verification conditions) or if the 
expressions aren't known (usually because the variable is exported by 
one or more procedures) then the values are given different names, x__1, 
x__2, ...

Phil