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.

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:

RoleBuilder.create("banker")
    .addAction(ActionConfig.local("withdraw", "Withdraw from an account", handler)
        .withContract(ContractSpec.builder()
            .precondition("amount > 0")
            .postcondition("result.success()")
            .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.