# annotations

`software.visionary.contrax:annotations:2026.10.13` · https://codeberg.org/contrax/annotations

Contrax Annotations: Design by Contract preconditions, postconditions and invariants for Java

Annotations for Design by Contract: <code>@PreCondition</code>, <code>@PostCondition</code> and <code>@Invariant</code> each name the check an obligation must pass, with no dependencies beyond the JDK.

## 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. <code>@PreCondition</code>, <code>@PostCondition</code> and <code>@Invariant</code> 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 <code>value</code> is a <code>Class&lt;? extends Consumer&lt;?&gt;&gt;</code>: the check, named by type rather than by string, so a rename carries it. Retention is <code>CLASS</code>, so the contracts reach the compiled class for a tool that reads it, and are absent at run time. They are <code>@Documented</code>, 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

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

A precondition naming its check

```java
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.