Annotation Documentation

@org.gcontracts.annotations.Invariant

Allows to specify a class-invariant: a boolean expression with access to all methods and properties of the current object instance.

Closure Variables
all object fields	e.g. @Invariant({ field1 > field2 })
all methods	e.g. @Invariant({ isSomeState() > this.isSomeOtherState() })
all static fields	e.g. @Invariant({ STATIC_FIELD == field1 })
all static methods	e.g. @Invariant({ CHECK_SYNTAX(field1) })

If a descendant inherits a class invariant from a parent class that class invariant will be joined to the current class invariant.

@org.gcontracts.annotations.Requires

Allows to specify a pre-condition: a boolean expression with access to all methods and properties of the current object instance. In addition, the annotation closure has access to all method parameters.

Closure Variables
all object fields	e.g. @Requires({ field1 > field2 })
all methods	e.g. @Requires({ isSomeState() > this.isSomeOtherState() })
all static fields	e.g. @Requires({ STATIC_FIELD == field1 })
all static methods	e.g. @Requires({ CHECK_SYNTAX(field1) })
all method parameters	e.g. @Requires({ parameter1 > 0 && parameter 2 < 100 })

If a descendant overwrites a method with an already defined precondition that precondition will be implicitly joined to the new precondition. The precondition will be weakened (joined with a boolean OR).

@org.gcontracts.annotations.Ensures

Allows to specify a post-condition: a boolean expression with access to all methods and properties of the current object instance. In addition, the annotation closure has access to all method parameters and the method’s return value through the result variable.

Closure Variables
all object fields	e.g. @ Ensures({ field1 > field2 })
all methods	e.g. @ Ensures({ isSomeState() > this.isSomeOtherState() })
all static fields	e.g. @ Ensures({ STATIC_FIELD == field1 })
all static methods	e.g. @ Ensures({ CHECK_SYNTAX(field1) })
all method parameters	e.g. @Ensures({ parameter1 > 0 && parameter 2 < 100 })
old field values	e.g. @Ensures({ old → old.field1 <= field1 })
method result variable	e.g. @Ensures({ result → result == field1 + field2 })

If a descendant overwrites a method with an already defined postcondition that postcondition will be implicitly joined to the new postcondition. The postcondition will be strengthened (joined with a boolean AND).

About Closure Annotations

All annotations use so-called “annotation closures”. By now, Groovy semantically supports closures as annotation parameters, but the compilation process fails. Therefore, all GContracts annotations have a single annotation attribute of type class, e.g.

public @interface Invariant {
    Class value();
}

This is just a simple trick which allows GContracts AST transformation process to replace the annotation closure and add valid code.

Using a closure annotation is pretty straight forward, e.g.

@Invarian({ // some boolean expression })

During compile-time all annotations are embedded at appropriate code places, using Java assertion statements. Java provides various settings to activate/deactivate asserts, e.g. you may activate asserts only for a single class or an entire package.

@org.gcontracts.annotations.Contracted

Used to specify that contract injection is enabled during the compilation process. If applied on a sub-type B where B extends A, contract in A will automatically be injected if B is marked with @Contracted.

Note: This annotation is optional since 1.2.1

@Contracted can be applied on package- or type-level.