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!s16g2000vbp.googlegroups.com!not-for-mail
From: Phil Thornley <phil.jpthornley@googlemail.com>
Newsgroups: comp.lang.ada
Subject: Re: Clarification for SPARK postconditions on hidden subprograms.
Date: Fri, 26 Jun 2009 00:55:25 -0700 (PDT)
Organization: http://groups.google.com
Message-ID: 
 <2bcddeb9-4823-469b-b496-d37f183fd929@s16g2000vbp.googlegroups.com>
References: <898abcf6-7315-4015-9d73-d9365a870294@v2g2000vbb.googlegroups.com>
NNTP-Posting-Host: 80.177.171.182
Mime-Version: 1.0
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: 7bit
X-Trace: posting.google.com 1246002948 13362 127.0.0.1 (26 Jun 2009 07:55:48
 GMT)
X-Complaints-To: groups-abuse@google.com
NNTP-Posting-Date: Fri, 26 Jun 2009 07:55:48 +0000 (UTC)
Complaints-To: groups-abuse@google.com
Injection-Info: s16g2000vbp.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 7.0; Windows NT 5.1;
	Trident/4.0; .NET CLR 1.1.4322; .NET CLR 2.0.50727),gzip(gfe),gzip(gfe)
Xref: g2news2.google.com comp.lang.ada:6626
Date: 2009-06-26T00:55:25-07:00
List-Id: <comp.lang.ada>

> I'm trying to work out what should be happening regarding the
> postcondition
> on a function with a hidden body:
>
>   function C_Open_Boundary
>     (File_Name : in String;
>      Flags     : in Open_Flag_Integer_t;
>      Mode      : in Permissions.Mode_Integer_t) return Descriptor_t
>   is
>     --# hide C_Open_Boundary
>     --# return D => (D  = -1 -> Error.Get_Error /= Error.Error_None) or
>     --#             (D /= -1 -> Error.Get_Error  = Error.Error_None);
>     ...
>   end C_Open_Boundary;

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.

If you move it to its normal place:

  function C_Open_Boundary
    (File_Name : in String;
     Flags     : in Open_Flag_Integer_t;
     Mode      : in Permissions.Mode_Integer_t) return Descriptor_t
    --# return D => (D  = -1 -> Error.Get_Error /= Error.Error_None)
or
    --#             (D /= -1 -> Error.Get_Error  = Error.Error_None);
  is
    --# hide C_Open_Boundary
    ...
  end C_Open_Boundary;

then the Examiner will now see it, but ...

> 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).

Also note that a return annotation is not simply another way of
writing a postcondition as it has no effect on the VCs generated
subsequently to the call.
(I did ask why this was once, but didn't fully understand the answer -
something to do with potential infinite recursion I think.)

So a return annotation on a hidden function is little more than a
comment.

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 ] .

Phil

(You might like to have a look at part 5 of the tutorial on proof
annotations at sparksure.com.)