Re: Representing errno in SPARK

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

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