annotations

Rationale

Why. In Design by Contract, a caller owes a routine its preconditions, the routine owes the caller its postconditions, and a class owes each visible state its invariants. Stating each where it applies tells a reader, and a tool, who is at fault when one fails.

Problem. Java has no syntax for contracts. Guard clauses inside a method body run late, read as ordinary logic, and do not say whether the caller or the implementation broke the agreement.

Solution. Annotate the party that owns the obligation: the parameter for a precondition, the method for a postcondition, the type for an invariant. Each names the class that checks it, for an annotation processor to read from source or from compiled classes.

Key Concepts

Contract

Role. The meta-annotation that marks an annotation as a contract. @PreCondition, @PostCondition and @Invariant wear it, and so may a contract annotation of your own.

PreCondition

Role. On a parameter: the caller's obligation, what an argument must satisfy before the routine runs. When it fails, the caller is at fault.

PostCondition

Role. On a method: the routine's obligation, what it guarantees when it returns. When it fails, the implementation is at fault.

Invariant

Role. On a type: the class's obligation, what every instance keeps true in each visible state.

How It Works

Guarantees. Each contract's value is a Class<? extends Consumer<?>>: the check, named by type rather than by string, so a rename carries it. Retention is CLASS, so the contracts reach the compiled class for a tool that reads it, and are absent at run time. They are @Documented, so each appears in generated Javadoc.

Lane

Purpose. Declaring who owes what at a routine's boundary, for a tool to check.

Alternative. The Checker Framework, for flow-sensitive analysis through pluggable type systems.

Usage

The module is needed at compile time only

module example {
    requires static software.visionary.contrax.annotations;
}

A precondition naming its check

import java.util.Objects;
import java.util.function.Consumer;
import software.visionary.contrax.annotations.PreCondition;

class NotNull implements Consumer<Object> {
    public void accept(Object value) { Objects.requireNonNull(value); }
}

class Greeter {
    String greet(@PreCondition(NotNull.class) String name) { return "Hello, " + name; }
}

Caveats

• The annotations check nothing themselves. Without an annotation processor that reads them, a contract is documentation.
• A contract is not repeatable: combine constraints into one check rather than stacking annotations.

Views

Drawn from the release. A link in a view opens its source at the release tag.