Copilot commented on code in PR #2563: URL: https://github.com/apache/groovy/pull/2563#discussion_r3294423451
########## subprojects/groovy-contracts/src/spec/doc/contracts-userguide.adoc: ########## @@ -141,6 +173,44 @@ include::../test/ContractsTest.groovy[tags=loop_invariant_multiple_example,inden * Assignment operators and state-changing postfix/prefix operators are not supported inside the closure. +== Loop Termination with @Decreases + +Where `@Invariant` on a loop asserts a condition that must hold _during_ iteration, +`@Decreases` asserts a condition that guarantees the loop will _terminate_: a +_loop variant_, also known as a termination measure. The closure must yield a +`Comparable` value (typically numeric) that strictly decreases on every iteration +and remains non-negative; if either part fails, a `LoopVariantViolation` +(a subclass of `AssertionError`) is thrown. Review Comment: The new `@Decreases` docs state the closure must yield/return a `Comparable`, but the implementation also supports `List` variants with lexicographic comparison (see `LoopVariantASTTransformation.checkDecreased` handling `prev instanceof List && curr instanceof List`). Please update this section (and the rules list) to document the `List`-of-`Comparable` option, or tighten the implementation/docs so they agree. -- 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]
