flang компилятор доказывает, что программа не зациклится 0.6.2 GitHub

Тавтология закрывается даром, поэтому число «доказано без теоремы» само по себе ничего не значит

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

Чем подтверждено. Замер 16 августа, функция «Противоположное» из flang/stdlib/higher-order.flang с телом 0 минус х (docs/benchmark2/05-…flang). Две строки в одном файле, обе проверены прогоном flang check --proof:

постусловие «результат есть нуль минус вход» (результат равен (0 минус х))
  — доказано сведением цели с телом функции: правило «тождество после переписки
    допущением» … обо ВСЕХ входах

постусловие «сумма с исходным — ноль» ((результат плюс х) равен 0)
  — сетка 5 значений (примеры функции). Это не доказательство

Содержательное утверждение о той же функции ядро не взяло. Взяло переписанное тело.

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

Правило на будущее. Считая, сколько утверждений закрылось без теоремы, разделяйте три класса и называйте все три:

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

Чем ограничено. Граница между «частичным» и «тавтологией» не машинная: после развёртки определения ядром содержательное утверждение результат равен («Делится на» от число и 2) тоже сводится к тождеству, но написано оно про связь двух функций библиотеки, а не про текст одной. Решать приходится глазами, и потому решение надо писать в отчёт, а не подразумевать.

Поправка от 20 августа 2026: разделять руками не надо, оно меряется прогоном.

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

Тавтология — постусловие вида результат равен Е, где Е есть само тело функции. Сравниваются деревья разбора без мест в исходнике. Никакого «на глаз».

Ослабленное — утверждение, пережившее подмену тела заглушкой того же объявленного типа. Подпись и текст утверждения остаются те же, тело заменяется на 0, "", нет или пустой список, ведомость считается заново. Утверждение, доказанное и при заглушке, верно про любую функцию этой подписи и про эту не говорит ничего. Это то же самое правило «снять правку и посмотреть, что покраснеет», приложенное не к коду, а к спецификации.

Опасение из абзаца выше — что развёртка определения сотрёт разницу — не подтвердилось, и вот почему: результат равен («Делится на» от число и 2) при теле нет отпадает, потому что «Делится на» осталась прежней и цель перестала сходиться. Развёртка стирает разницу между текстами, а подмена спрашивает про поведение — вопросы разные.

Чем подтверждено. benchmarks/proof-cost/schyot-20.mjs, ветка vypusk/vyrazimost. На точке ветвления (github/main = d3e27dad) счётчик печатает 2 содержательных из 20 — ровно то число, которое отчёт замера вывел руками. То есть машина воспроизвела ручную классификацию, а не заменила её другой. Раскладка там же: ослабленных 4, даровых 1, не проверено 2.

Чем ограничена сама поправка. Заглушка строится по объявленному типу результата, и типов у неё четыре. Функция, возвращающая объявленную сумму, запись или параметр типа, заглушки не получает, и её утверждение помечается НЕ ПРОВЕРЕНО — а не записывается в содержательные по умолчанию. На двадцати функциях таких два. Второе ограничение: примеры при подмене снимаются у обоих файлов, потому что они описывают настоящее поведение и у подменённого краснеют все разом; если утверждение несут примеры (по примеру), сравнить подмену нечем, и это тоже отдельная пометка, а не молчаливый зачёт.

Связано: bottleneck-moved-to-body-shape, proven-is-not-correct, unstatable-costs-more-than-unprovable

Дополнение. Классификацию, которую эта заметка предлагала делать руками, можно свести к механической проверке: подменить тело заглушкой той же подписи и посмотреть, осталось ли утверждение истинным. Замер на двух модулях и разбор форм — в darovoe-utverzhdenie-uznayotsya-podmenoy-tela-zaglushkoy. Там же стоит и второе утверждение про «Противоположное», которое здесь названо недоказуемым: оно доехало в библиотеку с оговоркой «х больше 0» — без неё оно ЛОЖНО на не числе, потому что «не число плюс не число равно нулю» ложно.