Требования, которые проверяются до реализации: корпус спек, конституция и ftspec

Новое требование сегодня проверяют памятью. Кто-то в команде помнит, что предел скидки ограничили тридцатью процентами на совете директоров в марте, и замечает, что свежая спека обещает сорок. Если не помнит — противоречие уезжает в реализацию и всплывает на проде, когда обе ветки кода уже написаны и отгружены.

Проверку можно сделать машинной и запускать до того, как написана первая строка кода. Условие ровно одно: носитель требований — не markdown, а компилируемая модель. Инструмент называется ftspec и живёт в github.com/digitable-lol/flang рядом с компилятором проекта ftsc и исполнителем ftsvm. Собственного парсера у него нет: разбор, связывание модулей и законы функторов делает ftsc, исполнение моделей — ядро FTS.

Минимальный пример

Конституция проекта — обычная модель FTS. Её утилиты играют роль инвариантов: принимают факты решения и возвращают число нарушений, ноль значит «всё в порядке». Служебное поле итог — результат проверяемой утилиты спеки.

категория «Конституция»

  объект «Решение»
    сумма является деньгами
    итог является деньгами

  утилита «Предельная скидка»
    принимает «Решение»
    возвращает число
    начинает с 0

    правило «Скидка превышает тридцать процентов суммы»
      если итог больше 30 процентов от поля сумма
      то результат равен 1

    свойство «Нарушение считается один раз»
      результат не больше 1

    пример «Скидка в пределах»
      дано сумма равна 10000
      дано итог равен 2000
      ожидается результат равен 0

    пример «Скидка ровно на пределе»
      дано сумма равна 10000
      дано итог равен 3000
      ожидается результат равен 0

    пример «Скидка сверх предела»
      дано сумма равна 10000
      дано итог равен 4000
      ожидается результат равен 1

В файле корпуса перед категорией стоит ещё строка модуль «Конституция» — её снимает ftsc, ядро видит уже саму категорию. Примеры обязательны и здесь: инвариант, который сам не проверен, проверять другими нечем.

Требование живёт в отдельной категории и выглядит так же обыденно:

    правило «Давнему подписчику сорок процентов»
      если «давний подписчик» равен да
      и сумма не меньше 500
      то результат равен 40 процентов от поля сумма

Ни одна строка тут не помечена как «спорная». Конфликт находит ftspec check.

Что делает компилятор

1. ftsc разбирает файлы корпуса, связывает модули по использует и экспортирует и проверяет законы функторов. Ошибки этого слоя приходят с кодами FTSC_MODULE_* и FTSC_FUNCTOR_* и до анализа требований дело не доводят: несвязываемый корпус проверять бессмысленно.
2. Ядро исполняет примеры всех моделей корпуса — конституции, спек и памяти. Модель с расходящимся примером не считается достоверной.
3. ftspec сравнивает условия правил из разных спек, прогоняет утилиты спек против инвариантов конституции и считает покрытие правил примерами.
4. Результат — JSON в stdout, диагностики в stderr, ненулевой код возврата при конфликтах: тот же контракт, что у ядра и у ftsc check.

Раскладка корпуса

constitution.fts                              инварианты проекта
memory/001-предел-скидки.fts                  принятые решения
specs/001-скидка-постоянному-клиенту/spec.fts одна фича — одна категория
mapping/скидки-в-подписки.fts                 функторы между категориями спек

Роль файла задаётся местом в дереве, а не содержимым: иначе её пришлось бы объявлять внутри файла, а объявление можно забыть. Идентификатор спеки — имя её каталога, поэтому в отчёте фича называется так же, как в трекере.

Четыре места отвечают на четыре разных вопроса. constitution.fts — что верно всегда и не обсуждается в отдельном требовании. specs/ — что требует конкретная фича; одна фича — одна категория, потому что категория и есть граница, внутри которой имена объектов и полей что-то значат. memory/ — почему решили именно так: решение, записанное моделью с примерами, остаётся проверяемым через три года, а записанное абзацем в переписке — нет. mapping/ — словарь между спеками: объекты разных категорий формально разные типы, и только функтор даёт право считать «Заказ» одной спеки и «Подписку» другой одним понятием.

Что проверяется машиной

Конфликт правил разрешим интервальной арифметикой

Условие правила FTS — конъюнкция сравнений поля с операндом, операторов ровно шесть. Если операнд константа, конъюнкция распадается по полям: они независимы, поэтому пересечение двух условий непусто ровно тогда, когда непусто пересечение ограничений по каждому полю. А ограничение на одно поле — это отрезок с открытыми или закрытыми концами и конечным множеством выколотых точек от не равен (число), подмножество {да, нет} (признак) или «всё, кроме перечисленного» (строка и дата). Все три случая решаются точно и за линейное время: SMT-решатель здесь не нужен, задача до него не дотягивает. Считается это без округлений в свою пользу — > 5 и ≥ 5 вместе дают (5, +∞), а не [5, +∞); ≥ 5 и ≤ 5 — ровно точку 5; ≠ 5 на [0, 10] выкалывает точку, а на [5, 5] делает множество пустым.

