This module provides contract annotations that support the specification of class-invariants, as well as pre- and post-conditions on Groovy classes and interfaces. Special support is provided so that post-conditions may refer to the old value of variables or to the result value associated with calling a method.
1. Applying @Invariant, @Requires and @Ensures
With Groovy contracts in your classpath, contracts can be applied on a Groovy
class or interface by using one of the annotations found in the groovy.contracts
package.
package acme
import groovy.contracts.*
@Invariant({ speed() >= 0 })
class Rocket {
int speed = 0
boolean started = true
@Requires({ isStarted() })
@Ensures({ old.speed < speed })
def accelerate(inc) { speed += inc }
def speed() { speed }
}
def r = new Rocket()
r.accelerate(5)
2. More Features
Groovy contracts supports the following feature set:
-
definition of class invariants, pre- and post-conditions via @Invariant, @Requires and @Ensures
-
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
-
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
3. The Stack Example
Currently, Groovy contracts supports 3 annotations: @Invariant, @Requires and @Ensures – all of them work as annotations with closures, where closures allow you to specify arbitrary code pieces as annotation parameters:
import groovy.contracts.*
@Invariant({ elements != null })
class Stack<T> {
List<T> elements
@Ensures({ is_empty() })
def Stack() {
elements = []
}
@Requires({ preElements?.size() > 0 })
@Ensures({ !is_empty() })
def Stack(List<T> preElements) {
elements = preElements
}
boolean is_empty() {
elements.isEmpty()
}
@Requires({ !is_empty() })
T last_item() {
elements.get(count() - 1)
}
def count() {
elements.size()
}
@Ensures({ result == true ? count() > 0 : count() >= 0 })
boolean has(T item) {
elements.contains(item)
}
@Ensures({ last_item() == item })
def push(T item) {
elements.add(item)
}
@Requires({ !is_empty() })
@Ensures({ last_item() == item })
def replace(T item) {
remove()
elements.add(item)
}
@Requires({ !is_empty() })
@Ensures({ result != null })
T remove() {
elements.remove(count() - 1)
}
String toString() { elements.toString() }
}
def stack = new Stack<Integer>()
The example above specifies a class-invariant and methods with pre- and post-conditions. Note, that preconditions may reference method arguments and post-conditions have access to the method’s result with the result variable and old instance variables values with old.
Indeed, Groovy AST transformations change these assertion annotations into Java assertion statements (can be turned on and off with a JVM param) and inject them at appropriate places, e.g. class-invariants are used to check an object’s state before and after each method call.
4. Annotation closure rules
-
Invariants should reference class fields only.
-
Preconditions may reference class fields and arguments.
-
Postconditions may reference class fields, arguments, the
result
and the old value of class fields using the syntaxold.fieldname
.
Old values of class fields will only be stored where Groovy
contracts knows how to make a copy. Currently, this means
fields with a Cloneable
class type, primitives, the primitive
wrapper types, BigInteger
, BigDecimal
, and G/Strings.
5. Use within scripts
Currently, Groovy contracts intentionally doesn’t support scripts, but you can use them with JEP-445 compatible scripts from Groovy 5 as shown in this example:
import groovy.contracts.*
import org.apache.groovy.contracts.*
import static groovy.test.GroovyAssert.shouldFail
@Requires({ arg > 0 })
@Ensures({ result < arg })
def sqrt(arg) { Math.sqrt(arg) }
def main() {
assert sqrt(4) == 2
shouldFail(PreconditionViolation) { sqrt(-1) }
}
You could even place an @Invariant
annotation on the main
method
and it will be moved to the generated script class.