Re: Representing errno in SPARK

[xorquewasp@googlemail.com]

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