Сквозной проект: исполнение заказа от модели до сервиса и формы
Капстоун соединяет всё, что было в курсе, в одном проекте: предметный объект, тип состояний, функцию расчёта с примерами и обещанием, допуск отгрузки, HTTP-сервис, форму и TypeScript для CI. Правило записано один раз — на flang, — а пользуются им пять частей системы. Ниже на каждом шаге стоит команда и её настоящий вывод.
1. Модель
Модель лежит в static/spec/models/order-fulfilment.flang:
модуль «Исполнение заказа»
тип «Состояние заказа»
вариант «Создан»
вариант «Оплачен»
вариант «Собран»
объект «Заказ»
«номер»: строка
«сумма»: неотрицательное
«оплачен»: признак
«склад подтвердил»: признак
тип «Решение по отгрузке»
вариант «Разрешено»
вариант «Отказано» содержит причина: строка
тотальная функция «Скидка»
принимает заказ: «Заказ»
возвращает число
обеспечивает «скидка ограничена» результат не больше 10000
пример «заказ на двадцать тысяч»
дано заказ равно запись «Заказ» с «номер» равным "ЗК-7781" и «сумма» равным 20000 и «оплачен» равным да и «склад подтвердил» равным да
ожидается 2000
пример «заказ ровно на потолок скидки»
дано заказ равно запись «Заказ» с «номер» равным "ЗК-7782" и «сумма» равным 100000 и «оплачен» равным да и «склад подтвердил» равным да
ожидается 10000
пример «заказ выше потолка»
дано заказ равно запись «Заказ» с «номер» равным "ЗК-7783" и «сумма» равным 250000 и «оплачен» равным да и «склад подтвердил» равным да
ожидается 10000
если заказ.«сумма» больше 100000
то 10000
иначе если заказ.«сумма» не меньше 10000
то (заказ.«сумма» умножить на 10) делить на 100
иначе 0
тотальная функция «Состояние»
принимает заказ: «Заказ»
возвращает «Состояние заказа»
пример «оплачен, склад молчит»
дано заказ равно запись «Заказ» с «номер» равным "ЗК-7781" и «сумма» равным 20000 и «оплачен» равным да и «склад подтвердил» равным нет
ожидается вариант «Оплачен»
если не заказ.«оплачен»
то вариант «Создан»
иначе если заказ.«склад подтвердил»
то вариант «Собран»
иначе вариант «Оплачен»
тотальная функция «Можно отгрузить»
принимает заказ: «Заказ»
возвращает признак
обеспечивает «неоплаченный заказ не отгружается» если не заказ.«оплачен» то результат равен нет иначе да
обеспечивает «без подтверждения склада не отгружается» если не заказ.«склад подтвердил» то результат равен нет иначе да
пример «собранный заказ отгружается»
дано заказ равно запись «Заказ» с «номер» равным "ЗК-7781" и «сумма» равным 20000 и «оплачен» равным да и «склад подтвердил» равным да
ожидается да
разбор «Состояние» от заказ
случай «Собран»
то да
случай «Оплачен»
то нет
случай «Создан»
то нет
тотальная функция «Допуск отгрузки»
принимает заказ: «Заказ»
возвращает «Решение по отгрузке»
пример «склад не подтвердил — причина названа»
дано заказ равно запись «Заказ» с «номер» равным "ЗК-7781" и «сумма» равным 20000 и «оплачен» равным да и «склад подтвердил» равным нет
ожидается вариант «Отказано» с причина равным "склад не подтвердил заказ"
разбор «Состояние» от заказ
случай «Собран»
то вариант «Разрешено»
случай «Оплачен»
то вариант «Отказано» с причина равным "склад не подтвердил заказ"
случай «Создан»
то вариант «Отказано» с причина равным "заказ не оплачен"
Что здесь что:
объект «Заказ»— данные, с которыми приходит запрос: номер, сумма и два факта — оплачен ли заказ и подтвердил ли его склад.тип «Состояние заказа»— три состояния. Значение этого типа нельзя просто прочитать: его разбираютразбор, и компилятор требует назвать все три варианта.- «Скидка» считает деньги. Её примеры — предметные тесты, которые гоняются на каждой проверке.
- «Можно отгрузить» и «Допуск отгрузки» описывают разрешённый переход «собран → можно отгружать». Первая отвечает да или нет, вторая — решением с причиной отказа.
Ничего из этого не пишет в базу и не вызывает курьерскую службу: модель только считает и выносит решение.
Потолок скидки назван двумя способами. Ветвь
если заказ.«сумма» больше 100000 то 10000 его держит, а обещание
обеспечивает «скидка ограничена» результат не больше 10000 его объявляет. Второй пример показывает, что потолок достижим
ровно: обещание, до которого не доходит ни один пример, ничего не проверяет.
Ловушки с границами разобраны в главе об антипаттернах.
В рабочих проектах курса эта модель разложена на две: расчёт скидки — в
order-discount.flang (его считает HTTP-сервис), допуск отгрузки — в
order-shipment.flang (его считает shipment-guard). Устроены они так же.
2. Архитектура
Модель проверяется один раз, а дальше от неё расходятся независимые ветки. Форма
берёт поля из flang ast, сервис считает скидку функцией, которую напечатал
flang emit, guard спрашивает flang facts, CI сверяет напечатанный TypeScript,
агент получает те же проверки через flang --mcp-mode. Если правило меняется,
меняется только левый узел графа — остальные пересобираются от него, а не
правятся по отдельности.
3. Шаг за шагом
3.1 Проверка модели
flang check static/spec/models/order-fulfilment.flang
модуль «Исполнение заказа»: функций 4, из них с доказанным завершением 4; типов 3
order-fulfilment.flang: проверено — разбор, типы, завершаемость, ядро и примеры; замечаний нет
Компилятор разобрал программу, вывел типы, доказал, что все четыре функции
завершаются, и прогнал примеры. Про доказательства обещаний эта команда не
говорит ничего — их показывает ключ --proof:
flang check static/spec/models/order-fulfilment.flang --proof
постусловие «скидка ограничена» функции «Скидка» — сетка 3 значения (примеры функции): …
постусловие «неоплаченный заказ не отгружается» функции «Можно отгрузить» — доказано сведением цели с телом функции: правило «разбор цели по условию» … — утверждение обо ВСЕХ входах, а не о написанных
постусловие «без подтверждения склада не отгружается» функции «Можно отгрузить» — доказано сведением цели с телом функции: правило «разбор случаев по внутреннему условию цели» … — утверждение обо ВСЕХ входах, а не о написанных
order-fulfilment.flang: НЕ ДОКАЗАНО — ОПОРА НЕ СУДИЛАСЬ — утверждений 3: доказано 2, условно 0, сетка 1, объявлено, не доказано 0, отвергнуто 0, нарушено 0; законов на сетке 0, на веру 0 — код возврата 3
Два обещания о допуске доказаны для любого заказа, а не для трёх написанных. Потолок
скидки компилятор не доказывает: оценку «десять процентов от суммы не больше
десяти тысяч» ядро не выводит, и обещание держится на трёх примерах — это и
значит «сетка 3». Код возврата 3 говорит об этом вслух. Что с этим делать — решать
команде: либо принять сетку и смотреть на код 3 в CI отдельно, либо переписать
тело так, чтобы граница совпала с ветвью если.
Предметные примеры отдельной командой:
flang test static/spec/models/order-fulfilment.flang
order-fulfilment.flang: примеров 6, прошло 6, не прошло 0
Если правило скидки когда-нибудь поменяют на 12 процентов, этот шаг упадёт первым — раньше HTTP-сервиса и раньше формы.
3.2 Допуск отгрузки по фактам
Разрешение на отгрузку — не поле в базе, а ответ flang facts на снимке
данных. Снимок — обычный JSON, который сервис собирает из своих таблиц перед
решением (static/spec/models/order-fulfilment.facts.json):
{
"заказ": {
"номер": "ЗК-7781",
"сумма": 20000,
"оплачен": true,
"склад подтвердил": true
}
}
flang facts static/spec/models/order-fulfilment.flang \
--facts static/spec/models/order-fulfilment.facts.json \
--claims '["«Можно отгрузить» от заказ равно да"]' --pretty
"claim": "«Можно отгрузить» от заказ равно да",
"holds": true,
"why": "«Можно отгрузить» от факта «заказ» = да; требование «равно да» выполнено",
"status": "verified"
Рядом с вердиктом приходят шаги: какой факт взят, какая функция вызвана, что
она вернула и с чем сравнили. Вызывать можно только функцию с доказанным
завершением — нетотальную flang facts отклоняет до вычисления.
examples/spec/shipment-guard/guard.mjs оборачивает то же самое в функцию для
сервиса. Он работает с моделью order-shipment.flang, где заказ ищется в
таблице по номеру:
node examples/spec/shipment-guard/guard.mjs ЗК-7781
даёт "allowed": true и код возврата 0. Тот же номер, но снимок, где склад не
подтвердил приёмку:
node examples/spec/shipment-guard/guard.mjs ЗК-7781 --blocked
"allowed": false,
"why": "«Заказ с номером отгружается» от факта «заказы», факта «номер» = нет, а утверждение требует «равно да». Исходные факты — «заказы»: [{\"номер\":\"ЗК-7781\",\"клиент\":\"ООО Маяк\",\"оплачен\":true,\"склад подтвердил\":false}]; «номер»: «ЗК-7781»"
Модель, утверждение и код guard не менялись — изменился только снимок, и решение
изменилось вместе с ним. Код возврата 1 делает эту разницу пригодной для
shell-скрипта и CI. Настоящий вызов shipping.createShipment(orderId) идёт
строго после allowed === true: действие живёт вне модели, а не внутри guard.
3.3 HTTP-сервис
npm run spec:api
На старте сервис прогоняет flang test по order-discount.flang: если пример
не сходится, процесс не поднимается вообще. Потом модель печатается в JavaScript
(flang emit --target js), и запросы считает напечатанная функция, без
компилятора в рантайме. После старта:
curl -s localhost:8788/discount -d '{"сумма":20000,"постоянный клиент":true}'
# {"discount": 3000}
curl -s localhost:8788/contract
# {"function": "Рассчитать скидку", "input": [{"name": "сумма", "type": "неотрицательное"},
# {"name": "постоянный клиент", "type": "признак"}], "output": "number"}
/contract не хардкодит список полей — он берёт их из flang ast. Добавили
поле в модель — контракт обновился сам. Запрос с неверным типом входа (строка
вместо числа) получает 400 с причиной, а не 500:
{"error": "вход не подходит к «Покупке»: «сумма»: ждали неотрицательное целое", "code": "INPUT"}
3.4 Форма
Схема формы — чистая функция от flang ast:
node examples/spec/form-schema/schema.mjs Покупка
{
"id": "Продажи.Покупка",
"title": "Покупка",
"fields": [
{ "name": "сумма", "label": "сумма", "type": "неотрицательное", "control": "number", "required": true, "min": 0 },
{ "name": "постоянный клиент", "label": "постоянный клиент", "type": "flag", "control": "checkbox", "required": true }
]
}
examples/spec/react-form/DiscountForm.jsx рисует поле под каждый элемент
fields, а предпросчёт скидки делает в браузере той же напечатанной функцией
«Рассчитать скидку». Пользователь видит скидку без запроса на сервер, а сервер
всё равно считает заново при отправке: браузеру не доверяют, но и не заставляют
ждать. Нарушенное обещание модели приходит в форму ошибкой с кодом
FLANG_PROPERTY — это ответ формы, а не падение интерфейса.
3.5 Генерация TypeScript
node examples/spec/typescript-codegen/generate.mjs
node examples/spec/typescript-codegen/generate.mjs --check
Первый вызов прогоняет примеры модели и печатает в generated/ модуль
program.ts с рантаймом рядом. Второй ничего не пишет — только сравнивает.
Если кто-то поправит напечатанный .ts руками, --check назовёт отставшие
файлы и выйдет кодом 1. Подробный разбор — в главе про генерацию и
CI.
3.6 CI
npm run spec:check
npm run spec:examples
Первая команда прогоняет компилятором каждую программу из глав курса и все
модели, вторая — тесты рабочих проектов: сервиса, guard, формы, генерации,
миграции. Готовый workflow examples/spec/ci/flang-check.yml ставит flang и
выполняет шаги по порядку: проверка модели, примеры, сверка напечатанного кода,
тесты интеграций. Первым падает самый дешёвый шаг, последним — самый дорогой.
Это тот же порядок, что в шагах 3.1–3.5.
4. Definition of done
flang checkпроходит,flang testпроходит;flang check --proofпрочитан: каждое обещание названо «доказано», «сетка N» или «объявлено, не доказано», и команда знает, какие из них держатся только на примерах;- обещание о потолке скидки достигается хотя бы одним примером ровно — иначе оно не проверяет ничего;
- форма читает поля из
flang ast, а не из второго списка в коде; - сервис печатает модель один раз при старте, а не на каждый запрос;
- guard требует
allowed: trueдо вызова действия; - внешний вызов курьерской службы не находится внутри модели;
- CI ловит ручную правку напечатанного кода режимом
--check; - README перечисляет, какие переходы состояний разрешены и почему.
5. Типичные ошибки капстоуна
- Хардкодить список полей формы вместо чтения
flang ast— тогда форма и модель расходятся при первом же новом поле. - Вызывать
shipping.createShipmentбез проверкиdecision.allowed— guard теряет смысл, если его ответ не читают. - Коммитить напечатанный
.tsбез шага--checkв CI — правка мимо модели останется незамеченной до продакшена. - Принимать вход HTTP без сверки типов — неверный вход должен вернуться клиенту
как
400, а не всплыть как500. - Читать код 3 как «всё хорошо».
flang check --proofс кодом 3 значит, что часть обещаний проверена только на примерах;flang runтакую программу без--trustне считает. - Склеивать текст утверждения из пользовательского ввода. Номер заказа уходит в
факты как данные, а не в текст
--claims; guard так и сделан.
6. Задание для ролей
Junior добавляет поле в объект «Заказ» и проверяет, что форма получила
контрол без правки JSX, а необязательное поле (иногда является) стало
необязательным. Middle строит Node-эндпоинт и отдаёт ошибки входа как 400, а
не 500. Senior проектирует снимок данных для flang facts и транзакционную
границу вокруг guard — где кончается ответственность модели и начинается
optimistic lock. Lead проверяет, что имена в модели совпадают с языком
предметного эксперта, и решает, какие обещания с «сеткой» команда принимает.
Агент может предложить новый пример, но обязан пройти flang check --proof и
flang test прежде, чем предложение попадёт в pull request.
Практика в песочнице
- Поменяйте второй пример на сумму 99999 и ожидание 9999.9 — проверка пройдёт, а потолок скидки перестанет достигаться ни одним примером. Верните пример.
- Удалите
случай «Создан»в «Допуске отгрузки» и прочитайтеFLANG_MATCH_NOT_EXHAUSTIVE. - Добавьте в
тип «Состояние заказа»вариант «Отгружен» и посмотрите, сколько разборов компилятор попросит дописать.
Критерий зрелости
Проект готов не тогда, когда модель выглядит красиво, а когда удалено настоящее
дублирование: одна модель управляет вычислением и тестом, а адаптеры читают
flang ast и напечатанный код. При этом действия, интерфейс и инфраструктура
остаются в своих слоях — модель не подменяет ни репозиторий, ни шину событий,
ни React.
Вернитесь к каталогу прикладных кейсов, выберите ближайший к своей работе и повторите капстоун на своей предметной области: один объект, одна функция с примерами и обещанием, одна функция допуска и один адаптер (HTTP, форма или CLI), который не затаскивает побочные действия внутрь модели.
Куда дальше: то, что начинается за границей спецификации
Модель в этом курсе — маленькая часть flang. Язык умеет больше, чем нужно для
правил: списки (отобразить, отфильтровать, свёртка), рекурсию с
доказанным завершением, строки, свои типы с вариантами и план действий с
файлами, процессами и сетью (план, flang io). Значит, инструмент вокруг
правила — парсер своего формата, сборку отчёта, проверку CSV — можно писать на
том же языке, а не только само правило.
У границы есть и вторая сторона, и её стоит знать заранее. В логике языка нет
состояния во времени: утверждение «после оплаты заказ не может стать
черновиком» не выражается. Нет доказательств о побочных действиях: план
описывает действие, исполняет его среда, и про внешний мир ядро не говорит
ничего. Процессы есть, утверждений о гонках и взаимных блокировках нет. И
flang run, и напечатанный код сами не доказаны: доказательство привязано к
flang check.
Любая модель печатается в десять языков — C, C++, C#, Elixir, Go, Java,
JavaScript, TypeScript, Python, Rust — одной командой flang emit (глава
«Из Python, Go и shell»).
Если захотите разобраться, как устроен сам язык — как доказывается завершение, что умеет ядро доказательств и где его граница, — это отдельный трек: «flang».