Re: Clarification for SPARK postconditions on hidden subprograms.

[xorque <xorquewasp@googlemail.com>]

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.