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,c91e482ae6ca8d4b X-Google-Attributes: gida07f3367d7,public,usenet X-Google-NewGroupId: yes X-Google-Language: ENGLISH,ASCII-7-bit Path: g2news2.google.com!postnews.google.com!r25g2000vbn.googlegroups.com!not-for-mail From: xorque Newsgroups: comp.lang.ada Subject: Re: Clarification for SPARK postconditions on hidden subprograms. Date: Fri, 26 Jun 2009 02:29:06 -0700 (PDT) Organization: http://groups.google.com Message-ID: References: <898abcf6-7315-4015-9d73-d9365a870294@v2g2000vbb.googlegroups.com> <2bcddeb9-4823-469b-b496-d37f183fd929@s16g2000vbp.googlegroups.com> NNTP-Posting-Host: 62.249.247.223 Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit X-Trace: posting.google.com 1246008550 20977 127.0.0.1 (26 Jun 2009 09:29:10 GMT) X-Complaints-To: groups-abuse@google.com NNTP-Posting-Date: Fri, 26 Jun 2009 09:29:10 +0000 (UTC) Complaints-To: groups-abuse@google.com Injection-Info: r25g2000vbn.googlegroups.com; posting-host=62.249.247.223; 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:6633 Date: 2009-06-26T02:29:06-07:00 List-Id: Phil Thornley wrote: > The Examiner will ignore everything from the hide annotation to the > corresponding 'end'. So the Examiner is not seeing the return > annotation where you have it here. D'oh! Should have realised that... Moving the annotation has, of course, highlighted an apparent error on my part: 82 --# post ((Descriptor = -1) -> (Error.Get_Error /= Error.Error_None)) or ^ *** Semantic Error : 3: Incorrect number of actual parameters for call of subprogram Get_Error. 83 --# ((Descriptor /= -1) -> (Error.Get_Error = Error.Error_None)); ^ *** Semantic Error : 3: Incorrect number of actual parameters for call of subprogram Get_Error. Does SPARK take issue with parameterless functions? Not unreasonable at all if this is the case, as SPARK should probably see them as constants. > > Is a postcondition on a hidden subprogram always assumed to have > > been satisfied? > > Yes - the Examiner belives everything that you claim about hidden code > (but your return annotation doesn't reference any of the function > imports, which is unusual). Yes, I agree. I've changed it to a procedure. It's calling hidden C code and I'd written a binding to a function that was probably a bit too faithful to the original interface. > The value of a return annotation is that the Examiner ensures that the > function body is consistent with the annotation, so it then justifies > the definition of user rules for the function. > In this example the rules would be: > > rule(1): error__get_error <> error__error_none may_be_deduced_from > [ c_open_boundary(File, Flags, Mode) = -1 ] . > rule(2): error__get_error = error__error_none may_be_deduced_from > [ c_open_boundary(File, Flags, Mode) <> -1 ] . > I haven't got as far as writing user rules yet. I'm reading the documentation on them now. > (You might like to have a look at part 5 of the tutorial on proof > annotations at sparksure.com.) I hadn't made the connection until just now that you were the author of those. Thanks for writing those - there's a distinct lack of SPARK related info online.