Петля постусловия развязана преобразованием программы, а не флажком при работе, — и круг «туда и обратно» стал выразим

Постусловие, ссылающееся на свою функцию, давало FLANG_RECURSION_LIMIT при ДОКАЗАННОЙ тотальности:

обеспечивает «переворот переворота — исходное» («Переворот» от результат) равен элементы
→ FLANG_RECURSION_LIMIT: функция «Переворот» исчерпала лимит шагов (40000000)
                          на глубине вызовов 1

Петля видна целиком: постусловие считается после КАЖДОГО возврата, значит вложенный вызов из самого постусловия считает его снова. То же у взаимных ссылок — «Меньшее», говорящее о «Большем», плюс «Большее», говорящее о «Меньшем». Цена была не «неудобно», а НЕВЫРАЗИМО: круг «разобрал и собрал обратно» — самый частый вид полной спецификации — написать было нельзя ни для одной функции.

Правило старое и не наше

В Eiffel и JML проверка контрактов на время вычисления контракта выключается. Довод тот же: постусловие есть СПЕЦИФИКАЦИЯ, а не работа программы, и проверять спецификацию внутри проверки спецификации незачем — тот же вложенный вызов проверится на своём настоящем месте.

Почему преобразованием программы, а не флажком «мы внутри постусловия»

Флажок пришлось бы завести ДЕВЯТЬ раз: в вычислителе и в каждой из восьми целей печати. Три из восьми изменяемого состояния не имеют вовсе — у Elixir постусловие печатается как Flang.Rt.post(…) без всякого контекста, — то есть флажок туда не кладётся в принципе. Девять реализаций одного правила расходятся молча, и это ровно тот класс беды, ради которого здесь заведены подделки.

Преобразование делается ОДИН раз, над разобранной программой («Развязать постусловия»): у функций, достижимых из зацикленного постусловия, заводится ДВОЙНИК с тем же телом и без постусловий, а вызовы внутри постусловия переписываются на двойников. Дальше вычислитель и все восемь целей получают программу, в которой петли нет по построению, и ни одна из девяти сторон о правиле не знает.

Граница узкая нарочно, и второе ребро обязательно

Двойники заводятся только когда петля ЕСТЬ: имя функции достижимо из её собственного постусловия по рёбрам «тело» И «постусловие». Второе ребро не украшение — петля «Меньшее»↔«Большее» идёт тело→контракт→тело→контракт, и без него не ловится вовсе.

Мерено на дереве: в flang/stdlib/lists.flang (28 функций) от постусловий достижимо 5 функций, зацикленных постусловий 0; в result.flang (11 функций) — 2 и 0. То есть преобразование сегодня не трогает ни одной программы репозитория и начнёт трогать ровно там, где сегодня стоит отказ.

Подделка в двух половинах, и одной мало

Опасность правила ровно одна: сняв проверку шире, оно проглотит НАРУШЕНИЕ.

• krug-tuda-i-obratno.flang — истинный круг плюс пара имён: flang check проходит без замечаний (до правки — FLANG_RECURSION_LIMIT);
• poddelka-razvyazka-postusloviy.flang — ложный круг: flang check отвергает словами FLANG_PROPERTY «круг переворота лжёт»;
• poddelka-krug-pri-rabote.flang — программа ПЕЧАТАЕТСЯ в C, собирается и зовётся: на [1] круг сходится, на [1, 2] собранная программа отвечает FLANG_PROPERTY. Примеры автора такого входа не содержат, и flang check файл принимает НАРОЧНО: без прогона напечатанного нельзя отличить «проверка жива» от «проверка снята вовсе».

Чем подтверждено. Ветка u/dokazuemost, основание github/main = 7e8495ec. Прогон node flang/scripts/poddelki-yadra.mjs: 7 файлов, аксиом ноль, нарушений 0. flang check по 57 файлам (flang/stdlib, flang/proof/examples): красных 0.

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

Связано: a-postcondition-runs-on-every-call-so-a-walk-inside-it-changes-the-cost-order, a-proved-postcondition-no-longer-reaches-printed-code, substantive-and-provable-claims-barely-overlap