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

Журнал упреждающей записи

docs/examples/wal/ — две программы на flang: разбор, печать и восстановление журнала упреждающей записи (write-ahead log) после обрыва, и план, который дописывает в журнал одну запись через поручения ввода-вывода. Обе целиком на flang; на диск ничего не пишут — пишет хозяин, исполняющий поручения плана.

Что лежит в каталоге

Файлов .flang два: | файл | что это | строк | |---|---|---:| | docs/examples/wal/write-ahead-log.flang | модуль «Write ahead log»: формат записи, разбор журнала по одному знаку, печать, восстановление до последней целой записи, следующий номер | 579 | | docs/examples/wal/append-plan.flang | модуль «Append plan»: план «Дописать в журнал» — прочитать файл, дописать запись, подтвердить номером. Использует первый модуль | 95 |

Примеров в обоих файлах вместе 110 ; они объявлены внутри функций и прогоняются командой bootstrap/flang test.

Формат записи

#<номер>:<длина>:<тело>;

Запись печатает функция «Напечатать запись». Журнал читает по одному знаку функция «Шаг чтения» — автомат с состояниями «Между записями», «Читаем номер», «Читаем длину», «Читаем тело», «Ждём метку конца» и «Сбились». Из состояния «Сбились» выхода нет: всё, что идёт после первой порчи рамки, отбрасывается; записи, прочитанные до неё, остаются.

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

Как запустить

bootstrap/flang check docs/examples/wal/write-ahead-log.flang --proof
bootstrap/flang check docs/examples/wal/append-plan.flang --proof
bootstrap/flang test  docs/examples/wal/write-ahead-log.flang
bootstrap/flang test  docs/examples/wal/append-plan.flang

check печатает первой строкой число функций и число функций с доказанным завершением; --proof добавляет отчёт по каждому утверждению; test печатает число примеров и сколько из них прошло.

План исполняется командой bootstrap/flang io. Путь к файлу журнал.wal план берёт относительно каталога, в котором лежит программа, и файл обязан существовать: на отсутствующий файл план отвечает «Провал» с кодом FLANG_IO_READ (код возврата 1). Чтобы не писать в дерево, скопируйте оба файла в отдельный каталог:

mkdir -p /tmp/wal && cp docs/examples/wal/*.flang /tmp/wal/ && : > /tmp/wal/журнал.wal
bootstrap/flang io /tmp/wal/append-plan.flang

Каждый запуск печатает в JSON два поручения — «Прочитать файл» и «Записать файл» — с откликами хозяина и дописывает в файл одну запись с телом «выдача товара» и следующим номером. Запись с испорченной рамкой в конце файла (например, без метки конца) при следующем запуске отбрасывается: файл переписывается целыми записями плюс новая.

Что проверено и что доказано

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

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

«Сетка» означает: утверждение проверено на примерах функции, доказательства обо всех входах у него нет — отчёт говорит это прямо. Ядро не берёт эти четыре утверждения потому, что они связывают результат свёртки по всей строке входа с самой строкой (печать равна началу входа); правила такого вида у ядра нет. Что ядро берёт, а что нет, названо на странице какие обещания ядро берёт.

Кроме этих четырёх на сетке стоят ещё три мелких: «цифра не больше девяти» («Цифра числом»), «печать не короче шести знаков» («Напечатать запись») и «разрез не теряет и не добавляет ни знака» («Разрез сходится») — прогон check --proof 11 сентября 2026 на коммите 2c40752d0: утверждений 17, доказано 10, сетка 7.

Что ядро доказало обо всех входах:

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

Подтверждение записи в плане: вариант «Конец работы» строится в модуле «Append plan» в одном месте — в ветви «Записано» функции «После записи журнала». Любой другой отклик хозяина даёт «Провал»: «Сбой» — со своим кодом, прочее — с кодом FLANG_IO_ORDER. Это видно чтением модуля и его примерами.

Чего программа не гарантирует

Рядом