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=-2.9 required=5.0 tests=BAYES_00,MAILING_LIST_MULTI autolearn=unavailable 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-12 22:05:09 PST Path: archiver1.google.com!news1.google.com!newsfeed.stanford.edu!news-spur1.maxwell.syr.edu!news.maxwell.syr.edu!newsfeed.icl.net!newsfeed.fjserv.net!opentransit.net!jussieu.fr!enst.fr!not-for-mail From: "Grein, Christoph" Newsgroups: comp.lang.ada Subject: Re: [Spark] Converting Arrays Date: Thu, 13 Mar 2003 06:55:38 +0100 (MET) Organization: ENST, France Message-ID: Reply-To: "Grein, Christoph" , "comp.lang.ada mail to news gateway" NNTP-Posting-Host: marvin.enst.fr Mime-Version: 1.0 Content-Type: TEXT/plain; charset=us-ascii X-Trace: avanie.enst.fr 1047535492 68435 137.194.161.2 (13 Mar 2003 06:04:52 GMT) X-Complaints-To: usenet@enst.fr NNTP-Posting-Date: Thu, 13 Mar 2003 06:04:52 +0000 (UTC) To: comp.lang.ada@ada.eu.org Return-Path: X-Authentication-Warning: mail.eurocopter.com: uucp set sender to using -f Content-MD5: Tx7b/Mu/xFjxUcDSGm/VVw== X-Mailer: dtmail 1.2.1 CDE Version 1.2.1 SunOS 5.6 sun4u sparc X-BeenThere: comp.lang.ada@ada.eu.org X-Mailman-Version: 2.1 Precedence: list List-Id: comp.lang.ada mail to news gateway List-Unsubscribe: , List-Post: List-Help: List-Subscribe: , Xref: archiver1.google.com comp.lang.ada:35280 Date: 2003-03-13T06:55:38+01:00 > 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.)