Re: [Spark] Converting Arrays

[Peter Amey <peter.amey@praxis-cs.co.uk>]

"Grein, Christoph" wrote:
> 
> > The restriction that an out mode parameter can't be referenced in a
> > precondition seems to be the major cause of the difficulty, and I have
> > (reluctantly) come to the conclusion that the way to avoid explicit
> > rules for each instance of the output parameter is to pass the length as
> > an additional parameter, as Rod suggests.
> 
> I've never used SPARK myself, but I've read the PDF excerpt of Barnes' book with
> interest.
> 
> I'm wondering whether it wouldn't be feasible to change the SPARK rules in such
> a way to allow references of attributes of out parameters in preconditions.
> (Even in Ada 83, where reading of out parameters was forbidden, reading of their
> attributes and discriminants was allowed - and for a good reason.)

That specific topic is the subject of an open "performance report" and
we have been thinking about it for quite a while.  FWIW, it is not
something that has been identified as a significant problem for most
SPARK users; however, that is no reason to ignore it for ever!

Peter