Another question about fixed point types.

Another question about fixed point types.

[Peter C. Chapin]

Hello!

Consider this type definition:

   type Julian_Day is delta 0.001 range 2_415_385.5 .. 2_489_665.0;

Now consider this function that is intended to return the (approximate)
interval between two Julian days in seconds:

   function Interval_Between
      (Left : Julian_Day; Right : Julian_Day) return Duration is
      Result : Duration;
   begin
      if Left > Right then
         Result := 86_400.0 * (Left - Right);
      else
         Result := 86_400.0 * (Right - Left);
      end if;
      return Result;
   end Interval_Between;

The difference 'Left - Right' is definitely not in the range of
Julian_Day. It is likely to be a small value and could even be zero. I
understand that the computation of 'Left - Right' will be done in
Julian_Day's base type but I'm unclear what that means to me.

It is my understanding that the compiler is allowed to choose a base
type that can only deal with the small-ish range of values between the
limits of Julian_Day. That range does not include zero. However, the
code above compiles and runs fine using GNAT GPL 2010. My test program
includes a case where Left and Right are the same so the difference is
zero. Is this code reliable or am I just seeing the effect of GNAT's
particular, implementation-specific choices?

Peter

P.S. The code above is a simplification of the real code, but I believe
it illustrates the question I have.

Re: Another question about fixed point types.

[Yannick Duchêne (Hibou57)]

Le Sun, 29 Aug 2010 00:45:16 +0200, Peter C. Chapin <chapinp@acm.org> a  
écrit:
> That range does not include zero. However, the
> code above compiles and runs fine using GNAT GPL 2010.
I have never used fixed point type in Ada (nor floats by the way, but will  
do in the future for sound synthesis).
However, I had a look at the reference, and here is what it says which may  
be relevant in your area:

ARM 2005 - 3.5.9 Fixed Point Types - says:

    12{base range (of a fixed point type) [partial]} The base range (see  
3.5)
    of a fixed point type is symmetric around zero, except possibly for an  
extra
    negative value in some implementations.

If it is symmetric around zero, that should explain your observations, as  
I would be very surprised if there would be provision for a hole  
somewhere. If it is symmetric around zero, and there is no two disjoint  
range, then this is include zero.

A tiny test program which would write first and last of the base type may  
tell more.

Hint: note the “possibly for an extra negative value in some  
implementations”, which may be important for you as you seems to require  
deep understanding of what's going on.

> P.S. The code above is a simplification of the real code, but I believe
> it illustrates the question I have.
Yes, it seems it illustrates fine.

-- 
“Dual licensing is the Perl's way to disinfect the GNU General Public  
Virus!” (anonymous)

Re: Another question about fixed point types.

[Phil Thornley]

On 28 Aug, 23:45, "Peter C. Chapin" <chap...@acm.org> wrote:
> Hello!
>
> Consider this type definition:
>
>    type Julian_Day is delta 0.001 range 2_415_385.5 .. 2_489_665.0;
>
> Now consider this function that is intended to return the (approximate)
> interval between two Julian days in seconds:
>
>    function Interval_Between
>       (Left : Julian_Day; Right : Julian_Day) return Duration is
>       Result : Duration;
>    begin
>       if Left > Right then
>          Result := 86_400.0 * (Left - Right);
>       else
>          Result := 86_400.0 * (Right - Left);
>       end if;
>       return Result;
>    end Interval_Between;
>
> The difference 'Left - Right' is definitely not in the range of
> Julian_Day. It is likely to be a small value and could even be zero. I
> understand that the computation of 'Left - Right' will be done in
> Julian_Day's base type but I'm unclear what that means to me.
>
> It is my understanding that the compiler is allowed to choose a base
> type that can only deal with the small-ish range of values between the
> limits of Julian_Day. That range does not include zero. However, the
> code above compiles and runs fine using GNAT GPL 2010. My test program
> includes a case where Left and Right are the same so the difference is
> zero. Is this code reliable or am I just seeing the effect of GNAT's
> particular, implementation-specific choices?

