On Thu, 17 Oct 2024 12:38:29 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^n` 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... ------------- PR Review Comment: https://git.openjdk.org/jdk/pull/21323#discussion_r1804743139
