Re: Another question about fixed point types.

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

On 29 Aug, 12:29, "Peter C. Chapin" <chap...@acm.org> wrote:
> On 2010-08-29 05:02, Phil Thornley wrote:
[...]
> > (and if this is SPARK, there's no base type assertion for fixed point
> > types...)
>
> I hope this doesn't sound like a stupid question but what do you mean by
> "base type assertion." Do you mean 'for Julian_Day'Base use ...'?

Peter,

(sorry for causing some confusion)

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 (which should contain copies of the declarations in
package Standard for your compiler).
See Section 3.3.2.3 of the Proof Manual in the GPL 2010 documentation.

These don't work for fixed point types are there aren't any fixed-
point types declared in Standard.

Cheers,

Phil