Re: [Spark] Converting Arrays

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

Lutz Donnerhacke wrote:
> 
> * Peter Amey wrote:
> > 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!
> 
> Thank you. Sorry for caming across this so early.

Ok, I feel nagged and have finally implemented something to solve the
problem you described.  The next release of the Examiner will allow
exported, formal parameters of unconstrained types to appear in
preconditions.  The idea will be to prove that the constraint provided
by the actual parameter in the calling environment is strong enough. 
The only useful preconditions that can be written will involve
attributes of the parameter.

e.g.

   procedure Copy (S : in     String;
                   D :    out String);
   --# derives D from S;
   --# pre D'Last >= S'Last;

is now provable for Copy ("AB", X); and Copy ("ABC", X);  but not
provable for Copy ("ABCD", X); 

regards

Peter and the SPARK team