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

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

Часть такой проверки можно сделать машинной и запускать до того, как написана первая строка кода. Условие одно: носитель требования — не markdown, а программа на flang, где требование записано обещанием обеспечивает. Компилятор отвечает, доказано ли оно. А каталог спек, который заводит flang new, сверяет спеки между собой: не ослабила ли новая спека прежнюю и не обещают ли две спеки несовместимого.

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

Две спеки об одном правиле — скидке подписчику. Первую, fspec/spec/02-discount-cap.flang, написали финансы:

модуль «Спека 2: потолок скидки»

тотальная функция «Скидка подписчику»
  принимает сумма: неотрицательное
  возвращает число
  обеспечивает «скидка не больше тридцати» результат не больше 30
  пример «обычная подписка»
    дано сумма равно 1000
    ожидается 10
  если сумма больше 100000
    то 30
    иначе 10

Вторую, fspec/spec/03-loyal-subscriber.flang, — продажи, через полгода:

модуль «Спека 3: давнему подписчику»

тотальная функция «Скидка подписчику»
  принимает сумма: неотрицательное
  возвращает число
  обеспечивает «давнему подписчику не меньше сорока» результат не меньше 40
  пример «давний подписчик»
    дано сумма равно 1000
    ожидается 40
  если сумма больше 100000
    то 50
    иначе 40

Каждая спека сама по себе в порядке: flang check --proof доказывает её обещание для всех входов и выходит кодом 0. Ни одна строка не помечена как «спорная». Конфликт находит проверка каталога спек — flang io fspec/guard.flang:

02-discount-cap.flang: спеки 02-discount-cap.flang и 03-loyal-subscriber.flang об одном правиле «Скидка подписчику» НЕСОВМЕСТИМЫ: 02-discount-cap.flang обещает «скидка не больше тридцати» целью «результат не больше 30», 03-loyal-subscriber.flang обещает «давнему подписчику не меньше сорока» целью «результат не меньше 40» — вместе эти цели не выполнимы ни на одном входе. Это противоречие НАБОРА требований: рёбер «использует» между этими спеками нет, и потому до сих пор их не сверяло ничто. Решите, какое из двух правил верно

Код возврата 1, код ошибки FLANG_SPEC_РАЗЛАД.

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