Непустое пересечение само по себе не конфликт: правила могут спокойно срабатывать вместе. Конфликт — когда несовместимы действия. set в разные значения — конфликт. set против add — конфликт, потому что итог зависит от порядка применения, а порядка между спеками не существует. Вместе с ответом выдаётся свидетель — конкретный вход, на котором требования расходятся:

FTSPEC_RULE_CONFLICT — правила «Постоянному клиенту десять процентов» и
«Давнему подписчику сорок процентов» (объект «Подписка») применимы одновременно
при «давний подписчик» = да, «сумма» ∈ [1000, +∞): оба правила задают
результат, но разными значениями
  пример входа: {"давний подписчик":true,"сумма":1000}

Со свидетелем не спорят — его подставляют в обе модели и смотрят. Это другой разговор, чем «мне кажется, тут противоречие».

Нарушение конституции проверяется на сетке входов

Утилита спеки прогоняется на конечной сетке, выведенной из порогов её собственных условий: для числового поля берутся все пороги и их соседи «порог ± шаг» (граница не меньше 500 различает 499, 500 и 501), для признака — оба значения, для строки — константы из условий плюс одна посторонняя. В каждой точке считается результат утилиты, он подставляется в поле итог входа инварианта, и инвариант исполняется ядром. Ненулевой ответ — FTSPEC_CONSTITUTION, и в диагностике назван вход:

утилита «Скидка подписчику» нарушает инвариант «Предельная скидка» конституции
при «сумма» = 500, «давний подписчик» = да: результат 200, нарушений 1

Размер сетки ограничен, усечение детерминировано: повторный запуск даёт тот же вердикт. Точка, на которой утилита сама отвергает вход своим свойством, выбывает — спорить с моделью о её же допусках не дело проверяющего.

Покрытие, дубли, осиротевшая память, функторы

FTSPEC_UNCOVERED (предупреждение) — правило не активируется ни одним примером. Активация определяется исполнением через ядро: строится утилита-зонд из правил 0..i, где у правила i действие заменено на метку; предыдущие правила остаются нетронутыми, потому что условие может ссылаться на накопленный результат. Непокрытое правило — не ошибка, но это ровно то, чего никто не проверял.

FTSPEC_RULE_DUPLICATE (предупреждение) — одинаковые условия и действие в двух спеках. Не конфликт, а заявка на общий модуль.

FTSPEC_MEMORY_STALE (ошибка) — решение в memory/ ссылается на файл или категорию, которых больше нет. Память, ссылающаяся в пустоту, хуже отсутствующей: её продолжают цитировать.

Законы функторов — FTSC_FUNCTOR_* — приходят целиком из ftsc check: тотальность, типы полей, форма морфизма, сохранение композиции.

Честная граница

Это не доказательство непротиворечивости требований. Проверяются четыре конкретные вещи, и ни одна не является полной.

• Зависимости между полями за пределами сравнений с константой. Условие если скидка больше 30 процентов от поля сумма связывает два поля, и покоординатное пересечение перестаёт работать. Такие пары правил считаются в summary.skippedPairs: они не «проверены и чисты», они не проверены.
• Кванторы и коллекции. «Ни один заказ клиента не должен…» на FTS не выражается — в языке нет ни списочного типа, ни рекурсии. Такие требования инструмент не видит вовсе.
• Внешние данные. Правило, зависящее от справочника, курса валют или времени, проверить нечем: модель их не содержит.
• Нарушение строго между узлами сетки. Выбор точек обоснован эмпирически: поведение правил меняется на границах условий. Нарушение, живущее внутри интервала и не достающее до края, будет пропущено. Уменьшение шага расширяет сетку, полноты не даёт.
• Синонимы, не записанные функтором. Если две спеки говорят об одном понятии разными словами и это нигде не объявлено, конфликт найден не будет. Сделано намеренно: угаданный синоним даёт ложную тревогу, а она дороже пропуска — после третьей команда перестаёт читать отчёт.
• Два правила добавить не считаются конфликтом. Сложение коммутативно, итог не зависит от порядка. Абсурдность суммарной скидки в 60 процентов — суждение человека; машине его сообщают, записав предел в конституцию, и только тогда он начнёт нарушаться.

Иначе говоря, инструмент отвечает на вопрос «есть ли вход, на котором два требования расходятся», и отвечает точно там, где они записаны сравнениями с константами. Всё остальное он честно называет непроверенным.

