GROOVY-12038: Graduate groovy-contracts from incubating to stable

subprojects/groovy-contracts/src/main/java/groovy/contracts/Contracted.java

@@ -35,6 +35,8 @@
  *
  * import groovy.contracts.*
  * </pre>
+ *
+ * @since 4.0.0
  */
 @Documented
 @Target({ElementType.PACKAGE, ElementType.TYPE})

subprojects/groovy-contracts/src/main/java/groovy/contracts/Ensures.java

@@ -21,7 +21,6 @@
 import org.apache.groovy.contracts.annotations.meta.AnnotationProcessorImplementation;
 import org.apache.groovy.contracts.annotations.meta.Postcondition;
 import org.apache.groovy.contracts.common.impl.EnsuresAnnotationProcessor;
-import org.apache.groovy.lang.annotation.Incubating;
 
 import java.lang.annotation.Documented;
 import java.lang.annotation.ElementType;
@@ -77,11 +76,12 @@
  *   }
  * </pre>
  * </p>
+ *
+ * @since 4.0.0
  */
 @Documented
 @Retention(RetentionPolicy.RUNTIME)
 @Target({ElementType.CONSTRUCTOR, ElementType.METHOD})
-@Incubating
 @Postcondition
 @Repeatable(EnsuresConditions.class)
 @AnnotationProcessorImplementation(EnsuresAnnotationProcessor.class)

subprojects/groovy-contracts/src/main/java/groovy/contracts/EnsuresConditions.java

@@ -18,21 +18,23 @@
  */
 package groovy.contracts;
 
-import org.apache.groovy.lang.annotation.Incubating;
-
 import java.lang.annotation.Documented;
 import java.lang.annotation.ElementType;
 import java.lang.annotation.Retention;
 import java.lang.annotation.RetentionPolicy;
 import java.lang.annotation.Target;
 
 /**
- * Represents multiple postconditions.
+ * Container annotation for multiple {@link Ensures} postconditions on the same target.
+ * Synthesized by the compiler from stacked {@code @Ensures} annotations via
+ * {@link java.lang.annotation.Repeatable}; not normally written by hand.
+ *
+ * @since 5.0.0
+ * @see Ensures
  */
 @Documented
 @Retention(RetentionPolicy.RUNTIME)
 @Target({ElementType.CONSTRUCTOR, ElementType.METHOD})