1. flang check --proof судит каждое обещание каждой спеки: «доказано» для всех входов, «сетка N» (проверено только на N примерах) или «объявлено, не доказано». Спека с несошедшимся примером не проходит проверку вовсе.
2. Проверка каталога — сама программа на flang, fspec/guard.flang. Она исполняется командой flang io: читает настройку settings.txt (путь к компилятору и каталог спек), перечисляет файлы spec/*.flang, для каждого зовёт flang check --proof --json и разбирает отчёт.
3. Правила согласия лежат рядом, в fspec/policy.flang, обычными функциями с обещаниями и примерами. Спека принимается, только если у каждого её обещания вердикт «доказано»; «сетка» и «объявлено, не доказано» доказанными не считаются.
4. Итог — одна строка JSON в stdout и код возврата: 0, если спеки согласны, 1 и FLANG_SPEC_РАЗЛАД со списком бед, если нет.

Раскладка каталога

flang new скидки заводит пакет:

скидки/скидки.flang                    модуль пакета
скидки/flang.package                   имя и версия
скидки/README.md
скидки/fspec/spec/01-order-steps.flang образец спеки
скидки/fspec/guard.flang               проверка каталога
скидки/fspec/policy.flang              правила согласия спек
скидки/fspec/settings.txt              компилятор и каталог спек
скидки/fspec/snapshot.txt              слепок обещаний
скидки/fspec/README.md

Одна спека — один файл в fspec/spec/ с номером в начале имени и модулем «Спека N: …». Номер даёт порядок, имя файла попадает в каждое сообщение проверки — поэтому спеку удобно называть так же, как задачу в трекере.

snapshot.txt — слепок обещаний: по строке на каждое обещание, с файлом, функцией, именем и целью:

01-order-steps.flang :: Шаги приёмки заказа :: шагов ровно три :: (длина результат) равен 3
01-order-steps.flang :: Шаги приёмки заказа :: первый шаг — оплата :: результат содержит "оплата"
02-discount-cap.flang :: Скидка подписчику :: скидка не больше тридцати :: результат не больше 30

Слепок лежит в репозитории и меняется через ревью, как код. В нём записано, что команда уже приняла, — и именно с ним проверка сравнивает спеки.

Две оговорки о поставке, обе проверены на 0.7.29. Сборка, которую ставит install.sh, образца fspec/ не везёт, и flang new отказывает:

FLANG_NEW: не найден образец fspec/ (guard.flang рядом с policy.flang) — искали
в $FLANG_FSPEC_TEMPLATE_DIR и в <каталог двоичного>/../fspec. Пакет не создан.

Лечится переменной FLANG_FSPEC_TEMPLATE_DIR, указывающей на каталог fspec/ из репозитория языка той же версии. Вторая: README каталога зовёт flang io fspec/snapshot.flang, чтобы переписать слепок, но flang new этот файл не копирует. Его берут из того же каталога репозитория — или дописывают строку в snapshot.txt руками: проверка сама печатает, какую.

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

Требование — обещание с вердиктом

Требование записывается обещанием обеспечивает у функции, которая это правило считает. Компилятор отвечает тремя разными словами, и путать их нельзя: «доказано» — верно для всех входов; «сетка N» — проверено на N примерах, как unit-тестами; «объявлено, не доказано» — нет ни доказательства, ни примеров. Каталог спек принимает только первое. Спека с обещанием, которое держится на примерах (здесь — fspec/spec/04-volume.flang), отвергается:

04-volume.flang: спека не проходит проверку языка — {"ledger":1,"module":"Спека 4: скидка за объём", …

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

Слепок не даёт молча ослабить правило

Если спеку правят, проверка сравнивает её обещания со слепком. Снятое обещание и переписанная цель — ошибки, а не предупреждения:

03-loyal-subscriber.flang: утверждение «давнему подписчику не меньше сорока» функции «Скидка подписчику» стояло в слепке целью «результат не меньше 40», а в спеках его больше нет — правило снято молча
02-discount-cap.flang: у утверждения «скидка не больше тридцати» функции «Скидка подписчику» переписана ЦЕЛЬ. В слепке: «результат не больше 30». Сейчас: «результат не больше 1000». Имя прежнее, обещание другое

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

Несовместимые пределы между спеками

Проверка находит пары обещаний об одной функции из разных файлов спек, цели которых вместе не выполнимы ни на одном входе. Это пример из начала главы: «не больше 30» против «не меньше 40». Сравниваются пределы вида результат не больше N, результат не меньше N и равенства числу.

Контрпример для одной функции

Два несовместимых обещания у одной функции (файл contra.flang):

модуль «Два требования»

тотальная функция «Скидка»
  принимает сумма: неотрицательное
  возвращает число
  обеспечивает «требование продаж: скидка не меньше сорока» результат не меньше 40
  обеспечивает «требование финансов: скидка не больше тридцати» результат не больше 30
  если сумма больше 100000
    то 50
    иначе 10

flang 0.7.32 останавливает проверку с кодом 1. При сумме 0 функция возвращает 10 и нарушает требование продаж. Такой ответ указывает на одно нарушенное обещание и конкретный вход. Сопоставление двух требований по-прежнему делает проверка спек.

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

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

• Спорят только пределы о числе. Пара «не больше 30» и «не меньше 40» находится. Цели другой формы — содержит, вызов функции-предиката, условие на поле входа — проверка не сравнивает: «цель не о числе — спора не видно».
• Спорят только функции с одним именем. Если две спеки говорят об одном правиле разными именами — «Скидка подписчику» и «Скидка давнему клиенту», — конфликт найден не будет. Связать два имени одного понятия во flang 0.7.29 нечем.
• Только между файлами спек. Два обещания одной функции в одном файле не сравниваются — как и в обычной flang check.
• Только доказанные требования. Требование, которое держится на примерах, в каталог не попадает вовсе, а значит, и со спорами не сверяется. Для правил с процентами это частый случай.
• Внешние данные, время, состояние. Правило, зависящее от справочника, курса валют, даты или истории заказа, проверить нечем: в логике языка нет ни времени, ни побочных действий.
• Сама проверка не доказана. flang io fspec/guard.flang без ключа --trust судит доказанность самой проверки, считает 2 минуты 43 секунды, набирает 2,6 ГиБ памяти и отказывается: «не доказано: утверждений 133: доказано 80, сетка 53». С --trust та же проверка идёт 9–11 секунд. В CI её запускают с --trust и называют это вслух.

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

Роль агента

ИИ-агент хорошо переводит разговор с заказчиком в черновик спеки: функцию, обещание и примеры. И хорошо объясняет словами, почему проверка отказала. Чтобы агент проверял себя тем же компилятором, его подключают к службе flang --mcp-mode: средство flang_check возвращает отчёт целиком, а flang_prove отвечает, чем доказано одно названное обещание. Три вердикта служба отдаёт порознь, и «сетку» агент не сможет выдать за «доказано».

Арбитром агент не работает. Решение принимает не текст его ответа, а детерминированная проверка: код возврата flang io fspec/guard.flang и строка с перечнем бед воспроизводимы, а «кажется, противоречий нет» — нет. То же правило — в главе про агентов (https://courses.digitable.life/post/spec/10-ai-agents/).

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

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

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

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

1. Отчёт песочницы покажет четыре обещания: одно доказано, три — «сетка». Какие из них годились бы в каталог спек как есть? Только «за очень крупную покупку не больше потолка»: остальные три проверка каталога отвергла бы как недоказанные.
2. Добавьте функции «Рассчитать скидку» второе обещание результат не меньше 20000 и проверьте. Отчёт не скажет, что оно несовместимо с «скидка ограничена»; покраснеют примеры, на которых скидка меньше 20 000, — с FLANG_PROPERTY и кодом 1.
3. Перепишите «Очень крупная покупка» так, чтобы она возвращала 20000 вместо 15000, и проверьте. Правку поймает пример «очень крупная покупка»: он нарушит обещание «за очень крупную покупку не больше потолка», и проверка остановится с FLANG_PROPERTY и кодом 1. В каталоге спек ту же правку поймал бы ещё и слепок.

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

• Закрывать FLANG_SPEC_РАЗЛАД переименованием функции. Спор исчезнет, потому что проверка сравнивает функции по имени, но требования противоречить друг другу не перестанут. Расходиться перестанут только изменённые пределы.
• Переписывать слепок вместе со спекой не глядя. Слепок нужен ровно для того, чтобы ослабление было видно на ревью. Переписанный заодно со спекой, он ничего не ловит.
• Записывать требование, которое ядро не докажет, и ждать, что каталог его примет. Обещание на примерах — «сетка», и проверка каталога его отвергнет. Это не поломка: требование либо переписывают так, чтобы его условие совпало с ветвью тела, либо оставляют проверенным на примерах вне каталога.
• Считать молчание проверки чистотой. Нет спора — значит, нет пары числовых пределов об одной функции. Спор о функциях с разными именами, о нечисловых целях или внутри одного файла проверка не видит.
• Ставить в CI проверку без --trust и удивляться коду 3. Проверка каталога сама не доказана. Без ключа она не запускается, а с ключом это нужно сказать в описании шага.

Чек-лист

• Требование записано обещанием обеспечивает с примерами до того, как заведена ветка реализации.
• flang check --proof по спеке выходит кодом 0: все её обещания доказаны.
• Каждая фича — отдельный файл в fspec/spec/ с номером в имени; номер совпадает с задачей в трекере.
• Одно правило называется одной функцией с одним именем во всех спеках — иначе споры между ними не ищутся.
• Слепок snapshot.txt лежит в репозитории и меняется только через ревью.
• На каждом pull request запускается flang io fspec/guard.flang --trust, и ненулевой код блокирует слияние.
• Известно, чего проверка не видит: нечисловые цели, синонимы, споры внутри одного файла, требования на примерах.
• Найденный спор разобран человеком: проверка показывает, что требования расходятся, но не какое из них правильное.

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