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

Постусловие на обработчике заводит восьмой вид отказа мимо замкнутого множества

Множество достижимых отказов процесса объявлено замкнутым и вычислимым: видов семь (flang/src/failures.mjs:220, ВИДЫ_ОТКАЗА), отказ, который процесс может выдать, а надзор не разбирает, — ошибка сборки FLANG_UNCOVERED_FAILURE. Обещание записано прямо: анализ «требует надзора там, где отказа может и не быть, но никогда не молчит там, где он может быть» (failures.mjs:203).

Строка обеспечивает у обработчика делает это обещание неправдой. Нарушенное постусловие бросается вычислителем кодом FLANG_PROPERTY (flang/src/interpret.mjs:288,874), нарушенное предусловие — FLANG_PRECONDITION (:311,435). Ни того, ни другого в КОДЫ_ОТКАЗА нет, и слов «постусловие», «предусловие», «обеспечивает» в failures.mjs нет ни одного (проверено grep: 0 вхождений каждого). Планировщик же кладёт код отказа в журнал как есть — conc.mjs:1085 берёт то, что бросил вычислитель.

Чем подтверждено. Прогон на ветке work/chto-utverzhdat-o-processah, 17 августа 2026. К flang/conc/examples/mailbox.flang дописана одна строка — обеспечивает «часы заводятся не больше раза» результат.«состояние».«заведено» не больше 1 — у обработчика шаг часов. Процесс «Часы» надзором не накрыт нарочно: в исходном файле у него нет ни одного достижимого отказа, и надзора он не требует.

Это ровно та форма улики, которой в conc/RESILIENCE.md:1019 закрыты пять прежних дыр замкнутости: программа, которая проходит все проверки с нулём диагностик и отказывает видом, которого в множестве нет.

Сторож на замкнутость есть и он настоящий — flang/test/failures.test.mjs:1148 гоняет все программы из flang/conc/examples по сетке семян и требует, чтобы каждый выданный код лежал в КОДЫ_ОТКАЗА. Он слеп здесь по той же причине, по которой был слеп сторож меры: ни в одной из десяти программ каталога нет ни одного обеспечивает у обработчика (проверено grep: 0 вхождений; четыре вхождения слова требует там есть, и все четыре — в комментариях). Дыра существует ровно потому, что корпус её не занимает.

Чем ограничено. Дыра — не довод против того, чтобы писать инвариант постусловием (process-invariant-is-a-handler-postcondition); она довод за то, что вместе с первой такой программой в корпус обязаны приехать две правки: FLANG_PROPERTY и FLANG_PRECONDITION восьмым и девятым видом в failures.mjs, и достижимость по тексту — «у обработчика процесса есть обеспечивает или требует», что решается по AST так же однозначно, как достижимость ящика. Цена оценена, не измерена: около 40 строк в failures.mjs плюс программа-улика в flang/conc/examples; прогонов, подтверждающих эту оценку, не делалось.

Второе ограничение: сказанное проверено только на свидетельском планировщике JavaScript. Как ведёт себя напечатанный код (Elixir, C) при нарушенном постусловии обработчика — не проверялось ни разу.

Связано: process-invariant-is-a-handler-postcondition, a-measured-zero-is-valuable, checks-that-stopped-comparing, a-hand-written-list-outlives-the-tree