Skip to main content
Welcome. This site supports keyboard navigation and screen readers. Press ? at any time for keyboard shortcuts. Press [ to focus the sidebar, ] to focus the content. High-contrast themes are available via the toolbar.
serard@dev00:~/cv

Pre, Post, Invariant

Bertrand Meyer's Eiffel: The Language introduced design-by-contract as a discipline that makes software prove it satisfies its contract at runtime. Every method has a precondition (what the caller must guarantee before invoking), a postcondition (what the method promises to deliver if its precondition held), and the enclosing class has invariants (what is true between every method call). @frenchexdev/ddd-dbc reifies the triad as TypeScript decorators so aggregate methods can carry their contract instead of hiding it.


What ddd-dbc Reifies

The three primitives are precise. Precondition (@Pre): a boolean expression that must be true on entry. The caller is on the hook — a failure means the caller did something the method explicitly does not handle, and the right response is to fail fast rather than try to recover. Postcondition (@Post): a boolean expression that must be true on successful exit. The callee is on the hook — a failure means the method did not deliver what it promised, and the right response is a developer-time error, not a customer-facing failure. Invariant (@Invariant): a boolean expression that must be true between every method call. The class is on the hook — a violation means an internal state mutation has corrupted the object.

For an aggregate, the triad maps directly. The aggregate's declared invariants (the optional invariants field on @AggregateRoot and @Entity) become @Invariant decorations the codegen can materialise. The aggregate's mutating methods declare what must hold before they run (@Pre) and what they guarantee after (@Post). The contract becomes machine-checkable.

The discipline pays off in two places. In tests, the property-based testing harness can verify the contract by feeding random inputs that satisfy preconditions and asserting postconditions hold. In production, contract violations fail-fast — the application crashes loudly rather than continuing with a corrupted invariant. Both are improvements over an aggregate whose contract lives in comments.


The Runtime: ddd-dbc

The runtime is at the M4/M5 stub milestone. The decorator surface — @Pre, @Post, @Invariant — is planned; the actual evaluation engine (a thin runtime that checks the predicate, throws a typed ContractViolation on failure, optionally enabled only in development) lands when a consumer drives it.

The expected shape (sketched, not shipped):

// Sketch — the runtime decorators are not yet exported.

@AggregateRoot({ /* ... */ })
@Invariant('this.balance >= 0', 'Balance never goes negative')
export class Account {
  constructor(public balance: number) {}

  @Pre('amount > 0', 'Withdrawal amount is positive')
  @Post('this.balance === old(this.balance) - amount', 'Balance decreases by exactly amount')
  withdraw(amount: number): void {
    this.balance -= amount;
  }
}

old(...) in the postcondition references the value of this.balance at the start of the method, the standard DbC convention for postconditions that reason about change. The runtime's responsibility is to snapshot old-referenced values on entry and use them when evaluating the postcondition on exit.


  • Composes with @Entity — the entity's invariants: readonly string[] declares names that @Invariant materialises.
  • Composes with @AggregateRoot — every mutating method on the aggregate carries @Pre/@Post; the analyzer's DDD0103_ENTITY_DECLARED_INVARIANT_NOT_ENFORCED (from the entity analyzer) becomes precisely answerable once DbC is wired.
  • Composes with @SchemaValidation — preconditions on input shape are often delegated to schema validators.
  • Failures produce a typed ContractViolation consumed by the same diagnostic surface as the analyzer codes.

Back to the series index.

⬇ Download