Contracts (`@Contract`)

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 — see Relationship to other mechanisms below.

At a glance

@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:

@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

Expressions are 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:

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:

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

@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.