Re: Another question about fixed point types.

["Peter C. Chapin" <chapinp@acm.org>]

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.

Peter