On Tue, 15 Oct 2024 09:56:30 GMT, fabioromano1 <d...@openjdk.org> wrote:
>> I would say yes... The invariant `i == max{n : 5^(2^n) <= 5^remainingZeros}`
>> should be a sufficient condition to affirm it, indeed the 2nd loop ends when
>> `remainingZeros == 0`, so `remainingZeros >= z` implies `z == 0`...
>
>> Yes, I considered that as well. Not sure, however, if this is sufficient to
>> prove that intVal has been indeed divided by 5^z after the 2nd loop is
>> terminated.
>
> New comments just added should be sufficient to prove it.
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.
-------------
PR Review Comment: https://git.openjdk.org/jdk/pull/21323#discussion_r1804710014