Роль агента

Навыки Digit лежат в github.com/digitable-lol/digit, в skills/software-development/, и разложены по шагам, а не по инструментам. fts-constitution заводит инварианты проекта. fts-specify превращает требование заказчика в категорию с правилами, свойствами и примерами. fts-admit прогоняет ftspec admit <корпус> --spec specs/003-промокод и получает вердикт по одной спеке: в ответе остаются только диагностики, в которых участвует она сама. Корпус может годами жить с известным техдолгом — это не повод отклонять новое требование, если оно ничего не ломает. fts-memory дописывает принятое решение в memory/ моделью с примерами.

Ключевое здесь то же, что в модуле про агентов (https://courses.digitable.life/post/fts/10-ai-agents/): решение принимает не текст ответа модели, а детерминированная проверка. Агент хорошо переводит разговор с заказчиком в черновик спеки и хорошо объясняет словами, почему ftspec отказал. Арбитром он не работает: accepted: true и код возврата воспроизводимы, а «кажется, противоречий нет» — нет.

Чем это отличается от GitHub Spec Kit

Spec Kit решает ту же задачу и расставляет те же сущности: конституция, спеки по фичам, план, задачи. Разница в носителе. Там спека — markdown, а непротиворечивость оценивает языковая модель: ответ зависит от формулировки промпта, от версии модели и от того, что попало в контекст, и два прогона на одном корпусе могут разойтись. Здесь спека компилируется, проверка детерминирована, свидетель конфликта — конкретный вход, а не абзац рассуждения; шаг ставится в CI и блокирует merge. Из той же модели ftsc печатает код на восьми языках, поэтому спека и реализация не расходятся физически.

Цена названа честно: FTS — маленький язык. Нет коллекций, кванторов, рекурсии, строковых операций, вызова утилиты из утилиты. Требования, которые в него не укладываются, остаются текстом и проверяются глазами — как раньше. Выбор не между «всё проверено» и «ничего не проверено», а между «часть проверена машиной, и известно какая» и «всё проверено памятью того, кто был на совещании».

Практика в песочнице

1. Правило «Большая покупка» ограничено порогом 10000. Выпишите порог и соседей порог ± 1 — это узлы сетки, на которых проверялся бы инвариант конституции для этой утилиты.
2. В правиле «Постоянный клиент» замените то добавить 5 процентов на то результат равен 5 процентов и запустите примеры. «Большая покупка постоянного клиента» перестанет сходиться: 3000 против 1000. Ровно поэтому set против add между двумя спеками считается конфликтом — итог зависит от того, какое правило применили раньше, а порядка между спеками нет.
3. Добавьте правило с порогом выше всех значений в примерах (если сумма больше 1000000). Модель останется зелёной — этот случай ловит FTSPEC_UNCOVERED, а не тесты.

Типичные ошибки

• FTSPEC_RULE_CONFLICT закрывают переименованием правила. Имя не двигает границы условия: свидетель останется тем же входом. Расходиться перестанут только изменённые пороги или действия.
• Спека без функтора и удивление, что конфликт не найден. Пока mapping/ не говорит, что «постоянный клиент» одной категории — это «давний подписчик» другой, правила сравнивать не с чем. Молчание означает «не проверено», а не «чисто».
• Инвариант конституции без примеров. Такая утилита исполняется, но проверять ею чужие спеки — доверять непроверенному судье.
• Пустая конституция. Если предел нигде не записан, нарушать нечего, и FTSPEC_CONSTITUTION не сработает ни на каком корпусе. Отсутствие диагностик здесь — не признак здоровья.
• ftspec check на pull request вместо ftspec admit. check валит сборку за старый техдолг корпуса и учит команду игнорировать красный шаг.
• summary.skippedPairs не читают. Ненулевое значение при зелёном вердикте — самая ценная строка отчёта.

Чек-лист

• Требование записано моделью с примерами до того, как заведена ветка реализации.
• Конституция существует, её инварианты возвращают число нарушений, и их собственные примеры сходятся.
• Каждая фича — отдельный каталог в specs/ и отдельная категория; имя каталога совпадает с идентификатором в трекере.
• Понятия, названные в двух спеках по-разному, связаны функтором в mapping/ — иначе конфликт между ними не ищется.
• Принятое решение попадает в memory/ моделью, а не абзацем в переписке.
• На pull request запускается ftspec admit --spec <спека>, на master — ftspec check; оба блокируют по ошибкам, а не по предупреждениям.
• skippedPairs, непокрытые правила и число узлов сетки прочитаны: это границы проверки, а не служебный шум.
• Свидетель конфликта разобран человеком: он показывает, что требования расходятся, но не какое из них правильное.

Кейсы каталога по этой теме