From: rod.chapman@praxis-cs.co.uk (Rod Chapman)
Subject: Re: [Spark] Converting Arrays
Date: 12 Mar 2003 01:43:31 -0800
Date: 2003-03-12T09:43:31+00:00 [thread overview]
Message-ID: <cf2c6063.0303120143.2310b3d9@posting.google.com> (raw)
In-Reply-To: slrnb6rfur.nq.lutz@taranis.iks-jena.de
Lutz Donnerhacke <lutz@iks-jena.de> wrote in message news:<slrnb6rfur.nq.lutz@taranis.iks-jena.de>...
> * Rod Chapman wrote:
> > A common trick in this case is to use a local,
> > hidden procedure to initialise the out parameter:
>
> Cool idea. I read the book yesterday evening till midnight and came to the
> conclusion, that I have to replace Fullpath by a large constraint array.
> This was obviosly wrong. You can always switch off Spark checkings when
> running into trouble. :-/
>
> But how can I write the required pre conditions?
>
You can pass the Length of the Path parameter as an addition "in"
parameter. e.g.
procedure To_Fullname (S : in String;
Path : out Fullname;
Path_Length : in Natural);
--# derives Path from S, Path_Length;
--# pre S'Length < Path_Length;
Then a caller simply does:
To_Fullname (LS, P, P'Length);
or similar.
- Rod
I
next prev parent reply other threads:[~2003-03-12 9:43 UTC|newest]
Thread overview: 18+ messages / expand[flat|nested] mbox.gz Atom feed top
2003-03-10 17:06 [Spark] Converting Arrays Lutz Donnerhacke
2003-03-10 20:03 ` James S. Rogers
2003-03-10 22:33 ` Lutz Donnerhacke
2003-03-11 10:14 ` Rod Chapman
2003-03-11 10:51 ` Lutz Donnerhacke
2003-03-11 10:52 ` Lutz Donnerhacke
2003-03-11 20:46 ` JP Thornley
2003-03-12 8:43 ` Phil Thornley
2003-03-12 11:57 ` Lutz Donnerhacke
2003-03-12 18:46 ` JP Thornley
2003-03-13 10:14 ` Lutz Donnerhacke
2003-03-12 9:43 ` Rod Chapman [this message]
2003-03-12 10:15 ` Lutz Donnerhacke
-- strict thread matches above, loose matches on Subject: below --
2003-03-13 5:55 Grein, Christoph
2003-03-13 9:47 ` Peter Amey
2003-03-13 10:15 ` Lutz Donnerhacke
2003-03-21 15:05 ` Peter Amey
2003-03-21 15:17 ` Lutz Donnerhacke
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox