DDD: bounded context, ubiquitous language and command guard

This chapter looks at where a flang module coincides with a bounded context from DDD and where it stops. flang describes facts, states and transition rules well, and it can prove that a rule holds on every input. It does not replace the aggregate, the repository or the event bus.

Minimal example

The rule “only an assembled and paid order may be shipped” as a function:

модуль «Исполнение заказа»

тип «Состояние заказа»
  вариант «Создан»
  вариант «Собран»
  вариант «Отгружен»

объект «Заказ»
  «номер»: строка
  «стадия»: «Состояние заказа»
  «оплачен»: признак

тотальная функция «Отгрузка разрешена»
  принимает заказ: «Заказ»
  возвращает признак
  обеспечивает «отгружают только собранный заказ» если не (заказ.«стадия» равен (вариант «Собран»)) то результат равен нет иначе да
  обеспечивает «отгружают только оплаченный заказ» если не заказ.«оплачен» то результат равен нет иначе да
  пример «собранный и оплаченный заказ можно отгрузить»
    дано заказ равно запись «Заказ» с «номер» равным "ЗК-7781" и «стадия» равным (вариант «Собран») и «оплачен» равным да
    ожидается да
  если заказ.«стадия» равен (вариант «Собран»)
    то заказ.«оплачен»
    иначе нет

The order state is a type with variants, not a status string. The rule is the function «Отгрузка разрешена» (shipping allowed), and the two обеспечивает lines state what this function promises on every input.

What the compiler does

flang check parses the module, checks the types of fields and variants, proves that the function terminates and runs the example:

модуль «Исполнение заказа»: функций 1, из них с доказанным завершением 1; типов 2
shipment.flang: проверено — разбор, типы, завершаемость, ядро и примеры; замечаний нет

A typo in a variant name never reaches code review:

FLANG_UNKNOWN_NAME в файле shipment.flang, строка 16, столбец 82: неизвестный конструктор варианта «Собрн»

flang check --proof goes further and answers whether the promises hold on all inputs, not only on the written example:

  постусловие «отгружают только собранный заказ» функции «Отгрузка разрешена» — доказано сведением цели с телом функции: правило «разбор случаев по внутреннему условию цели», объявленные типы аргументов не понадобились — утверждение обо ВСЕХ входах, а не о написанных; теоремы при нём нет и не нужно
shipment.flang: ПРОВЕРЕНО САМОСТОЯТЕЛЬНО — утверждений 2: доказано 2, условно 0, сетка 0, объявлено, не доказано 0, отвергнуто 0, нарушено 0; законов на сетке 0, на веру 0 — код возврата 0

Exit code 0 means “everything is proved”. Code 3 means that some promises were checked only on examples; the report calls this “сетка N” (grid N), where N is the number of values the promise was counted on.

A module as a bounded context

One module is one bounded context, not the whole business domain of the company. «Исполнение заказа» (order fulfilment) is responsible for the step from assembly to shipping. Payments, accounting and warehouse stock are other contexts with their own modules, even if they read the same orders table.

Names inside the module must match the language the business speaks. If the warehouse says “the order is assembled”, the model has the variant «Собран», not status === 3. Ubiquitous language here is not a glossary in a wiki: the names of functions, variants, promises and examples are part of the program. The example “an assembled and paid order can be shipped” runs on every check, and the promise “only a paid order is shipped” is proved in the same words the domain expert used to state it.

A state is a type with variants. The compiler requires a разбор (match) on a state to name every variant. Add the variant «Отгружен» (shipped) without fixing the function, and the check refuses:

FLANG_MATCH_NOT_EXHAUSTIVE в файле shipment.flang, строка 19, столбец 3: разбор «Состояние заказа» не покрывает «Отгружен»

A state transition as a function

An allowed transition is a function that decides from the state whether a command may run, together with its promises. It does not ship anything and does not move money: it answers “yes” or “no” and can give a reason. The real transition — a database write, a call to the courier service — stays in code outside. This is the DDD principle in its plain form: domain rules are kept apart from effects.

The full model lives in static/spec/models/order-lifecycle.flang. Besides the admission it has the command «Отгрузить» (ship), which returns the type «Итог команды» (command outcome): the variant «Принято» (accepted) with the new stage, or «Отклонено» (rejected) with a reason. The rejection reason is a value, not an exception.

A promise of the form если не … то результат равен нет иначе да is an implication: “if the order is not assembled, the answer is no”. The kernel proves such promises when the condition in the body is written as a comparison. There is a trap: the same condition moved into a separate function with разбор is no longer unfolded by the kernel.

модуль «Исполнение заказа»

тип «Состояние заказа»
  вариант «Создан»
  вариант «Собран»
  вариант «Отгружен»

объект «Заказ»
  «номер»: строка
  «стадия»: «Состояние заказа»
  «оплачен»: признак

тотальная функция «Собран ли»
  принимает стадия: «Состояние заказа»
  возвращает признак
  пример «созданный ещё не собран»
    дано стадия равно вариант «Создан»
    ожидается нет
  разбор стадия
    случай «Создан»
      то нет
    случай «Собран»
      то да
    случай «Отгружен»
      то нет

тотальная функция «Отгрузка разрешена»
  принимает заказ: «Заказ»
  возвращает признак
  обеспечивает «отгружают только собранный заказ» если не («Собран ли» от заказ.«стадия») то результат равен нет иначе да
  обеспечивает «отгружают только оплаченный заказ» если не заказ.«оплачен» то результат равен нет иначе да
  пример «собранный и оплаченный заказ можно отгрузить»
    дано заказ равно запись «Заказ» с «номер» равным "ЗК-7781" и «стадия» равным (вариант «Собран») и «оплачен» равным да
    ожидается да
  если «Собран ли» от заказ.«стадия»
    то заказ.«оплачен»
    иначе нет

The program is correct and the example passes, yet both promises drop to being checked on the example only:

shipment.flang: НЕ ДОКАЗАНО — ОПОРА НЕ СУДИЛАСЬ — утверждений 2: доказано 0, условно 0, сетка 2, объявлено, не доказано 0, отвергнуто 0, нарушено 0; законов на сетке 0, на веру 0 — код возврата 3

The rule that follows is simple: write the admission condition as a comparison directly in the body (заказ.«стадия» равен (вариант «Собран»)), and keep разбор for functions that return something different for each variant.

Command guard: the compiler grants admission

examples/spec/shipment-guard/guard.mjs shows what command admission looks like in practice. The model is static/spec/models/order-shipment.flang; its function «Заказ с номером отгружается» (the order with this number ships) finds the order in a list by number and asks «Можно отгрузить» (may be shipped). The claim is fixed by the application, not by the agent and not by the user:

export const CLAIM = '«Заказ с номером отгружается» от заказы, номер равно да';

export async function decideShipment(orderNumber, orders) {
  const verdict = await (await flang()).facts(MODEL_FILE, { заказы: orders, номер: String(orderNumber) }, [CLAIM]);
  const [result] = verdict.results;
  return { allowed: verdict.ok && result.holds === true, claim: CLAIM, why: result.why, steps: result.steps ?? [] };
}

Under the hood this is flang facts: the compiler evaluates the claim on JSON facts and returns a verdict with the evaluation steps. The difference from a plain if (order.readyToShip) ship() is that the decision is not a flag computed somewhere earlier but the result of evaluating a provably terminating function on the snapshot of data passed in.

node examples/spec/shipment-guard/guard.mjs ЗК-7781

returns "allowed": true and the steps: which facts were taken, which function was called and what it returned. If the warehouse has not confirmed the order, the same number and model with a different snapshot:

node examples/spec/shipment-guard/guard.mjs ЗК-7781 --blocked

return "allowed": false and the reason in the compiler’s own words:

«Заказ с номером отгружается» от факта «заказы», факта «номер» = нет, а утверждение требует «равно да». Исходные факты — «заказы»: [{"номер":"ЗК-7781","клиент":"ООО Маяк","оплачен":true,"склад подтвердил":false}]; «номер»: «ЗК-7781»

The process exits with code 1, so the guard fits shell scripts, CI and an agent pipeline alike.

The order number goes into the facts as data rather than being pasted into the program text. Nobody can smuggle foreign logic through it: guard.test.mjs checks that a number with quotes in it simply matches no order.

Admission does not replace an optimistic lock. The state may change between the data snapshot and the write, so the transaction boundary and the version check remain the application’s job.

Where the aggregate boundary runs

flang does not store state and does not manage concurrent access: the language has neither mutable variables nor side effects inside functions. The model describes facts and the transition rule; the application service assembles a snapshot of the aggregate, asks the model and runs the command only on success. Put the model next to the bounded context, not into a shared rules folder:

src/order-execution/
  domain/
  application/
  policies/
    shipment.flang
    shipment.facts.example.json

Version the policy as code: a pull request that changes a .flang file shows the changed rule, the changed examples and the changed promises, and CI runs flang check --proof.

Practice in the sandbox

Remove заказ.«оплачен» from the body of «Отгрузка разрешена» (leave only the stage comparison) and run the check. The promise about payment drops to “сетка 1”: the single example does not refute it. Then add the example “an assembled but unpaid order is not shipped” expecting нет — the check will refuse with FLANG_PROPERTY.

In the example “paid and confirmed may ship” change «склад подтвердил» (warehouse confirmed) to нет and run the check: the function returns нет, the example expects да, and the compiler names the example that failed.

Common mistakes

FLANG_UNKNOWN_NAME — a typo in the name of a variant, field or function. Caught before type checking.
FLANG_MATCH_NOT_EXHAUSTIVE — a разбор on a state forgot a variant. An если … иначе если chain gives no such error: the forgotten case silently falls into the last иначе. That is why branching on a state goes through разбор.

FLANG_PROPERTY — an example broke a promise:

FLANG_EXAMPLE: пример «собранный, но неоплаченный заказ не отгружается» функции «Отгрузка разрешена»: FLANG_PROPERTY: нарушено свойство «отгружают только оплаченный заказ» функции «Отгрузка разрешена»

“сетка N” where “доказано” (proved) was expected. The check itself does not fail (flang check without --proof returns code 0), so CI needs flang check --proof, and the report is worth reading.
An error the compiler will not catch: the rule is written and proved but wrong in substance. The kernel proves that the function keeps its promise, not that the expert stated the rule correctly.

Exercise

Take a command with a real business refusal from your project — approve, refund, publish or deploy. Describe the state as a type with variants and the admission as a function with two implication promises, and get “доказано 2” in the report of flang check --proof. Then build two fact snapshots on which flang facts must and must not grant admission. Separately, in text outside the model, list the technical conditions (lock, idempotency, retries) that stay in the application.

Checklist

A module covers one bounded context, not the whole system.
The names of fields, variants and promises match the expert’s language word for word.
A state is a type with variants, and branching on it is разбор.
Admission is a function that answers “yes” or “no”; the effect is called outside.
The admission promises are proved (доказано in the report), not resting on examples.
The command guard asks the model on a current snapshot (flang facts) instead of storing an “already computed” flag.
The optimistic lock and the transaction boundary stay in the application service.
The model lives next to the bounded context and is reviewed as code.

Catalogue cases on this topic

Каталог применимости

Эти кейсы разбирают тему главы:

Образование