On Tue, 15 Oct 2024 09:13:48 GMT, Raffaello Giulietti <rgiulie...@openjdk.org>
wrote:
>> 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.
>
> Anyway, if you find a nice proof please add it to the comments. The algorithm
> is quite sophisticated, so it needs one.
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`...
-------------
PR Review Comment: https://git.openjdk.org/jdk/pull/21323#discussion_r1800778340
