Clarification for SPARK postconditions on hidden subprograms.

Clarification for SPARK postconditions on hidden subprograms.

[xorque]

Hello.

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;

Is a postcondition on a hidden subprogram always assumed to have
been satisfied?

I ask because a subprogram that calls C_Open_Boundary and then
checks the return value against -1 can't seem to work out that
Error.Get_Error won't be equal to Error.Error_None when the value
is equal to -1.

Is it an error in my postcondition?

I will post more of the implementation if necessary, I just don't want
to spam the list with a 100 lines of VCGs...

Re: Clarification for SPARK postconditions on hidden subprograms.

[Phil Thornley]

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

Re: Clarification for SPARK postconditions on hidden subprograms.

[xorque]

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.

Re: Clarification for SPARK postconditions on hidden subprograms.

[Rod Chapman]

On Jun 26, 10:29 am, xorque <xorquew...@googlemail.com> wrote:
>   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.
> Does SPARK take issue with parameterless functions? Not unreasonable
> at all if this is the case, as SPARK should probably see them as
> constants.

Does this function have a global variable by any chance? If so, then
in annotations, you have to give additional actual parameters.
See section 3.3 of the Examiner_GenVCs manual.

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

We have very deliberately made the _entire_ set of manuals
available with the GPL release.  We hope in future to make
more tutorial-style information available on-line.

Yours,
 Rod Chapman, SPARK Team

Re: Clarification for SPARK postconditions on hidden subprograms.

[Phil Thornley]

On 26 June, 10:29, xorque <xorquew...@googlemail.com> wrote:
[...]
> 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.

But this isn't a parameterless function - it must have a global
annotation, something like:
function Error return Error_T;
--# global Stored_Error;

in which case the *proof* function Error has a parameter corresponding
to the global Stored_Error.
(Proof functions are not allowed global access to anything.)

Phil Thornley

Re: Clarification for SPARK postconditions on hidden subprograms.

[xorque]

Rod Chapman wrote:
>
> Does this function have a global variable by any chance? If so, then
> in annotations, you have to give additional actual parameters.
> See section 3.3 of the Examiner_GenVCs manual.

It does indeed. Checking now...

> We have very deliberately made the _entire_ set of manuals
> available with the GPL release.  We hope in future to make
> more tutorial-style information available on-line.

And they are certainly appreciated. They're not particularly
easy to search, however, especially when you're not exactly
sure what you're looking for. I'm really after more practical
examples - the case studies in the manuals are somewhat
abstract and Tokeneer is a bit on the large side. I look forward
to the tutorials.