On Thu, 17 Oct 2024 12:59:37 GMT, fabioromano1 <d...@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. > >> 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). ------------- PR Review Comment: https://git.openjdk.org/jdk/pull/21323#discussion_r1804899523
