Каталог спек: стенд, проверка и слепок

Соседняя страница — Спеки: доказанное правило — показывает, ЧТО такое спека-программа. Эта отвечает на следующий вопрос: как из спек собирается каталог, который не расползается, и чем он проверяется.

Каталог живёт в дереве и называется fspec/. Это не спецификация языка — спецификация языка лежит в docs/flang/SPEC.md. Это образец пакета и одновременно стенд: сорок с лишним правил предметной области, записанных программами, правило их приёмки, проверяющая программа, память о том, что стояло вчера, набор нарочно испорченных случаев и набор программ, показывающих границу.

Что где лежит

Разбор устройства мастера уточнений — отдельный документ, docs/fspec/clarifications.md.

Стенд написан на flang целиком: ни одного файла на JavaScript в каталоге нет. Это оказалось возможно потому, что проверка не разбирает .flang сама — она запускает компилятор процессом и читает ответ, а на это у языка есть поручения «Перечислить каталог», «Прочитать файл» и «Запустить процесс».

Как выглядит спека

Спека — не markdown, а программа. Вот первая спека каталога целиком, fspec/spec/01-discount-cap.flang, без комментариев:

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

тотальная функция «Потолок скидки»
  принимает сумма: число
  возвращает число
  обеспечивает «скидка не больше 30» результат не больше 30
  обеспечивает «zh: 折扣不超过 30» результат не больше 30
  обеспечивает «en: discount is at most 30» результат не больше 30
  пример «потолок»
    дано сумма равно 1000
    ожидается 30
  30

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

Связь со спекой, написанной раньше, — строка использует:

модуль «Спека 3: наценка за срочность»
  использует «Спека 2: промо» из "./02-promo.flang"

Ссылка — часть программы, а не проза: переименование спеки без правки наследницы ломает подключение сразу.

Правило приёмки

Записано на самом языке, в policy.flang. Спека принимается, только если каждое её утверждение доказано, и каждое утверждение предшественницы осталось в отчёте наследницы доказанным.

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

Что отвергается:

Цена названа честно. Истинное, но невыводимое утверждение тоже будет отвергнуто: ядро неполно, и образец неполноты лежит в дереве — flang/proof/examples/precondition.flang. Спека, упёршаяся в неполноту, — это заявка на новое правило ядра, а не повод ослабить приёмку порогом. Какие записи ядро берёт сегодня, разобрано на странице Какие обещания ядро берёт.

Что считается настоящим утверждением

Утверждение может быть доказано и при этом не говорить ничего. Ослабленное утверждение — то, которое переживает подмену тела заглушкой той же подписи: 0, "", нет, пустой список. Если заглушка тоже проходит, утверждение верно про ЛЮБУЮ функцию такой подписи, а про эту не говорит ничего.

Проверяется это прогоном, а не спором: скопировать функцию в отдельный файл, оставив подпись и обеспечивает, заменить тело заглушкой и позвать check.

модуль «Заглушка»

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

$ flang check zaglushka.flang --proof
zaglushka.flang: ПРОВЕРЕНО САМОСТОЯТЕЛЬНО — утверждений 1: доказано 1 … код возврата 0

Заглушка прошла — значит утверждение первой спеки ослаблено, и это не оговорка, а часть замысла: у функции с телом-константой содержательного обещания нет вовсе. Первые две спеки показывают, как выглядит СВЯЗЬ двух спек, а не как выглядит сильное утверждение.

Отсюда и выбор формы обещаний дальше по каталогу. Заглушку не переживают утверждения о длине ((длина результат) равен ((длина х) плюс 1)), о вхождении (результат содержит "…"), о булевой формуле, о полях записи и о границе, где границей стоит сам результат (цена не больше результат). Переживают — односторонние верхние границы (результат не больше 30) и неотрицательность (результат не меньше 0).

Слепок: память о том, что стояло вчера

Правило приёмки смотрит на спеки, КАКИЕ ОНИ СЕЙЧАС. Отсюда дыра: переписать цель утверждения, не тронув его имени, — и приёмка не заметит.