As Yannick points out, the base type will be symettric around zero.
(That extra negative value is allowed so that 2's complement machines
don't have work to exclude it.)

With that definition, the largest value that 'Small is allowed to take
is 2**-10, and the upper bound is between 2**21 and 2**22, so the
minimum number of bits for the base type will be 33 (which may or may
not be significant to you).

Assuming that the compiler is allocating 64 bits for the type, it can
choose any 'Small such that the actual range of the base type includes
at least the specified range, so it could be anywhere between
2**-10, with a range -(2**53) .. (2**63 - 1)*2**-10
and
2**-41 with a range -(2**22) .. (2**63 - 1)*2**-41

(and if this is SPARK, there's no base type assertion for fixed point
types...)

Cheers,

Phil

Re: Another question about fixed point types.

[Simon Wright]

"Peter C. Chapin" <chapinp@acm.org> writes:

> Consider this type definition:
>
>    type Julian_Day is delta 0.001 range 2_415_385.5 .. 2_489_665.0;

I'd add

   for Julian_Day'Small use 0.001;

Re: Another question about fixed point types.

[Peter C. Chapin]

On 2010-08-29 02:32, Yannick Duchêne (Hibou57) wrote:

> If it is symmetric around zero, that should explain your observations,
> as I would be very surprised if there would be provision for a hole
> somewhere. If it is symmetric around zero, and there is no two disjoint
> range, then this is include zero.
> 
> A tiny test program which would write first and last of the base type
> may tell more.

You're right. Thanks for pointing that out. Here is the range of
Julian_Day'Base that I obtained using a test program:

-9007199254740992.000 .. 9007199254740991.999

So my understanding was that for integral types the compiler is allowed
to allocate only the number of bits necessary to hold the range. For
example:

type Example_Type is range 1000 .. 1001;

The compiler is permitted (not required) to represent objects of type
Example_Type using only a single bit. But I guess this is a separate
issue. The base type, in which computations are done, might be wide even
if the compiler chooses to store the objects in a much small space.

So in my case as Phil explained computations on Julian Day are being
done, most likely, with a 64 bit type. Yet despite that, storage could
(perhaps) be using a smaller space since 64 bits is not needed to
represent the full range of Julian_Day at my specified resolution.

I understand that these details are compiler specific. However, it does
seem like my code, at least, should be portable in its effect.

Peter

Re: Another question about fixed point types.

[Peter C. Chapin]

On 2010-08-29 05:02, Phil Thornley wrote:

> With that definition, the largest value that 'Small is allowed to take
> is 2**-10, and the upper bound is between 2**21 and 2**22, so the
> minimum number of bits for the base type will be 33 (which may or may
> not be significant to you).

Using 64 bit integers for computations isn't too scary if it is
necessary for handling my required precision. I'd prefer not to have to
store the values in 64 bits if I can avoid it. It sounds like I might
have to take a little more control over the representation of certain
numeric types than I might ideally like. It's still a little early to be
sure (meaning I'm not going to worry about it until performance
measurements indicate that it's actually a problem). That said, I do
want to at least understand the issues.

> (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

Re: Another question about fixed point types.

[Phil Thornley]

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

Re: Another question about fixed point types.

[Jeffrey Carter]

On 08/29/2010 05:31 AM, Phil Thornley wrote:
>
> These don't work for fixed point types are there aren't any fixed-
> point types declared in Standard.

Duration.

-- 
Jeff Carter
"We call your door-opening request a silly thing."
Monty Python & the Holy Grail
17

--- news://freenews.netfront.net/ - complaints: news@netfront.net ---

Re: Another question about fixed point types.

[Stephen Leake]

"Peter C. Chapin" <chapinp@acm.org> writes:

>    type Julian_Day is delta 0.001 range 2_415_385.5 .. 2_489_665.0;
>
> Now consider this function that is intended to return the (approximate)
> interval between two Julian days in seconds:
>
>    function Interval_Between
>       (Left : Julian_Day; Right : Julian_Day) return Duration is
>       Result : Duration;
>    begin
>       if Left > Right then
>          Result := 86_400.0 * (Left - Right);
>       else
>          Result := 86_400.0 * (Right - Left);
>       end if;
>       return Result;
>    end Interval_Between;
>
> The difference 'Left - Right' is definitely not in the range of
> Julian_Day. It is likely to be a small value and could even be zero. 

Or negative.

> I understand that the computation of 'Left - Right' will be done in
> Julian_Day's base type but I'm unclear what that means to me.

This is no different than using Integer_16 to evaluate 30_000 * 30_000;
if an intermediate value is outside the base type range, you get
Constraint_Error at runtime.

> It is my understanding that the compiler is allowed to choose a base
> type that can only deal with the small-ish range of values between the
> limits of Julian_Day. That range does not include zero. However, the
> code above compiles and runs fine using GNAT GPL 2010. My test program
> includes a case where Left and Right are the same so the difference is
> zero. Is this code reliable or am I just seeing the effect of GNAT's
> particular, implementation-specific choices?

It is harder to guess what the compiler will choose as the base type
for fixed_point than for integer, but it's still just a guess; the base
type for Integer_16 could be 32 bits.

If you want to ensure that intermediate values are safe, you need to
widen the range of the type declaration, so the compiler is forced to
choose a safe base type. You could then use a subtype to provide a
restricted range:

    type Safe_Julian_Day is delta 0.001 range -2_489_665.0 .. 2_489_665.0;
    subtype Julian_Day is Safe_Julian_Day range 2_415_385.5 .. 2_489_665.0;

-- 
-- Stephe

Re: Another question about fixed point types.

[Peter C. Chapin]

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

Re: Another question about fixed point types.

[Phil Thornley]

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

Re: Another question about fixed point types.

[Peter C. Chapin]

On 2010-08-29 13:50, Phil Thornley wrote:

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

Thanks, this is good to know.

Peter

Re: Another question about fixed point types.

[Mark Lorenzen]

On 29 Aug., 19:50, Phil Thornley <phil.jpthorn...@gmail.com> wrote:
>
> 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.
>

It would be handy if the Examiner would insert safe default base type
assertions just as it inserts default loop invariants.

- Mark L