Re: [Spark] Converting Arrays

["Grein, Christoph" <christoph.grein@eurocopter.com>]

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