This is an automated email from the ASF dual-hosted git repository.
paulk pushed a commit to branch master
in repository https://gitbox.apache.org/repos/asf/groovy.git
The following commit(s) were added to refs/heads/master by this push:
new 5b65cd7420 GROOVY-11890: groovy-contracts could support "@Decreases"
5b65cd7420 is described below
commit 5b65cd742065bfd2d9bcb158f90f22f014435967
Author: Paul King <[email protected]>
AuthorDate: Tue Mar 31 16:12:36 2026 +1000
GROOVY-11890: groovy-contracts could support "@Decreases"
---
.../src/main/java/groovy/contracts/Decreases.java | 63 ++++++
.../groovy/contracts/LoopVariantViolation.java | 59 ++++++
.../ast/LoopVariantASTTransformation.java | 233 +++++++++++++++++++++
.../contracts/tests/inv/LoopDecreasesTests.groovy | 171 +++++++++++++++
4 files changed, 526 insertions(+)
diff --git
a/subprojects/groovy-contracts/src/main/java/groovy/contracts/Decreases.java
b/subprojects/groovy-contracts/src/main/java/groovy/contracts/Decreases.java
new file mode 100644
index 0000000000..dace842070
--- /dev/null
+++ b/subprojects/groovy-contracts/src/main/java/groovy/contracts/Decreases.java
@@ -0,0 +1,63 @@
+/*
+ * Licensed to the Apache Software Foundation (ASF) under one
+ * or more contributor license agreements. See the NOTICE file
+ * distributed with this work for additional information
+ * regarding copyright ownership. The ASF licenses this file
+ * to you under the Apache License, Version 2.0 (the
+ * "License"); you may not use this file except in compliance
+ * with the License. You may obtain a copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing,
+ * software distributed under the License is distributed on an
+ * "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY
+ * KIND, either express or implied. See the License for the
+ * specific language governing permissions and limitations
+ * under the License.
+ */
+package groovy.contracts;
+
+import groovy.lang.annotation.ExtendedElementType;
+import groovy.lang.annotation.ExtendedTarget;
+import org.apache.groovy.lang.annotation.Incubating;
+import org.codehaus.groovy.transform.GroovyASTTransformationClass;
+
+import java.lang.annotation.ElementType;
+import java.lang.annotation.Retention;
+import java.lang.annotation.RetentionPolicy;
+import java.lang.annotation.Target;
+
+/**
+ * Specifies a termination measure for a loop. The closure must return a
+ * {@link Comparable} value that <em>strictly decreases</em> on every
+ * iteration and remains non-negative (i.e., {@code >= 0} for numeric types).
+ * <p>
+ * At runtime, the expression is evaluated at the start and end of each
+ * iteration. A {@link org.apache.groovy.contracts.LoopVariantViolation
+ * LoopVariantViolation} is thrown if:
+ * <ul>
+ * <li>the value did not decrease, or</li>
+ * <li>the value became negative.</li>
+ * </ul>
+ * <p>
+ * Example:
+ * <pre>
+ * int n = 10
+ * {@code @Decreases}({ n })
+ * while (n > 0) {
+ * n--
+ * }
+ * </pre>
+ *
+ * @since 6.0.0
+ * @see Invariant
+ */
+@Retention(RetentionPolicy.RUNTIME)
+@Target(ElementType.TYPE)
+@ExtendedTarget(ExtendedElementType.LOOP)
+@Incubating
+@GroovyASTTransformationClass("org.apache.groovy.contracts.ast.LoopVariantASTTransformation")
+public @interface Decreases {
+ Class value();
+}
diff --git
a/subprojects/groovy-contracts/src/main/java/org/apache/groovy/contracts/LoopVariantViolation.java
b/subprojects/groovy-contracts/src/main/java/org/apache/groovy/contracts/LoopVariantViolation.java
new file mode 100644
index 0000000000..b9905debc9
--- /dev/null
+++
b/subprojects/groovy-contracts/src/main/java/org/apache/groovy/contracts/LoopVariantViolation.java
@@ -0,0 +1,59 @@
+/*
+ * Licensed to the Apache Software Foundation (ASF) under one
+ * or more contributor license agreements. See the NOTICE file
+ * distributed with this work for additional information
+ * regarding copyright ownership. The ASF licenses this file
+ * to you under the Apache License, Version 2.0 (the
+ * "License"); you may not use this file except in compliance
+ * with the License. You may obtain a copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing,
+ * software distributed under the License is distributed on an
+ * "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY
+ * KIND, either express or implied. See the License for the
+ * specific language governing permissions and limitations
+ * under the License.
+ */
+package org.apache.groovy.contracts;
+
+/**
+ * Thrown whenever a loop variant (decreases/increases) violation occurs.
+ *
+ * @see AssertionViolation
+ * @since 6.0.0
+ */
+public class LoopVariantViolation extends AssertionViolation {
+
+ public LoopVariantViolation() {
+ }
+
+ public LoopVariantViolation(Object o) {
+ super(o);
+ }
+
+ public LoopVariantViolation(boolean b) {
+ super(b);
+ }
+
+ public LoopVariantViolation(char c) {
+ super(c);
+ }
+
+ public LoopVariantViolation(int i) {
+ super(i);
+ }
+
+ public LoopVariantViolation(long l) {
+ super(l);
+ }
+
+ public LoopVariantViolation(float f) {
+ super(f);
+ }
+
+ public LoopVariantViolation(double d) {
+ super(d);
+ }
+}
diff --git
a/subprojects/groovy-contracts/src/main/java/org/apache/groovy/contracts/ast/LoopVariantASTTransformation.java
b/subprojects/groovy-contracts/src/main/java/org/apache/groovy/contracts/ast/LoopVariantASTTransformation.java
new file mode 100644
index 0000000000..77902c1acb
--- /dev/null
+++
b/subprojects/groovy-contracts/src/main/java/org/apache/groovy/contracts/ast/LoopVariantASTTransformation.java
@@ -0,0 +1,233 @@
+/*
+ * Licensed to the Apache Software Foundation (ASF) under one
+ * or more contributor license agreements. See the NOTICE file
+ * distributed with this work for additional information
+ * regarding copyright ownership. The ASF licenses this file
+ * to you under the Apache License, Version 2.0 (the
+ * "License"); you may not use this file except in compliance
+ * with the License. You may obtain a copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing,
+ * software distributed under the License is distributed on an
+ * "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY
+ * KIND, either express or implied. See the License for the
+ * specific language governing permissions and limitations
+ * under the License.
+ */
+package org.apache.groovy.contracts.ast;
+
+import groovy.contracts.Decreases;
+import org.apache.groovy.contracts.LoopVariantViolation;
+import org.codehaus.groovy.ast.ASTNode;
+import org.codehaus.groovy.ast.AnnotationNode;
+import org.codehaus.groovy.ast.ClassHelper;
+import org.codehaus.groovy.ast.expr.BooleanExpression;
+import org.codehaus.groovy.ast.expr.ClosureExpression;
+import org.codehaus.groovy.ast.expr.Expression;
+import org.codehaus.groovy.ast.stmt.BlockStatement;
+import org.codehaus.groovy.ast.stmt.ExpressionStatement;
+import org.codehaus.groovy.ast.stmt.LoopingStatement;
+import org.codehaus.groovy.ast.stmt.Statement;
+import org.codehaus.groovy.control.CompilePhase;
+import org.codehaus.groovy.control.SourceUnit;
+import org.codehaus.groovy.transform.ASTTransformation;
+import org.codehaus.groovy.transform.GroovyASTTransformation;
+
+import java.util.List;
+import java.util.Objects;
+import java.util.concurrent.atomic.AtomicLong;
+
+import static org.codehaus.groovy.ast.tools.GeneralUtils.args;
+import static org.codehaus.groovy.ast.tools.GeneralUtils.assignS;
+import static org.codehaus.groovy.ast.tools.GeneralUtils.block;
+import static org.codehaus.groovy.ast.tools.GeneralUtils.boolX;
+import static org.codehaus.groovy.ast.tools.GeneralUtils.callX;
+import static org.codehaus.groovy.ast.tools.GeneralUtils.constX;
+import static org.codehaus.groovy.ast.tools.GeneralUtils.ctorX;
+import static org.codehaus.groovy.ast.tools.GeneralUtils.declS;
+import static org.codehaus.groovy.ast.tools.GeneralUtils.geX;
+import static org.codehaus.groovy.ast.tools.GeneralUtils.localVarX;
+import static org.codehaus.groovy.ast.tools.GeneralUtils.ltX;
+import static org.codehaus.groovy.ast.tools.GeneralUtils.stmt;
+import static org.codehaus.groovy.ast.tools.GeneralUtils.throwS;
+import static org.codehaus.groovy.ast.tools.GeneralUtils.varX;
+
+/**
+ * Handles {@link Decreases} annotations placed on loop statements ({@code
for},
+ * {@code while}, {@code do-while}). The closure must return a value that
+ * strictly decreases on every iteration and remains non-negative.
+ * <p>
+ * The transformation injects code to:
+ * <ol>
+ * <li>Save the expression value at the start of each iteration.</li>
+ * <li>Re-evaluate it at the end of the iteration.</li>
+ * <li>Assert the value has strictly decreased.</li>
+ * <li>Assert the value is non-negative.</li>
+ * </ol>
+ * <p>
+ * Example:
+ * <pre>
+ * int n = 10
+ * {@code @Decreases}({ n })
+ * while (n > 0) {
+ * n--
+ * }
+ * </pre>
+ *
+ * @since 6.0.0
+ * @see Decreases
+ * @see LoopVariantViolation
+ */
+@GroovyASTTransformation(phase = CompilePhase.SEMANTIC_ANALYSIS)
+public class LoopVariantASTTransformation implements ASTTransformation {
+
+ private static final AtomicLong COUNTER = new AtomicLong();
+
+ @Override
+ public void visit(final ASTNode[] nodes, final SourceUnit source) {
+ if (nodes.length != 2) return;
+ if (!(nodes[0] instanceof AnnotationNode annotation)) return;
+ if (!(nodes[1] instanceof LoopingStatement loopStatement)) return;
+
+ Expression value = annotation.getMember("value");
+ if (!(value instanceof ClosureExpression closureExpression)) return;
+
+ Expression variantExpression = extractExpression(closureExpression);
+ if (variantExpression == null) return;
+
+ String suffix = Long.toString(COUNTER.getAndIncrement());
+ String prevVarName = "$_gc_decreases_prev_" + suffix;
+ String currVarName = "$_gc_decreases_curr_" + suffix;
+
+ // At start of iteration: def prevVar = <expression>
+ Statement savePrev = declS(localVarX(prevVarName,
ClassHelper.dynamicType()), variantExpression);
+ savePrev.setSourcePosition(annotation);
+
+ // At end of iteration: def currVar = <expression copy>
+ // We need a fresh copy of the expression for re-evaluation
+ Expression variantCopy = copyExpression(closureExpression);
+ Statement saveCurr = declS(localVarX(currVarName,
ClassHelper.dynamicType()), variantCopy);
+ saveCurr.setSourcePosition(annotation);
+
+ // Assert: currVar < prevVar (must strictly decrease)
+ Statement decreaseCheck = stmt(
+ callX(
+
ClassHelper.makeWithoutCaching(LoopVariantASTTransformation.class),
+ "checkDecreased",
+ args(varX(prevVarName), varX(currVarName))
+ )
+ );
+ decreaseCheck.setSourcePosition(annotation);
+
+ // Inject: save at start, check at end
+ injectAtLoopBodyStartAndEnd(loopStatement, savePrev, block(saveCurr,
decreaseCheck));
+ }
+
+ /**
+ * Runtime check called from generated code. Throws {@link
LoopVariantViolation}
+ * if the variant did not strictly decrease or became negative.
+ * <p>
+ * If both values are {@link List}s, they are compared lexicographically:
+ * the first position where values differ must show a strict decrease;
+ * all earlier positions must be equal. If all positions are equal, the
+ * variant has not decreased and a violation is thrown.
+ */
+ public static void checkDecreased(Object prev, Object curr) {
+ if (prev instanceof List<?> prevList && curr instanceof List<?>
currList) {
+ checkDecreasedLexicographic(prevList, currList);
+ } else if (prev instanceof Comparable && curr instanceof Comparable) {
+ checkDecreasedScalar(prev, curr);
+ } else {
+ throw new LoopVariantViolation(
+ "<groovy.contracts.Decreases> loop variant is not
Comparable: prev=" + prev + ", curr=" + curr);
+ }
+ }
+
+ @SuppressWarnings("unchecked")
+ private static void checkDecreasedScalar(Object prev, Object curr) {
+ Comparable<Object> prevComp = (Comparable<Object>) prev;
+ if (prevComp.compareTo(curr) <= 0) {
+ throw new LoopVariantViolation(
+ "<groovy.contracts.Decreases> loop variant did not
decrease: was " + prev + ", now " + curr);
+ }
+ if (curr instanceof Number && ((Number) curr).doubleValue() < 0) {
+ throw new LoopVariantViolation(
+ "<groovy.contracts.Decreases> loop variant became
negative: " + curr);
+ }
+ }
+
+ @SuppressWarnings("unchecked")
+ private static void checkDecreasedLexicographic(List<?> prev, List<?>
curr) {
+ int size = Math.min(prev.size(), curr.size());
+ for (int i = 0; i < size; i++) {
+ Object p = prev.get(i);
+ Object c = curr.get(i);
+ if (!(p instanceof Comparable) || !(c instanceof Comparable)) {
+ throw new LoopVariantViolation(
+ "<groovy.contracts.Decreases> loop variant element at
position " + i
+ + " is not Comparable: prev=" + p + ", curr="
+ c);
+ }
+ int cmp = ((Comparable<Object>) p).compareTo(c);
+ if (cmp > 0) {
+ // This element decreased — lexicographic comparison satisfied
+ return;
+ }
+ if (cmp < 0) {
+ throw new LoopVariantViolation(
+ "<groovy.contracts.Decreases> loop variant increased
at position " + i
+ + ": was " + prev + ", now " + curr);
+ }
+ // cmp == 0: equal at this position, check next
+ }
+ // All compared positions are equal — no progress
+ throw new LoopVariantViolation(
+ "<groovy.contracts.Decreases> loop variant did not decrease:
was " + prev + ", now " + curr);
+ }
+
+ private static Expression extractExpression(ClosureExpression
closureExpression) {
+ BlockStatement block = (BlockStatement) closureExpression.getCode();
+ List<Statement> statements = block.getStatements();
+ if (statements.size() != 1) return null;
+ Statement stmt = statements.get(0);
+ if (stmt instanceof ExpressionStatement) {
+ return ((ExpressionStatement) stmt).getExpression();
+ }
+ return null;
+ }
+
+ private static Expression copyExpression(ClosureExpression
closureExpression) {
+ // Re-extract from the closure to get a fresh AST node
+ // (the original is consumed by the first injection point)
+ BlockStatement block = (BlockStatement) closureExpression.getCode();
+ List<Statement> statements = block.getStatements();
+ if (statements.size() != 1) return null;
+ Statement stmt = statements.get(0);
+ if (stmt instanceof ExpressionStatement exprStmt) {
+ // Use transformExpression to get a deep copy
+ return exprStmt.getExpression().transformExpression(expr -> expr);
+ }
+ return null;
+ }
+
+ private static void injectAtLoopBodyStartAndEnd(LoopingStatement
loopStatement,
+ Statement startCheck,
Statement endCheck) {
+ Statement loopBody = loopStatement.getLoopBlock();
+ BlockStatement newBody;
+ if (loopBody instanceof BlockStatement block) {
+ // Prepend save at start
+ block.getStatements().add(0, startCheck);
+ // Append checks at end
+ block.getStatements().addAll(((BlockStatement)
endCheck).getStatements());
+ newBody = block;
+ } else {
+ newBody = new BlockStatement();
+ newBody.addStatement(startCheck);
+ newBody.addStatement(loopBody);
+ newBody.addStatements(((BlockStatement) endCheck).getStatements());
+ newBody.setSourcePosition(loopBody);
+ loopStatement.setLoopBlock(newBody);
+ }
+ }
+}
diff --git
a/subprojects/groovy-contracts/src/test/groovy/org/apache/groovy/contracts/tests/inv/LoopDecreasesTests.groovy
b/subprojects/groovy-contracts/src/test/groovy/org/apache/groovy/contracts/tests/inv/LoopDecreasesTests.groovy
new file mode 100644
index 0000000000..8951a5216c
--- /dev/null
+++
b/subprojects/groovy-contracts/src/test/groovy/org/apache/groovy/contracts/tests/inv/LoopDecreasesTests.groovy
@@ -0,0 +1,171 @@
+/*
+ * Licensed to the Apache Software Foundation (ASF) under one
+ * or more contributor license agreements. See the NOTICE file
+ * distributed with this work for additional information
+ * regarding copyright ownership. The ASF licenses this file
+ * to you under the Apache License, Version 2.0 (the
+ * "License"); you may not use this file except in compliance
+ * with the License. You may obtain a copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing,
+ * software distributed under the License is distributed on an
+ * "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY
+ * KIND, either express or implied. See the License for the
+ * specific language governing permissions and limitations
+ * under the License.
+ */
+package org.apache.groovy.contracts.tests.inv
+
+import org.apache.groovy.contracts.tests.basic.BaseTestClass
+import org.junit.jupiter.api.Test
+
+import static groovy.test.GroovyAssert.assertScript
+import static groovy.test.GroovyAssert.shouldFail
+
+/**
+ * Tests for {@code @Decreases} applied to loop statements.
+ */
+class LoopDecreasesTests extends BaseTestClass {
+
+ @Test
+ void decreasesOnWhileLoop() {
+ assertScript '''
+ import groovy.contracts.Decreases
+
+ int n = 10
+ @Decreases({ n })
+ while (n > 0) {
+ n--
+ }
+ assert n == 0
+ '''
+ }
+
+ @Test
+ void decreasesOnClassicForLoop() {
+ assertScript '''
+ import groovy.contracts.Decreases
+
+ int remaining = 5
+ @Decreases({ remaining })
+ for (int i = 0; i < 5; i++) {
+ remaining--
+ }
+ assert remaining == 0
+ '''
+ }
+
+ @Test
+ void decreasesWithExpression() {
+ assertScript '''
+ import groovy.contracts.Decreases
+
+ int lo = 0, hi = 10
+ @Decreases({ hi - lo })
+ while (lo < hi) {
+ lo++
+ }
+ assert lo == 10
+ '''
+ }
+
+ @Test
+ void decreasesViolationWhenNotDecreasing() {
+ shouldFail AssertionError, '''
+ import groovy.contracts.Decreases
+
+ int n = 5
+ @Decreases({ n })
+ while (n > 0) {
+ // oops, not decreasing
+ n++
+ if (n > 10) break
+ }
+ '''
+ }
+
+ @Test
+ void decreasesViolationWhenStayingSame() {
+ shouldFail AssertionError, '''
+ import groovy.contracts.Decreases
+
+ int n = 5
+ int count = 0
+ @Decreases({ n })
+ while (n > 0 && count < 3) {
+ // n stays the same - should violate
+ count++
+ }
+ '''
+ }
+
+ @Test
+ void decreasesLexicographic() {
+ assertScript '''
+ import groovy.contracts.Decreases
+
+ // outer stays the same while inner decreases,
+ // then outer decreases and inner resets
+ int outer = 2, inner = 3
+ @Decreases({ [outer, inner] })
+ while (outer > 0) {
+ if (inner > 0) {
+ inner--
+ } else {
+ outer--
+ inner = 3
+ }
+ }
+ assert outer == 0
+ '''
+ }
+
+ @Test
+ void decreasesLexicographicViolation() {
+ shouldFail AssertionError, '''
+ import groovy.contracts.Decreases
+
+ int a = 5, b = 3
+ @Decreases({ [a, b] })
+ while (a > 0) {
+ // a stays the same, b increases - should violate
+ b++
+ if (b > 10) break
+ }
+ '''
+ }
+
+ @Test
+ void decreasesLexicographicFirstElementDecreases() {
+ assertScript '''
+ import groovy.contracts.Decreases
+
+ // first element decreases, second can do anything
+ int x = 5, y = 0
+ @Decreases({ [x, y] })
+ while (x > 0) {
+ x--
+ y += 10 // second element increases, but first decreased so
it is OK
+ }
+ assert x == 0
+ '''
+ }
+
+ @Test
+ void decreasesCombinedWithInvariant() {
+ assertScript '''
+ import groovy.contracts.Decreases
+ import groovy.contracts.Invariant
+
+ int n = 5
+ @Invariant({ n >= 0 })
+ @Decreases({ n })
+ while (n > 0) {
+ n--
+ }
+ assert n == 0
+ '''
+ }
+}
