Representing errno in SPARK

Representing errno in SPARK

[xorquewasp]

What is the correct way to model a pair of subprograms
that affect state completely outside of the SPARK program?

Specifically, in this case, I have a procedure:

  procedure Errno_Set (Code : Integer);
  pragma Import (C, Errno_Set, "posix_errno_set");

And a function:

  function Errno_Get return Integer;
  pragma Import (C, Errno_Get, "posix_errno_get");

The problem in this case is that the C variable 'errno' that these
subprograms refer to is completely external to the program but
the value of the Errno_Get function depends on it and therefore
the execution path the program takes depends on it. Those
closest I can find in the SPARK95 manual is "external own variables"
but even then, the variables are actually objects within the program:

package body Device
--# own State is        OldX,       -- state variable constituent
--#              in     StatusPort, -- external variable constituent
--#                 out Register;   -- external variable constituent
is
  OldX : Integer := 0; -- only component that needs or permits
initialization

  StatusPort : Integer;
  for StatusPort’Address use .........;
  Register : Integer;
  for Register’Address use ..........;

Re: Representing errno in SPARK

[roderick.chapman]

On Jun 9, 3:06 pm, xorquew...@googlemail.com wrote:
> What is the correct way to model a pair of subprograms
> that affect state completely outside of the SPARK program?

Create an abstraction of that state as a SPARK abstract own
variable, thus:

package POSIX
--# own Errno;

  procedure Errno_Set (Code : Integer);
  --# global out Errno;
  --# derives Errno from Code;
  pragma Import (C, Errno_Set, "posix_errno_set");

  function Errno_Get return Integer;
  --# global in Errno;
  pragma Import (C, Errno_Get, "posix_errno_get");

end POSIX;

Notes

1) POSIX.Errno is _never_ actually declared in SPARK - it's
just an abstraction for something that is outside the
SPARK boundary.

2) do NOT use an external own variable for this - these
are for _volatile_ states, which Errno is not...

3) You should read the "Informed Design Method" manual
(Informed.pdf) that comes with the SPARK distibution.

 - Rod

Re: Representing errno in SPARK

[xorquewasp]

roderick.chap...@googlemail.com wrote:
> Create an abstraction of that state as a SPARK abstract own
> variable, thus:
>
> package POSIX
> --# own Errno;
>
>   procedure Errno_Set (Code : Integer);
>   --# global out Errno;
>   --# derives Errno from Code;
>   pragma Import (C, Errno_Set, "posix_errno_set");
>
>   function Errno_Get return Integer;
>   --# global in Errno;
>   pragma Import (C, Errno_Get, "posix_errno_get");
>
> end POSIX;

Thank you, that's actually what I have here. The problem, however,
is that the package also has a body and SPARK doesn't seem to
like this:

$ spark posix-error.ads posix-error.adb
...
 304  end POSIX.Error;
          ^
***        Semantic Error    : 28: The own variable POSIX_errno does
not have a
           definition [SR95 7.2.3].

Is it, by any chance, an issue due to Errno_Get and Errno_Set being
defined in the private section of the package spec? I think probably
not...

>
> 2) do NOT use an external own variable for this - these
> are for _volatile_ states, which Errno is not...

Ok.

>
> 3) You should read the "Informed Design Method" manual
> (Informed.pdf) that comes with the SPARK distibution.
>

That's where I first got the idea for the above. The device
driver example in the SPARK95 manual made me think my
solution was incorrect, however.

Re: Representing errno in SPARK

[Phil Thornley]

On Jun 9, 4:02 pm, xorquew...@googlemail.com wrote:
...
>
> Thank you, that's actually what I have here. The problem, however,
> is that the package also has a body and SPARK doesn't seem to
> like this:
>
> $ spark posix-error.ads posix-error.adb
> ...
>  304  end POSIX.Error;
>           ^
> ***        Semantic Error    : 28: The own variable POSIX_errno does
> not have a
>            definition [SR95 7.2.3].
>
> Is it, by any chance, an issue due to Errno_Get and Errno_Set being
> defined in the private section of the package spec? I think probably
> not...

No it's not that.

What you are trying to do (by having other SPARK code in the body) is
mixing code that is inside and outside the 'SPARK boundary' in a
single package.

One possibility is to move the Errno abstraction and the two imported
operations to another package internal to POSIX (but this means having
an implementation for the POSIX versions of these subprograms). So:

1 - Remove the Import pragmas from POSIX spec.
2 - Create an internal package (eg POSIX.Internals) in the POSIX body
that has the Errno abstraction and the imported subprograms.
3 - In the refinement annotation on the POSIX body put "--# own Errno
is Internals.Errno;".
4 - Call through to these imported subprograms in the implementation
of the subprograms that you now have to provide.

(A second possibility is simply to create an Errno in the package body
with a comment that it isn't actually used by the code ...)

Phil Thornley

Re: Representing errno in SPARK

[xorquewasp]

Phil Thornley wrote:
> What you are trying to do (by having other SPARK code in the body) is
> mixing code that is inside and outside the 'SPARK boundary' in a
> single package.

I'm not entirely sure that's the case. The code in the body just maps
errno values to enumeration values. I'd consider this code to be on
the boundary at most (as opposed to any of it being "outside").

> One possibility is to move the Errno abstraction and the two imported
> operations to another package internal to POSIX (but this means having
> an implementation for the POSIX versions of these subprograms). So:
>
> 1 - Remove the Import pragmas from POSIX spec.
> 2 - Create an internal package (eg POSIX.Internals) in the POSIX body
> that has the Errno abstraction and the imported subprograms.
> 3 - In the refinement annotation on the POSIX body put "--# own Errno
> is Internals.Errno;".
> 4 - Call through to these imported subprograms in the implementation
> of the subprograms that you now have to provide.

Certainly a possibility.

> (A second possibility is simply to create an Errno in the package body
> with a comment that it isn't actually used by the code ...)

I did consider this but I wondered if this would cause issue with
SPARK's
flow analysis (as I'm only pretending to read/write a variable).

Re: Representing errno in SPARK

[Phil Thornley]

On 9 June, 17:11, xorquew...@googlemail.com wrote:
> Phil Thornley wrote:
> > What you are trying to do (by having other SPARK code in the body) is
> > mixing code that is inside and outside the 'SPARK boundary' in a
> > single package.
>
> I'm not entirely sure that's the case. The code in the body just maps
> errno values to enumeration values. I'd consider this code to be on
> the boundary at most (as opposed to any of it being "outside").
>
Well, the implementation of Errno is clearly outside the boundary and
any other code you are submitting to the Examiner must be inside the
boundary, by definition.
('On the boundary' would be a new concept for SPARK :-)
. . .

> > (A second possibility is simply to create an Errno in the package body
> > with a comment that it isn't actually used by the code ...)
>
> I did consider this but I wondered if this would cause issue with
> SPARK's
> flow analysis (as I'm only pretending to read/write a variable).

It shouldn't upset the flow analysis (but you will get compiler
warnings about unused data).

Phil Thornley