Re: Another question about fixed point types.

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

On 29 Aug, 15:20, "Peter C. Chapin" <chap...@acm.org> wrote:
> On 2010-08-29 08:31, Phil Thornley wrote:
>
> > I was referring to the SPARK annotation that tells the Examiner which
> > predefined type the compiler will use as the base type of a type
> > declaration - it's needed for overflow checks and looks like:
>
> >    type An_Int is range -10_000 .. 10_000;
> >    --# assert An_Int'Base is Short_Integer;
>
> > where the range for Short_Integer is defined in the SPARK
> > configuration file
>
> I see, okay. So am I right in saying that one should provide one of
> these annotations for every scalar type definition in a SPARK program?
> I'm guessing that by doing so SPARK could prove more automatically since
> it would have more information. On the other hand it then becomes my
> responsibility to get the base type right.

It's all about completing the proofs of overflow checks - where the
Simplifier needs to know the range of the base type.  Up to and
including version 8.1.1 of last year, it was optional whether to
include these checks when VCs were generated for run-time checks
(generated only if you used the -exp qualifier for the Examiner).  But
in the recent 2010 version the overflow checks have become mandatory
and can't be turned off.

It's certainly a good idea to put them in - the coding standards of
last project I worked on required a base type assertion for every new
integer or floating point type declared.

You do have to get them right - OTOH it's always safe to use the
smallest possible range for the base type as it doesn't matter if you
prove the checks for a more restricted range.

For some compilers it's possible to check that the actual base type is
what you expected it to be.

Cheers,

Phil