I want to create a divisor type or subtype of Float to catch divide by zero at compile time, but can’t figure out how to create this type or subtype.
subtype Positive_Float is Float range Float’Succ (0.0)…Float’Last;
Thanks [dmitry-kazakov]. Your answer gives me the positive half of the floats, but not the negative half. I need the union of range Float’First … Float’Pred(0,0) and Float’Succ(0.0) … Float’Last, but I don’t know how to express it.
In newer Ada you could try static predicate:
subtype Positive_Float is Float with
Static_Predicate => Positive_Float in Float'Range
and Positive_Float not in 0.0;
Float’Range excludes IEEE 754 non-numbers.
Thanks [dmitry-kazakov]. Your solution with Static_Predicate worked perfectly. Tomorrow I’ll research Static_Predicate, and how to incorporate digits into your subtype definition.
For private types you may want to look into Type_Invariant
too.
Can you explain “Positive_Float not in 0.0” ? Choice_simple_expression allows for a single value in a membership choice but wouldn’t Positive_Float = 0.0 do the same same ?
I know checking for equality with Float never make sense, but I don’t see how “in value” is different.
In this case “not in” is same as “/=” (ARM 4.5.2 2/3). [In-]equality makes sense in this case too because 0.0 is not treated as an interval, which is usually the case otherwise. So 1.0/0.0 would be zero divide (NaN) rather than negative (-Inf) or positive (+Inf) overflow.
One difference (not relevant in this case, though) is that membership tests are not operators, and work without the need for use
or use type
To expand on this a bit, I would recommend splitting this subtype up:
-- Assuming "with Interfaces".
-- Exclude non-numeric representations.
Subtype Real is Interfaces.IEEE_Float_64 range Interfaces.IEEE_Float_64'Range;
-- Exclude zeroes.
Subtype Divisor is Real
with Static_Predicate => Divisor not in (-0.0)..(+0.0);
IEEE +0 and -0 are both zero. Though they have different representation in all numeric operations they are 0. The following program (for Intel, big endian) illustrates the behavior:
with Ada.Text_IO; use Ada.Text_IO;
with Interfaces; use Interfaces;
with Ada.Unchecked_Conversion;
procedure Test is
function Convert is
new Ada.Unchecked_Conversion (Unsigned_64, IEEE_Float_64);
Z1 : IEEE_Float_64 := Convert (16#00000000_00000000#);
Z2 : IEEE_Float_64 := Convert (16#80000000_00000000#);
I2 : IEEE_Float_64 := 1.0/Z2;
begin
Put_Line ("Z1=" & Z1'Image);
Put_Line ("Z2=" & Z2'Image);
Put_Line ("Z1=Z2=" & Boolean'Image (Z1 = Z2));
Put_Line ("Z2 in 0.0=" & Boolean'Image (Z2 in 0.0));
Put_Line ("Z2 not in 0.0=" & Boolean'Image (Z2 not in 0.0));
Put_Line ("Z1'Succ=Z2'Succ=" & Boolean'Image (IEEE_Float_64'Succ (Z1) = IEEE_Float_64'Succ (Z2)));
Put_Line ("I2=" & I2'Image);
end Test;
The only difference is 'Image and non-numeric outcomes. E.g. 1.0/-0.0 gives negative infinity.
Yes, but there are subtle oddities about it. I know -0.0 = +0.0
, but this is because of the definition of IEEE754, not bitbatterns. I was doing something years and years ago (experimenting? some project? I don’t recall), and came across that datum. — I also recall a story from my dad who, in the navy, had heard about a fluid-dynamics simulator going odd (it was supposed to be symmetrical in the particular simulation, but wasn’t) and the culprit turned out to be negative-zero vs positive-/normal-zero, so it’s not entirely out in the weeds to conside it.
I had thought about finding my IEEE754-ish float-value/float-record implementation —I had the really short not-754 values used in one of the CUDA cards, IIRC— and using that for the example, but that would involve searching through all my archived code for little/no payoff.
I always argue with people using representation clauses instead of honest decoding hardware or network packets. But, again, in this case it does not matter. If you can see any difference, your code is broken, because at no point you should let an infinity appear.
Which is why you strip out the non-numeric values with:
Subtype Real is Interfaces.IEEE_Float_64 range Interfaces.IEEE_Float_64'Range;
Yes, this the standard advice for all floating-point types as any of them can be actually backed by IEEE 754 hardware.