From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=ham
	autolearn_force=no version=3.4.4
X-Google-Language: ENGLISH,ASCII-7-bit
X-Google-Thread: 103376,744136b4fae1ff3e
X-Google-Attributes: gid103376,public
X-Google-ArrivalTime: 2003-03-21 07:03:19 PST
Path: 
 archiver1.google.com!news1.google.com!newsfeed.stanford.edu!headwall.stanford.edu!fu-berlin.de!uni-berlin.de!213.155.153.242!not-for-mail
From: Peter Amey <peter.amey@praxis-cs.co.uk>
Newsgroups: comp.lang.ada
Subject: Re: [Spark] Converting Arrays
Date: Fri, 21 Mar 2003 15:05:01 +0000
Organization: Praxis Critical Systems
Message-ID: <3E7B2A1D.CA3214D9@praxis-cs.co.uk>
References: <mailman.18.1047535488.308.comp.lang.ada@ada.eu.org>
 <3E7053AC.DB4C71DD@praxis-cs.co.uk> <slrnb70mhp.nv.lutz@taranis.iks-jena.de>
NNTP-Posting-Host: 213.155.153.242
Mime-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Content-Transfer-Encoding: 7bit
X-Trace: fu-berlin.de 1048258998 76922831 213.155.153.242 (16 [69815])
X-Mailer: Mozilla 4.73 [en] (Windows NT 5.0; U)
X-Accept-Language: en
Xref: archiver1.google.com comp.lang.ada:35599
Date: 2003-03-21T15:05:01+00:00
List-Id: <comp.lang.ada>



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