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=-0.9 required=5.0 tests=BAYES_00,FORGED_GMAIL_RCVD, FREEMAIL_FROM autolearn=no autolearn_force=no version=3.4.4 X-Google-Thread: 103376,6d79efdb8dde2c5a X-Google-NewGroupId: yes X-Google-Attributes: gida07f3367d7,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII Path: g2news1.google.com!postnews.google.com!y11g2000yqm.googlegroups.com!not-for-mail From: Phil Thornley Newsgroups: comp.lang.ada Subject: Re: SPARK : third example for Roesetta - reviewers welcome Date: Sun, 15 Aug 2010 22:51:42 -0700 (PDT) Organization: http://groups.google.com Message-ID: References: <589eea9a-0b14-4ae5-bf62-9abf4b33e7fb@i31g2000yqm.googlegroups.com> NNTP-Posting-Host: 80.177.171.182 Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable X-Trace: posting.google.com 1281937902 25974 127.0.0.1 (16 Aug 2010 05:51:42 GMT) X-Complaints-To: groups-abuse@google.com NNTP-Posting-Date: Mon, 16 Aug 2010 05:51:42 +0000 (UTC) Complaints-To: groups-abuse@google.com Injection-Info: y11g2000yqm.googlegroups.com; posting-host=80.177.171.182; posting-account=Fz1-yAoAAACc1SDCr-Py2qBj8xQ-qC2q User-Agent: G2/1.0 X-HTTP-UserAgent: Mozilla/4.0 (compatible; MSIE 8.0; Windows NT 6.1; WOW64; Trident/4.0; SLCC2; .NET CLR 2.0.50727; .NET CLR 3.5.30729; .NET CLR 3.0.30729; Media Center PC 6.0; .NET4.0C),gzip(gfe) Xref: g2news1.google.com comp.lang.ada:13385 Date: 2010-08-15T22:51:42-07:00 List-Id: On 15 Aug, 23:19, Yannick Duch=EAne (Hibou57) wrote: > Le Sun, 15 Aug 2010 22:57:21 +0200, Yannick Duch=EAne (Hibou57) =A0 > a =E9crit:> I saw something wrong in this vers= ion. > > Half false alarm, half True alarm: there is not way to have an empty arra= y =A0 > in SPARK. But I don't really enjoy the lack of a test for the empty array= =A0 > case, as a SPARK program is always a valid Ada program, and may be =A0 > compiled ignoring any SPARK error as well. This is perfectly possible to = =A0 > compile this passing Search an empty array. I would prefer SPARK allow = =A0 > empty array, and thus end into the creation of more robust units. > > So whatever SPARK says about it, I will get back the test for the empty = =A0 > array case. But if you put that test back in you are going to get flow errors for the added path - because Position will be exported but no value will be assigned to it. There's an interesting general point here - the 'SPARK' assumption is that the complete program is SPARK, so an empty array can't happen (it would require a index subtype with 'First > 'Last, which is a semantic error). However, if we start to see individual packages being put into the public domain then the calling program could well be just Ada, so an empty array becomes a possibility. My personal view is against changing the code of SPARK operations to handle non-SPARK constructs, because it will cause all sorts of problems (like the flow error in this case). For the examples in Rosetta Code we should just state that assumption in the accompanying text, since these code samples are for demonstrating language features rather than providing a source code library. But there is still a problem in the real world. Perhaps what is needed is an 'Ada to SPARK' interface to check for violations. One possiblity would be for the SPARK operation to become internal to the package and the body of the visible operation to check that the array is non-null and only call the internal operation if it's OK (the code of that operation will probably have to be hidden from the Examiner). Cheers, Phil