RFR: 8341470: BigDecimal.stripTrailingZeros() optimization [v44]

[Raffaello Giulietti]

On Tue, 15 Oct 2024 09:56:30 GMT, fabioromano1 <duke at 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