paulk-asert opened a new pull request, #2665: URL: https://github.com/apache/groovy/pull/2665
…hat disagree with loop semantics A do-while runs its body before the first condition check, so its loop @Invariant only needs to be established by that first body execution; checking it at loop entry rejected valid loops. The invariant is now checked after each body execution for do-while (start-of-iteration placement is unchanged for for/while), and is intentionally not checked at break exits, matching standard loop-invariant semantics. A @Decreases variant was measured at the start and end of a single pass, which misses progress made by a classic for loop's update expression (it runs after the body end) and demanded non-negativity after the final body execution. The variant is now evaluated once at the start of each iteration: a scalar measure must be non-negative at entry (well-foundedness), and consecutive iteration-start values must strictly decrease. The cross-iteration state is hoisted into the block directly enclosing the loop; when the loop is not a direct child of a block (e.g. a braceless if branch), the previous single-pass measurement is kept as a fallback. -- This is an automated message from the Apache Git Service. To respond to the message, please log on to GitHub and use the URL above to go to the specific comment. To unsubscribe, e-mail: [email protected] For queries about this service, please contact Infrastructure at: [email protected]