Дыру закрывает snapshot.txt — строка на каждое обещание, и в ней, кроме файла, функции и имени, стоит САМА ЦЕЛЬ дословно:

01-discount-cap.flang :: Потолок скидки :: скидка не больше 30 :: результат не больше 30

Проверка читает слепок первым делом и сверяет его со спеками в обе стороны:

• слепок → спеки: каждое записанное обещание стоит на месте и той же целью. Пропало — «правило снято молча». Цель переписана — «имя прежнее, обещание другое», и обе цели показаны рядом;
• спеки → слепок: каждое обещание спеки записано. Не записано — значит ничем не защищено, и завтра его можно переписать молча.

Слепок пишется отдельной командой, и это тоже правило:

flang io fspec/snapshot.flang

Слепок, обновляющийся молча вместе со спеками, не защищал бы ни от чего: он записал бы ослабление вместе с ним. Правка цели — это ДВА действия, и второе видно в разборе изменений отдельной строкой.

Откуда берётся цель. Из исходника спеки, а не из отчёта компилятора: в отчёте при утверждении стоит проза («доказано сведением цели с телом функции…»), и сверять по ней содержание значит сверять по формулировке доказательства. Разобранная цель в отчёте есть, но она втрое больше остального отчёта, и разбор такого JSON на flang стоит гигабайтов памяти. Поэтому цель читается из первоисточника — строки обеспечивает самой спеки, знак в знак.

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

Чего слепок НЕ делает: он не судит, слабее ли новая цель прежней. «Не больше 1000» и «не больше 30» для него просто РАЗНЫЕ. Он говорит другое и меньшее: содержание доказанного обещания не меняется молча.

Требование на другом языке

Для кода многоязычие вредно: два имени одного дробят сообщество. Для требования — наоборот: требование читает не программист, а тот, кто платит. Доказательство при этом одно на все языки, потому что доказывается не текст, а цель.

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

Переводится ИМЯ обещания. Имена функций, параметров и переменных — нет: тело у видов общее, и переведённое имя функции проверка отвергает отдельной бедой.

Метки языков — список ЗАКРЫТЫЙ, и перечислен он в функции «Метки языков» самой проверки. Будь он открыт, опечатка zn: перестала бы быть видом и стала бы ОТДЕЛЬНЫМ обещанием, которое ни с чем не сверяется, — тихое расхождение вместо красного. Отсюда цена, названная прямо: разделитель ": " в имени обещания означает метку языка и ничего другого.

Чего сверка НЕ умеет: прочитать перевод. Если китайский вид назван неверно, а цель при нём стоит верная, проверка промолчит — судить о СЛОВАХ ей нечем. Она судит о том, что формально: два вида одного обещания обязаны обещать одно и то же.

Подлог: проверка обязана краснеть

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

flang io fspec/forgery.flang --timeout 600000

Ловятся, в числе прочего: ослабление правила под тем же именем; спека без предшественницы; вид на другом языке, обещающий не то, что основной; опечатка в метке языка; переведённое имя функции; одно имя правила с двумя разными подписями; замкнутая ложь у функции без входов.

Сегодня стенд красен, и вот чем

Так выглядит прогон на 11 сентября 2026, двоичным 0.7.17 (коммит 2c40752d0; впервые снято 8 сентября на 0.7.14, с тех пор не изменилось):

$ flang io fspec/guard.flang
бед в системе спек: 79
03-urgency-markup.flang: утверждение «скидка с промо не больше 30» функции
«Скидка с промо» доказано у 02-promo.flang, а здесь его нет или оно ослаблено
…
код 1

Все 79 бед одной породы, и причина у них одна: отчёт check --proof больше не содержит утверждений подключённых модулей. Наследница получает отчёт «ПРОВЕРЕНО САМОСТОЯТЕЛЬНО», где стоят только её собственные утверждения, — а второе правило приёмки требует найти там утверждение предшественницы.

$ flang check fspec/spec/03-urgency-markup.flang --proof
  утверждений 1: доказано 1 (из них без теоремы 1, объявленным типом 1), сетка 0

