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,FREEMAIL_FROM autolearn=ham autolearn_force=no version=3.4.4 X-Google-Thread: a07f3367d7,6d47e90d50b280da X-Google-Attributes: gida07f3367d7,public,usenet X-Google-NewGroupId: yes X-Google-Language: ENGLISH,ASCII-7-bit Path: g2news2.google.com!postnews.google.com!h28g2000yqd.googlegroups.com!not-for-mail From: xorquewasp@googlemail.com Newsgroups: comp.lang.ada Subject: Re: Representing errno in SPARK Date: Tue, 9 Jun 2009 09:11:28 -0700 (PDT) Organization: http://groups.google.com Message-ID: References: <95bb6d31-f4fe-47c9-9274-72382ffad7ba@j32g2000yqh.googlegroups.com> <8a00d4ad-0ca3-4908-abf0-4fa980decb19@o36g2000vbi.googlegroups.com> <90f77911-389b-484e-b7f8-5f4d5e81e84e@y7g2000yqa.googlegroups.com> <51812f56-6c0a-407a-9f53-98c9b15f957c@p4g2000vba.googlegroups.com> NNTP-Posting-Host: 81.86.41.187 Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit X-Trace: posting.google.com 1244563888 32065 127.0.0.1 (9 Jun 2009 16:11:28 GMT) X-Complaints-To: groups-abuse@google.com NNTP-Posting-Date: Tue, 9 Jun 2009 16:11:28 +0000 (UTC) Complaints-To: groups-abuse@google.com Injection-Info: h28g2000yqd.googlegroups.com; posting-host=81.86.41.187; posting-account=D9GNUgoAAAAmg7CCIh9FhKHNAJmHypsp User-Agent: G2/1.0 X-HTTP-UserAgent: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.9.0.7) Gecko/2009030814 Iceweasel/3.0.9 (Debian-3.0.9-1),gzip(gfe),gzip(gfe) Xref: g2news2.google.com comp.lang.ada:6398 Date: 2009-06-09T09:11:28-07:00 List-Id: Phil Thornley wrote: > What you are trying to do (by having other SPARK code in the body) is > mixing code that is inside and outside the 'SPARK boundary' in a > single package. I'm not entirely sure that's the case. The code in the body just maps errno values to enumeration values. I'd consider this code to be on the boundary at most (as opposed to any of it being "outside"). > One possibility is to move the Errno abstraction and the two imported > operations to another package internal to POSIX (but this means having > an implementation for the POSIX versions of these subprograms). So: > > 1 - Remove the Import pragmas from POSIX spec. > 2 - Create an internal package (eg POSIX.Internals) in the POSIX body > that has the Errno abstraction and the imported subprograms. > 3 - In the refinement annotation on the POSIX body put "--# own Errno > is Internals.Errno;". > 4 - Call through to these imported subprograms in the implementation > of the subprograms that you now have to provide. Certainly a possibility. > (A second possibility is simply to create an Errno in the package body > with a comment that it isn't actually used by the code ...) I did consider this but I wondered if this would cause issue with SPARK's flow analysis (as I'm only pretending to read/write a variable).