Re: Clarification for SPARK postconditions on hidden subprograms.

[Phil Thornley <phil.jpthornley@googlemail.com>]

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