Подлог тем же прогоном отвечает «расхождений 7 (подложенных случаев 19)», и шесть из семи — следствие той же перемены: случаи, ждавшие слов «не доказано — declared» и «ЗАМКНУТА», получают вместо них отказ на самом языке.

Красноту стенд не прячет: она записана в описи проверок дерева (docs/ci-inventory.md) словами «КРАСЕН по делу», а починка ведётся задачей задачника. Пишете свои спеки — держите в уме, что проверка в этом состоянии краснеет на каждой наследнице, а не только на вашей ошибке.

Границы: чего одна flang check не видит

Программы в experiments/ показывают, где компилятор говорит, а где молчит. Коды сняты 8 сентября 2026 двоичным 0.7.14 и перепроверены 11 сентября двоичным 0.7.17 (коммит 2c40752d0) командой flang check <файл> --proof:

Читается таблица так.

Три строки false-claim-* — не про доказуемость, а про истинность. Доказано ≠ правильно: ядро выводит то, что написано, и если написана ложь, поймает её пример, а не вывод. Ноль, пустое, край отрезка, минус ноль и «не число» стоят одной строки примера каждый — и дешевле боевого запуска. У «не числа» ядро с некоторых пор отвечает прямо, отдельной диагностикой FLANG_BOUND_ON_NAN, и называет контрпример словами.

Код 3 — это «НЕ ПРОВЕРЕНО». Утверждение высказано, доказательства при нём нет, ядро откладывает его на рантайм. Раньше такой файл получал код 0, и на этом стояла половина довода «одной flang check мало»; сегодня он получает свой код, и половина довода закрыта самим языком.

Строки с кодом 0 — то, ради чего каталог и проверяется. Ни один из двух последних случаев компилятор не считает бедой, и он прав: подключение с отбором — законная запись, замена правила — законная работа. Отличить отмену исподтишка от честной замены можно только зная, что стояло вчера, — то есть слепком и правилом приёмки, а не проверкой одного файла.

Ядро тут не виновато, и чинить его не надо. Непротиворечивость набора спек — это правило приёмки поверх отчёта о доказательствах, а не новое правило внутри ядра. Ровно оно и написано в policy.flang.

Как добавить спеку

1. Положите файл в fspec/spec/ с номером в начале имени: 43-….flang. Номер задаёт порядок, в котором спеки читает человек.
2. Первой строкой — модуль «Спека 43: …». Опирается на написанную раньше — второй строкой использует «Спека 42: …» из "./42-….flang".
3. Напишите функцию с обеспечивает «имя» …. Имя пишите так, чтобы оно читалось в отчёте о беде: оно туда и попадёт.
4. Прогоните проверку: flang io fspec/guard.flang. Получило утверждение «объявлено, не доказано» — либо цель сформулирована слишком широко, либо телу нечем её нести; ослаблять приёмку нельзя, а переписать цель или тело можно.
5. Проверьте утверждение подменой тела на заглушку. Пережило — переписывайте: доказано оно про подпись, а не про вашу функцию.
6. Впишите обещание в слепок: flang io fspec/snapshot.flang. Пока его там нет, проверка красит спеку словами «не записано в слепке».

Имена файлов — английскими словами, содержимое — русское. Транслит не годится ни в ту, ни в другую сторону.

Чего здесь нет

Вторая строка — главная незакрытая. Спецификация без тела в языке сегодня не высказывается вовсе, а с телом она уже наполовину реализация.

Полный решатель выполнимости (Z3 и подобные) сюда не годится и не будет: он отвечает «невыполнимо» без предъявления значения, на котором это видно. Принять такой ответ значило бы завести аксиому «внешний решатель не врёт», а аксиом в языке ноль. Подсказчиком он допустим: ищет он, а решает ядро по тому, что он предъявил.

Что почитать дальше

• Спеки: доказанное правило — зачем это всё, на сквозном примере.
• Что доказано, а что нет — числа по дереву.
• Какие обещания ядро берёт — какую запись ядро возьмёт, а какую отложит.
• Ядро отказало: чья это ошибка — коды отказов ядра.
• Служба для ИИ-помощника — как из недоказанного обещания получается вопрос к автору требования.