-@Incubating
 public @interface EnsuresConditions {
     /**
      * Returns the repeated postcondition annotations declared on the target element.

subprojects/groovy-contracts/src/main/java/groovy/contracts/Invariant.java

@@ -23,7 +23,6 @@
 import org.apache.groovy.contracts.annotations.meta.AnnotationProcessorImplementation;
 import org.apache.groovy.contracts.annotations.meta.ClassInvariant;
 import org.apache.groovy.contracts.common.impl.ClassInvariantAnnotationProcessor;
-import org.apache.groovy.lang.annotation.Incubating;
 import org.codehaus.groovy.transform.GroovyASTTransformationClass;
 
 import java.lang.annotation.Documented;
@@ -61,11 +60,12 @@
  * Whenever a class has a parent which itself specifies a class-invariant, that class-invariant expression is combined
  * with the actual class's invariant (by using a logical AND).
  * </p>
+ *
+ * @since 4.0.0
  */
 @Documented
 @Retention(RetentionPolicy.RUNTIME)
 @Target(ElementType.TYPE)
-@Incubating
 @ClassInvariant
 @Repeatable(Invariants.class)
 @ExtendedTarget({ExtendedElementType.LOOP, ExtendedElementType.IMPORT})

subprojects/groovy-contracts/src/main/java/groovy/contracts/Invariants.java

@@ -18,21 +18,23 @@
  */
 package groovy.contracts;
 
-import org.apache.groovy.lang.annotation.Incubating;
-
 import java.lang.annotation.Documented;
 import java.lang.annotation.ElementType;
 import java.lang.annotation.Retention;
 import java.lang.annotation.RetentionPolicy;
 import java.lang.annotation.Target;
 
 /**
- * Represents multiple invariants
+ * Container annotation for multiple {@link Invariant} declarations on the same type.
+ * Synthesized by the compiler from stacked {@code @Invariant} annotations via
+ * {@link java.lang.annotation.Repeatable}; not normally written by hand.
+ *
+ * @since 5.0.0
+ * @see Invariant
  */
 @Documented
 @Retention(RetentionPolicy.RUNTIME)
 @Target(ElementType.TYPE)
-@Incubating
 public @interface Invariants {
     /**
      * Returns the repeated invariant annotations declared on the annotated type.

subprojects/groovy-contracts/src/main/java/groovy/contracts/Requires.java

@@ -21,7 +21,6 @@
 import org.apache.groovy.contracts.annotations.meta.AnnotationProcessorImplementation;
 import org.apache.groovy.contracts.annotations.meta.Precondition;
 import org.apache.groovy.contracts.common.impl.RequiresAnnotationProcessor;
-import org.apache.groovy.lang.annotation.Incubating;
 
 import java.lang.annotation.Documented;
 import java.lang.annotation.ElementType;
@@ -54,11 +53,12 @@
  *   }
  * </pre>
  * </p>
+ *
+ * @since 4.0.0
  */
 @Documented
 @Retention(RetentionPolicy.RUNTIME)
 @Target({ElementType.CONSTRUCTOR, ElementType.METHOD})
-@Incubating
 @Precondition
 @AnnotationProcessorImplementation(RequiresAnnotationProcessor.class)
 @Repeatable(RequiresConditions.class)

subprojects/groovy-contracts/src/main/java/groovy/contracts/RequiresConditions.java

@@ -18,21 +18,23 @@
  */
 package groovy.contracts;
 
-import org.apache.groovy.lang.annotation.Incubating;
-
 import java.lang.annotation.Documented;
 import java.lang.annotation.ElementType;
 import java.lang.annotation.Retention;
 import java.lang.annotation.RetentionPolicy;
 import java.lang.annotation.Target;
 
 /**
- * Represents multiple preconditions.
+ * Container annotation for multiple {@link Requires} preconditions on the same target.
+ * Synthesized by the compiler from stacked {@code @Requires} annotations via
+ * {@link java.lang.annotation.Repeatable}; not normally written by hand.
+ *
+ * @since 5.0.0
+ * @see Requires
  */
 @Documented
 @Retention(RetentionPolicy.RUNTIME)
 @Target({ElementType.CONSTRUCTOR, ElementType.METHOD})
-@Incubating
 public @interface RequiresConditions {
     /**
      * Returns the repeated precondition annotations declared on the target element.

subprojects/groovy-contracts/src/main/java/groovy/contracts/package-info.java

@@ -21,10 +21,25 @@
  * Design-by-contract (DbC) support with compile-time assertion generation.
  *
  * <p>
- * {@link groovy.contracts.Requires @Requires} (precondition),
- * {@link groovy.contracts.Ensures @Ensures} (postcondition),
- * {@link groovy.contracts.Invariant @Invariant} (class invariant).
- * Postconditions can access {@code result} and {@code old()} values.
+ * Stable annotations:
  * </p>
+ * <ul>
+ *   <li>{@link groovy.contracts.Requires @Requires} &ndash; method precondition</li>
+ *   <li>{@link groovy.contracts.Ensures @Ensures} &ndash; method postcondition; closures
+ *       may reference {@code result} and {@code old}</li>
+ *   <li>{@link groovy.contracts.Invariant @Invariant} &ndash; class invariant, also usable
+ *       as a loop invariant on {@code for} / {@code while} / {@code do-while} loops</li>
+ *   <li>{@link groovy.contracts.Contracted @Contracted} &ndash; package- or class-level
+ *       opt-in marker that enables contract processing</li>
+ * </ul>
+ * <p>
+ * Incubating in 6.0.0 (semantics may evolve in a subsequent 6.x release):
+ * </p>
+ * <ul>
+ *   <li>{@link groovy.contracts.Modifies @Modifies} &ndash; frame condition declaring
+ *       which fields and parameters a method may modify</li>
+ *   <li>{@link groovy.contracts.Decreases @Decreases} &ndash; loop termination measure
+ *       (a strictly-decreasing, non-negative variant)</li>
+ * </ul>
  */
 package groovy.contracts;

subprojects/groovy-contracts/src/spec/doc/contracts-userguide.adoc

@@ -38,19 +38,51 @@ package.
 include::../test/ContractsTest.groovy[tags=basic_example,indent=0]
 ----
 
+== Enabling contracts with @Contracted
+
+Contract processing is opt-in. By default, classes that simply mention the contract annotations
+will have them processed; the `@Contracted` marker is used when you want to make the opt-in
+explicit at the package level, or when you want to apply contract processing to a type that
+doesn't itself carry any contract annotations (for example, an empty class whose contract
+comes entirely from inherited interfaces).
+
+`@Contracted` may be placed on a package declaration (in a `package-info.groovy` /
+`package-info.java`) to enable contract processing across every type in that package:
+
+[source,groovy]
+----
+@Contracted
+package com.acme.banking
+
+import groovy.contracts.*
+----
+
+or on an individual type:
+
+[source,groovy]
+----
+@Contracted
+class Account { /* ... */ }
+----
+
+Once enabled, runtime assertion checking still honours the JVM's `-ea` / `-da` flags;
+`@Contracted` controls whether the AST transforms generate assertion code at compile time,
+not whether the resulting assertions execute at run time.
+
 == More Features
 
 Groovy contracts supports the following feature set:
 
 * definition of class invariants, pre- and post-conditions via @Invariant, @Requires and @Ensures
 * definition of loop invariants on `for`, `while`, and `do-while` loops via @Invariant
 * declaration of frame conditions (which fields a method may modify) via @Modifies
+* declaration of loop termination measures via @Decreases
 * inheritance of class invariants, pre- and post-conditions of concrete predecessor classes
 * inheritance of class invariants, pre- and post-conditions in implemented interfaces
 * usage of old and result variable in post-condition assertions
 * assertion injection in Plain Old Groovy Objects (POGOs)
 * human-readable assertion messages, based on Groovy power asserts
-* enabling contracts at package- or class-level with @AssertionsEnabled
+* enabling contracts at package- or class-level with @Contracted
 * enable or disable contract checking with Java's -ea and -da VM parameters
 * annotation contracts: a way to reuse reappearing contract elements in a project domain model
 * detection of circular assertion method calls
@@ -141,6 +173,69 @@ 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 value
+whose successive iteration values form a strictly decreasing, well-founded sequence.
+Two value shapes are supported:
+
+* A single `Comparable` value — usually numeric — that strictly decreases
+  on every iteration. If the value is also a `Number`, it must additionally remain
+  non-negative.
+* A `List` of `Comparable` elements, compared lexicographically: the first position
+  at which consecutive values differ must show a strict decrease, and earlier
+  positions must be equal. This is the natural way to express termination for
+  nested loops (e.g. `[i, j]`).
+
+If the variant fails to decrease (or a numeric scalar variant becomes negative),
+a `LoopVariantViolation` (a subclass of `AssertionError`) is thrown.
+
+This is inspired by similar constructs in design-by-contract languages such as
+Dafny and Eiffel.
+
+NOTE: `@Decreases` is incubating in Groovy 6.0.0. The contract — in particular
+the scalar non-negativity rule and the lexicographic shape for `List` variants —
+may be relaxed or extended in a future release based on usage feedback.
+
+=== While loop
+
+[source,groovy]
+----
+include::../test/ContractsTest.groovy[tags=decreases_while_example,indent=0]
+----
+
+=== For loop
+
+[source,groovy]
+----
+include::../test/ContractsTest.groovy[tags=decreases_for_example,indent=0]
+----
+
+=== Lexicographic (tuple) variants
+
+For nested loops where no single counter strictly decreases on every iteration,
+return a `List` whose elements form a tuple compared lexicographically. In the
+example below the outer counter stays equal while the inner one decreases, then
+the outer one decreases and the inner one is allowed to reset:
+
+[source,groovy]
+----
+include::../test/ContractsTest.groovy[tags=decreases_lexicographic_example,indent=0]
+----
+
+=== Rules for @Decreases closures
+
+* The closure must return a `Comparable` value or a `List` of `Comparable` elements.
+* The value is evaluated at the start and end of each iteration; the end-of-iteration
+  value must be strictly less than the start-of-iteration value (lexicographically,
+  for `List` variants).
+* For numeric scalar variants, the value must also remain `>= 0`.
+  This non-negativity rule does _not_ apply to non-`Number` `Comparable` values
+  (e.g. `String`) or to `List` variants.
+* The closure may reference any variables visible in the enclosing scope.
+
 == Frame Conditions with @Modifies
 
 The `@Modifies` annotation declares which fields or parameters a method is allowed to modify.

subprojects/groovy-contracts/src/spec/test/ContractsTest.groovy

@@ -156,6 +156,56 @@ class ContractsTest extends GroovyTestCase {
         '''
     }
 
+    void testDecreasesWhile() {
+        assertScript '''
+        // tag::decreases_while_example[]
+        import groovy.contracts.Decreases
+
+        int n = 10
+        @Decreases({ n })
+        while (n > 0) {
+            n--
+        }
+        assert n == 0
+        // end::decreases_while_example[]
+        '''
+    }
+
+    void testDecreasesFor() {
+        assertScript '''
+        // tag::decreases_for_example[]
+        import groovy.contracts.Decreases
+
+        int remaining = 5
+        @Decreases({ remaining })
+        for (int i = 0; i < 5; i++) {
+            remaining--
+        }
+        assert remaining == 0
+        // end::decreases_for_example[]
+        '''
+    }
+
+    void testDecreasesLexicographic() {
+        assertScript '''
+        // tag::decreases_lexicographic_example[]
+        import groovy.contracts.Decreases
+
+        int outer = 2, inner = 3
+        @Decreases({ [outer, inner] })
+        while (outer > 0) {
+            if (inner > 0) {
+                inner--
+            } else {
+                outer--
+                inner = 3
+            }
+        }
+        assert outer == 0
+        // end::decreases_lexicographic_example[]
+        '''
+    }
+
     void testJep445Script() {
         runScript '''
         // tag::jep445_example[]