enforcements

Rationale

Why. Contrax's annotation layer (contrax:annotations) is plain Java: @PreCondition, @PostCondition and @Invariant name an enforcement class and depend on nothing. This module is the other half of the vocabulary. Enforcement and the CallSite it inspects expose javac's tree API, so they live here, beside the enforcements nearly every codebase needs out of the box: this value must not be null; at string-shaped seams, this value must not be blank; and at numeric seams used as sizes, indices, or counts, this value must be strictly positive. Rather than copy IsNotNull, IsNotBlank, and IsPositive implementations everywhere, contrax:enforcements provides them once, correctly, ready for any pack to bake in. Each enforcement is a final class implementing Enforcement with a single enforce(CallSite) method that inspects the AST at the seam and emits a diagnostic when the contract is violated. The module registers each built-in twice: a provides software.visionary.contrax.enforcements.Enforcement directive for the module path, which javac validates when this module is built, and a @Pequenino(service = Enforcement.class, implementation = …) for the class path, which piggies' human writes as a registrations file when it is on the processor path. A pack's rooter reads both into a compiled-in registry, its MotherTree, and dispatches the one a @PreCondition or @PostCondition names. The MotherTree stands where java.util.ServiceLoader would, and is the part a port to a language without one keeps; Enforcement's javadoc shows the TypeScript shape. Nothing is discovered on a consumer's classpath, so a missing jar is a build failure rather than a contract that silently stops being checked. Every expression other than the ones each enforcement recognizes is satisfied. One class per enforcement covers both directions because the detection logic is identical whether the seam is an argument site or a return site — a null is a null, a blank string is a blank string, a non-positive number is a non-positive number. Constants, not just literals: two mechanisms sit behind proving a hoisted value, because Java gives no single answer. IsNotBlank and IsPositive read VariableElement.getConstantValue() — the JLS 4.12.4 constant variable: final, of primitive or String type, initialized with a constant expression. Soundness is by construction, since nothing else reports a value. Constant folding (1 - 2, " " + "\t") and constants read from a separately-compiled classfile are both covered; a boxed declared type such as final Integer n = 0 is not, because it is not a constant variable. IsNotNull cannot use that: per JLS 15.29 null is not a constant expression, so javac computes no constant value for it. It instead reads the variable's declaration tree and checks for a null literal initializer on a variable carrying final. That proof is scoped to the current compilation round — a null constant read from a classfile has no tree to read, so it passes silently. Parentheses and a leading sign are read through, and a negation is proven from the operand's value, not its shape — - -5 is +5 and compiles clean, because javac folds the inner sign into the literal. Binary operators, casts and conditionals are constant expressions javac can fold but contrax does not read, so take(ONE - 1) stays silent. The line is drawn at what the compiler can prove from a declaration, not at what a value will be at runtime. Reassignment, branches, loops, and "effectively final" are all out of scope: contrax reports only violations it can prove, and stays silent otherwise. One enforcement, one concern: each Enforcement implementation expresses exactly one constraint. The enforcement is the dispatch key: a pack's registry is keyed by implementation class name — the only form a Class-valued annotation member takes during annotation processing — and dispatch calls enforce(CallSite). A final class with a public no-arg constructor is what a pack needs to construct one, and what javac checks of a provides, and human of a @Pequenino, at this module's build. Stateless: a pack builds each enforcement once and reuses it for every seam, across concurrent compilations. Writing an enforcement needs this module; naming one does not drag in javac. A declaring module requires this one static, for the class it names; a pack picks whichever enforcement modules it wants.

Key Concepts

Enforcement

Role. A compile-time Design-by-Contract enforcement, void enforce(CallSite): the constraint carrier. A pack resolves the enforcement class named in a contract annotation to a baked-in instance.

Pattern. Functional interface, a Consumer<CallSite>

CallSite

Role. The single parameter object handed to an Enforcement — everything the framework knows about the seam being inspected: the expression, the annotation that triggered dispatch, the substrate, and violate(), the only way to report a contract violation. Unsealed — the framework implements it, and so may a test.

Pattern. Interface, a Runnable that violates

Details

Role. The substrate a CallSite carries: the executable at the seam, its compilation unit, and the compilation's Javac facades (env(), and trees() and javacTask() derived from it), so an enforcement can resolve what it sees at the seam and the framework can position its diagnostic through trees(). Details.Seam is the value over a live compilation; a test doubles the interface and answers the facades itself, so nothing reaches for Trees.instance.

Pattern. Lens over the compilation

IsNotNull

Role. Demands a non-null value at compile time. Recognizes, at either parameter or return seam, a null literal or a declared-final variable initialized to one.

Pattern. Enforcement: stateless final class, public no-arg constructor

IsNotBlank

Role. Demands a non-blank String at compile time. Recognizes, at either parameter or return seam, an empty- or whitespace-only string constant.

Pattern. Enforcement: stateless final class, public no-arg constructor

IsPositive

Role. Demands a strictly positive numeric value (greater than zero) at compile time. Recognizes, at either parameter or return seam, a numeric constant that is not strictly positive — zero, negative, or NaN.

Pattern. Enforcement: stateless final class, public no-arg constructor

How It Works

Guarantees. Report violations by calling CallSite.violate(); return silently otherwise. An enforcement that fails instead is contained: the framework catches it and emits a build error naming the enforcement, the throwable, and the seam whose contract went unverified. Only the failing enforcement is affected — other seams still get checked. Construction is covered too: a pack builds every enforcement it baked in before checking anything, and one whose constructor throws is blamed with a build error rather than left to fail silently at some seam.

Lane

Purpose. Compile-time enforcement where you control compilation: your callers are part of the same compile graph and you want the constraint enforced at the seam where they write the literal.

Alternative. Type-driven runtime enforcement, such as a software.visionary.strings.NonEmptyString parameter that throws on construction. The two tools are complementary: compile-time enforcement covers the inside of your codebase; type-driven runtime enforcement covers the boundary.

When to avoid. When you take arbitrary input from sources you don't control — HTTP request bodies, file parsers, third-party callers compiled separately — enforce the invariant at runtime through the type system instead.

Usage

Usage

// module-info.java
requires static software.visionary.contrax.enforcements;
// transitively requires software.visionary.contrax.annotations

Usage in annotations

// Caller's obligation: argument must not be null
void process(@PreCondition(IsNotNull.class) Object value) { … }

// Caller's obligation: string must carry actual content
void greet(@PreCondition(IsNotBlank.class) String name) { … }

// Caller's obligation: count must be strictly positive
void take(@PreCondition(IsPositive.class) int n) { … }

// Supplier's obligation: returned size must be strictly positive
@PostCondition(IsPositive.class)
int size() { … }

// Supplier's obligation: return value must not be null
@PostCondition(IsNotNull.class)
Object produce() { … }

// Supplier's obligation: returned string must carry actual content
@PostCondition(IsNotBlank.class)
String headline() { … }

A value hoisted into a constant is still proven

process(null);                  // compile error
final Object none = null;
process(none);                  // compile error — same proof

Object maybe = null;            // not final
process(maybe);                 // compiles: it could be reassigned before the call

Dependencies

• software.visionary.contrax:annotations:2026.10.13 at Compile
• software.visionary.piggies:pequenino:2026.10.13 at Provided
• software.visionary:junit-closure:2026.09.17 at Testing
• software.visionary.spex:carlin:2026.09.17 at Testing

Views

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