On Tue, 15 Oct 2024 09:18:59 GMT, fabioromano1 <d...@openjdk.org> wrote:
>> 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`...
> 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.
-------------
PR Review Comment: https://git.openjdk.org/jdk/pull/21323#discussion_r1800837070
