# Contracts (`@Contract`)

`@Contract` brings **Design by Contract** to actions: JEXL **preconditions**, **postconditions**, and **invariants** that the framework enforces around every action invocation. Preconditions reject bad input (including parameters an LLM hallucinated) *before* the method runs; postconditions catch incorrect results or corrupted state *after* it runs.

This is the declarative, JEXL-backed contract mechanism (`com.tnsai.actions.contracts.ContractValidator`). It is distinct from the older `InvariantChecker` / `@ActionSpec.precondition` mechanism described in [Validation](validation.md) — see [Relationship to other mechanisms](#relationship-to-other-mechanisms) below.

## At a glance

```java
@ActionSpec(type = ActionType.LOCAL, description = "Withdraw from an account")
@Contract(
    preconditions  = {"amount > 0", "amount <= account.balance"},
    postconditions = {"account.balance == old(account.balance) - amount"},
    invariants     = {"account.balance >= 0"})
public Account withdraw(Account account, double amount) {
    account.balance -= amount;
    return account;
}
```

* A failed **precondition** throws before `withdraw` runs — the LLM gets a clear "precondition violated: amount > 0" and can retry with corrected arguments.
* The **postcondition** binds `old(account.balance)` to the pre-execution value, so it verifies the balance actually dropped by `amount`.
* The **invariant** is checked both before and after.

## Pairing with `@ActionSpec`

In TnsAI 0.14.0 (`TnsAI@4b9aff80`, TAN-2774 / PR #127),
`ActionDiscovery` fails loud if a method carries `@Contract` and no
`@ActionSpec`. The exception is `IllegalStateException` and names the
method FQN:

```text
@Contract on com.example.Ledger.helper has no @ActionSpec; the clause is
never evaluated. Annotate the method with @ActionSpec or remove @Contract.
```

Discovery does **not** synthesize an `@ActionSpec`. A helper that only
has `@Contract` is no longer a silent no-op. This rule ships in
Maven Central `0.14.1`.

## Clause semantics

| Clause | When | On failure |
| --- | --- | --- |
| `preconditions` | before execution | always throws `ContractViolationException` |
| `postconditions` | after execution | throws (unless `strict = false`, then logs) |
| `invariants` | before **and** after | always throws |

Expressions are [JEXL](https://commons.apache.org/proper/commons-jexl/). Inside them you can reference the action's parameters by name, plus two special bindings in postconditions:

* **`result`** — the value the action returned (e.g. `result.success()`).
* **`old(expr)`** — the value `expr` had *before* execution, captured automatically (e.g. `old(account.balance)`). Use it to assert a delta.

### Flags

* `validate = false` — disables all enforcement for that action; the contract becomes documentation only.
* `strict = false` — downgrades **postcondition** failures to a logged warning instead of throwing (preconditions and invariants always throw).
* `message = "…"` — overrides the default violation message.

## Programmatic contracts (`ContractSpec`)

Actions added through `RoleBuilder.addAction(...)` have no annotated method, so they attach a contract with `ActionConfig.withContract(...)`. The `ContractSpec` builder is the programmatic equivalent of `@Contract`, enforced through the exact same code path:

<!-- java-contract: src/main/java/com/example/tnsai/docs/ContractSpecBuilderExample.java -->
```java
package com.example.tnsai.docs;

import com.tnsai.metadata.ActionConfig;
import com.tnsai.metadata.ActionHandler;
import com.tnsai.metadata.ContractSpec;
import com.tnsai.roles.Role;
import com.tnsai.roles.RoleBuilder;

public final class ContractSpecBuilderExample {
    private ContractSpecBuilderExample() {}

    public static Role banker(ActionHandler handler) {
        return RoleBuilder.create()
            .name("banker")
            .goal("Process withdrawals")
            .addAction(ActionConfig.local("withdraw", "Withdraw from an account", handler)
                .withContract(ContractSpec.builder()
                    .precondition("amount > 0")
                    .postcondition("result.success()")
                    .build()))
            .build();
    }
}
```

`ContractSpec.from(@Contract)` adapts an annotation into a spec, so the annotation and builder paths are indistinguishable at enforcement time.

## Build-time validation (AGENT-V013)

`AgentBuilder.build()` parses every contract clause with the JEXL engine and reports a malformed expression as a warning — `AGENT-V013` — so a typo surfaces at build time instead of failing on the first invocation. Suppress it (for example if you template expressions at runtime) with:

```java
AgentBuilder.create().relaxValidation("AGENT-V013").build();
```

## Relationship to other mechanisms

TnsAI has more than one way to constrain an action; they coexist:

* **`@Contract`** (this page) — declarative **JEXL** preconditions/postconditions/invariants with `old(...)`/`result`. The richest, most expressive option.
* **`@ActionSpec.precondition` / `@State.invariants` + `InvariantChecker`** — an earlier rule-engine mechanism, documented under [Validation](validation.md). Single expressions plus state effects; not JEXL.
* **`ActionContract`** — an imperative interface for contracts expressed in Java rather than expression strings.

Prefer `@Contract` for new code unless you specifically need one of the others.

## How it compares

| Framework | Mechanism | Scope |
| --- | --- | --- |
| **TnsAI `@Contract`** | JEXL pre/post/invariants with `old()`/`result`, enforced around the action | Behavioural correctness of each action, not just shape |
| MCP JSON Schema | tool input schema | Parameter **shape**, not semantics |

`@Contract` differs in that it enforces **semantic** pre/post conditions on the action's own parameters and result (and state deltas via `old(...)`), not only the shape of the input.