I expect ENTIER and Math.Floor to do the same thing numerically, but ENTIER gives the answer 94906267 and the Math.Floor gives 94906268.0. I don't think this has a reasonable explanation in terms of rounding or TYPE ranges. The Math Docu says they are identical, except for some small print which does not apply here .
Some analysis: (m − 1/2)^2 = m^2 − m + 1/4, which is less than n = m^2 − m + 1. Thus the square root of n is more than m − 1/2, so should round to m.
Obviously, using 64 bit REALs, one does not expect that Math.Sqrt is exact. According to my investigations it gives 9490626.5 exactly to 64 bits, but rather less in its internal 80 bit format, maybe 1 80-bit LSB less.
Summary: The Math library gives the correct answer, but only by making two errors. It thinks the square root is less than 94906267.5, when it is actually more, but rounds it up anyway.
Most CP REAL functions/operations work to the internal 80-bit accuracy. Math.Floor seems to be an exception, and probably should be fixed to align with ENTIER.
Any other opinions?
Code: Select all
PROCEDURE EntierBug*;
VAR
m, n, v, w, y, z : REAL;
BEGIN
m := 94906268.;
n := m * m - m + 1.;
v := M.Sqrt (n);
w := M.Sqrt (n) - m;
y := ENTIER (M.Sqrt (n) + 0.5);
z := M.Floor (M.Sqrt (n) + 0.5);
HALT (60)
END EntierBug;
TRAP 60 (postcondition violated)
AaaKaraTest.EntierBug [00002AF1H]
.m REAL 94906268.0
.n REAL 9007199610781556.0
.v REAL 94906267.5
.w REAL -0.5000000013169483
.y REAL 94906267.0
.z REAL 94906268.0
Kernel.Call [000020BFH]