diff --git a/subprojects/groovy-contracts/src/main/java/groovy/contracts/Contracted.java b/subprojects/groovy-contracts/src/main/java/groovy/contracts/Contracted.java index 06204f1ffc8..5eda698b91e 100644 --- a/subprojects/groovy-contracts/src/main/java/groovy/contracts/Contracted.java +++ b/subprojects/groovy-contracts/src/main/java/groovy/contracts/Contracted.java @@ -35,6 +35,8 @@ * * import groovy.contracts.* * + * + * @since 4.0.0 */ @Documented @Target({ElementType.PACKAGE, ElementType.TYPE}) diff --git a/subprojects/groovy-contracts/src/main/java/groovy/contracts/Ensures.java b/subprojects/groovy-contracts/src/main/java/groovy/contracts/Ensures.java index 5ea65e790f7..d79144ca730 100644 --- a/subprojects/groovy-contracts/src/main/java/groovy/contracts/Ensures.java +++ b/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 @@ * } * *

+ * + * @since 4.0.0 */ @Documented @Retention(RetentionPolicy.RUNTIME) @Target({ElementType.CONSTRUCTOR, ElementType.METHOD}) -@Incubating @Postcondition @Repeatable(EnsuresConditions.class) @AnnotationProcessorImplementation(EnsuresAnnotationProcessor.class) diff --git a/subprojects/groovy-contracts/src/main/java/groovy/contracts/EnsuresConditions.java b/subprojects/groovy-contracts/src/main/java/groovy/contracts/EnsuresConditions.java index b89d8cebe28..a46c94f60b1 100644 --- a/subprojects/groovy-contracts/src/main/java/groovy/contracts/EnsuresConditions.java +++ b/subprojects/groovy-contracts/src/main/java/groovy/contracts/EnsuresConditions.java @@ -18,8 +18,6 @@ */ 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; @@ -27,12 +25,16 @@ 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. diff --git a/subprojects/groovy-contracts/src/main/java/groovy/contracts/Invariant.java b/subprojects/groovy-contracts/src/main/java/groovy/contracts/Invariant.java index 96760e920fa..c89bc4c8132 100644 --- a/subprojects/groovy-contracts/src/main/java/groovy/contracts/Invariant.java +++ b/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). *

+ * + * @since 4.0.0 */ @Documented @Retention(RetentionPolicy.RUNTIME) @Target(ElementType.TYPE) -@Incubating @ClassInvariant @Repeatable(Invariants.class) @ExtendedTarget({ExtendedElementType.LOOP, ExtendedElementType.IMPORT}) diff --git a/subprojects/groovy-contracts/src/main/java/groovy/contracts/Invariants.java b/subprojects/groovy-contracts/src/main/java/groovy/contracts/Invariants.java index eaa81f4a3f3..0817e08932c 100644 --- a/subprojects/groovy-contracts/src/main/java/groovy/contracts/Invariants.java +++ b/subprojects/groovy-contracts/src/main/java/groovy/contracts/Invariants.java @@ -18,8 +18,6 @@ */ 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; @@ -27,12 +25,16 @@ 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. diff --git a/subprojects/groovy-contracts/src/main/java/groovy/contracts/Requires.java b/subprojects/groovy-contracts/src/main/java/groovy/contracts/Requires.java index e1da332744e..0cc9139dde4 100644 --- a/subprojects/groovy-contracts/src/main/java/groovy/contracts/Requires.java +++ b/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 @@ * } * *

+ * + * @since 4.0.0 */ @Documented @Retention(RetentionPolicy.RUNTIME) @Target({ElementType.CONSTRUCTOR, ElementType.METHOD}) -@Incubating @Precondition @AnnotationProcessorImplementation(RequiresAnnotationProcessor.class) @Repeatable(RequiresConditions.class) diff --git a/subprojects/groovy-contracts/src/main/java/groovy/contracts/RequiresConditions.java b/subprojects/groovy-contracts/src/main/java/groovy/contracts/RequiresConditions.java index ac742430e27..fedd0e502c7 100644 --- a/subprojects/groovy-contracts/src/main/java/groovy/contracts/RequiresConditions.java +++ b/subprojects/groovy-contracts/src/main/java/groovy/contracts/RequiresConditions.java @@ -18,8 +18,6 @@ */ 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; @@ -27,12 +25,16 @@ 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. diff --git a/subprojects/groovy-contracts/src/main/java/groovy/contracts/package-info.java b/subprojects/groovy-contracts/src/main/java/groovy/contracts/package-info.java index b976ba4da37..b66fa2f882e 100644 --- a/subprojects/groovy-contracts/src/main/java/groovy/contracts/package-info.java +++ b/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. * *

- * {@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: *

+ * + *

+ * Incubating in 6.0.0 (semantics may evolve in a subsequent 6.x release): + *

+ * */ package groovy.contracts; diff --git a/subprojects/groovy-contracts/src/spec/doc/contracts-userguide.adoc b/subprojects/groovy-contracts/src/spec/doc/contracts-userguide.adoc index dee4c8934ec..1aa1100641e 100644 --- a/subprojects/groovy-contracts/src/spec/doc/contracts-userguide.adoc +++ b/subprojects/groovy-contracts/src/spec/doc/contracts-userguide.adoc @@ -38,6 +38,37 @@ 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: @@ -45,12 +76,13 @@ 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. diff --git a/subprojects/groovy-contracts/src/spec/test/ContractsTest.groovy b/subprojects/groovy-contracts/src/spec/test/ContractsTest.groovy index 18aa43eeb0a..06343cc061d 100644 --- a/subprojects/groovy-contracts/src/spec/test/ContractsTest.groovy +++ b/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[]