On Thu, 17 Oct 2024 14:29:36 GMT, Raffaello Giulietti <rgiulie...@openjdk.org> wrote:
>>> The comments are OK. However, there seems to be no explicit relation >>> between the "running" vars used in the reasoning and the expected outcome. >>> >>> To clarify what I mean, let v0, z0 and s0 be the initial values at method >>> entry of intVal, z and scale, resp. At the exit of the method, the >>> following is supposed to hold by contract: >>> >>> v0 = intVal * 10^z0, s0 = scale + z0. >>> >>> At least to me, this is not apparent from the comments. >> >> @rgiulietti Starting from the facts `min(scale - preferredScale, powsOf2) >= >> remainingZeros` and `remainingZeros >= 2^i`, if `intVal % 5^(2^i) == 0`, >> then `(intVal * 2^powsOf2) % 10^(2^i) == 0`, so dividing `intVal` by >> `5^(2^i)` is legit (in the sense that we don't remove powers of 2 and we >> don't reduce the scale more than allowed) and exactly mimics the division >> `(intVal * 2^powsOf2) / 10^(2^i)` subtracting `2^i` from `powsOf2`. This >> allows to reduce the initial problem to the new values of the "running" vars >> after an iteration. So, I don't see the reason why it should not be apparent >> from the comments onestly... > > OK, let me reformulate the reasoning to check that we are in sync. > For simplicity, I'm assuming that the powers of 2 are _not_ stripped away, so > I'm using powers of 10 rather than powers of 5. Adding the powers of 2 > optimization to the reasoning is then straightforward. > > As above, let v0, z0 and s0 be the initial values at method entry of intVal, > z and scale, resp. > We need to return intVal = v0 / 10^z0, scale = s0 - z0. > > Let sexp be the running sum of all exponents exp inside both loops that lead > to zero remainders in the division intVal / 10^exp. > It should be easy to see that both "then" branches maintain > > z = z0 - sexp, intVal = v0 / 10^sexp, scale = s0 - sexp > > and that both branches in both loops maintain > > remainingZeros >= z > > When the 2nd loop exits, remainingZeros = 0, so z = 0. This means z0 = sexp, > intVal = v0 / 10^z0, scale = s0 - z0 (correctness). > > In addition, both loops exit for the reasons in the comments (termination) > and both loops require very few iterations (quality of service). @rgiulietti That's correct, although I prefer that the correctness is proved by "reducing the size of the problem" rather than "total number of removed powers", because it was the logic to prove implicitly the correctness of the older implementation, namely by reducing the number of zeros without exceeding the largest scale decreasing allowed. ------------- PR Review Comment: https://git.openjdk.org/jdk/pull/21323#discussion_r1804936621
