Четыре вещи, которых в обеспечивает написать нельзя, и одна из них ВЕШАЕТ проверку вместо отказа
Померено при написании 69 утверждений о трёх строковых модулях. Все четыре границы нашлись прогоном, три из них дают понятный отказ, а первая — нет.
1. Постусловие не может звать свою же функцию — проверка ВИСНЕТ. Проверка постусловия идёт и на вложенном вызове, поэтому «обратить обратно — исходное» у «Обратить строку» раскручивается бесконечно:
обеспечивает «двойной переворот» («Обратить строку» от результат) равен текстflang check на таком файле не падает и не отказывает — он ВИСИТ, и снимать его приходится по времени. То же у пары взаимно ссылающихся постусловий: если постусловие А зовёт функцию Б, а постусловие Б зовёт функцию А, виснет так же. Следствие для работы: круговые утверждения приходится писать в ОДНУ сторону, а у второй функции говорить что-то другое. Проверять надо и транзитивно: у «Это цифра» нельзя звать «Цифра числом», потому что ТЕЛО «Цифра числом» зовёт «Это цифра».
2. Списки нельзя сравнивать на равенство. «список А» равен «список Б» отвергает слой типов: «сравнивать на равенство можно только скаляры, а не список строки». Значит круговой ход про список («отрезал голову, приписал обратно — тот же список») прямо не выразить. Обход — скалярные проекции списка: длина, элемент N в, содержит и склейка соединить … по …. Склейка делает основную работу: у двух списков строк одинаковая склейка без разделителя означает «те же строки в том же порядке», если ни одна не пуста.
3. Перебрать список внутри обеспечивает нечем. (ПОПРАВКА 20 августа, ветка u/kvantor: неверно про СВЁРТКУ и неверно про соседние пары. Свёртка в постусловии разрешена — проверено прогоном, модуль с постусловием-свёрткой проходит flang check и flang test без замечаний; писать её руками никто не станет (68 токенов на утверждение), но выразимости она не запрещает. Квантор по парам соседей теперь есть записью — СПИСОК не убывает, см. a-quantifier-over-adjacent-pairs-cost-two-files-not-twenty-nine. Про квантор СУЩЕСТВОВАНИЯ пункт остаётся верным.) Ни свёртки, ни «для каждого» там нет, а рекурсивная функция-помощник упирается в границу 1. Поэтому квантор («найдётся часть, у которой следующий знак другой» — настоящая максимальность общего начала; «каждый байт годен») не пишется. Обход, который сработал: сказать точно на списках длины 0, 1 и 2, а на произвольном — только неравенство.
4. нат минус нат даёт целое, и в нат его уже не отдать. длина годится там, где ждут нат, а (длина текст) минус (длина суффикс) — нет: «ожидался нат, получен целое». Обход — писать подстрока напрямую с охраной, а не звать функцию, требующую нат.
Что при этом МОЖНО и оказалось неожиданно полезным:
если … то … иначевобеспечиваетразрешено;илиии притомСОКРАЩАЮТ вычисление — правая сторона не считается, если левая всё решила. Значит охрана вида((длина знак) равен 0) или (…)безопасна, и опасные формы (разделить … по "",подстрокавне диапазона — обе даютFLANG_BUILTIN_ARGS) за ней не сработают;- поля варианта читаются точкой прямо в утверждении:
ход.осталось,результат.точки. На этом стоят все утверждения о разборе UTF-8, и они вышли точными («знак замены добавляется ровно тогда, когда хвост оборван»), а не «длина не растёт».
Чем подтверждено. Ветка vypusk/utv-strings, основание df055a6b. Зацикливание — прогон flang check на пробном модуле из одной функции, снят по времени на 20 секундах. Остальные три — отказы компилятора, текст приведён дословно.
Поправка от 20 августа 2026. Пункт 2 («списки нельзя сравнивать на равенство») на двоичном дерева 702a3602 не воспроизводится: в постусловии результат равен пустой список и результат равен [(элемент 1 в элементы) умножить на 2] проходят типизацию и проверяются при работе. В обычном теле запрет остался. Пункт 3 тоже смягчился: перебрать список нечем, но отфильтровать … где в постусловии работает, и счёт через (длина (отфильтровать … где …)) даёт квантор существования. Пункты 1 (свою функцию звать нельзя, виснет) и 4 (нат минус нат даёт целое) проверены заново и держатся. Подробности — three-of-five-named-postcondition-walls-are-already-gone.
Вторая поправка, 21 августа 2026. Совет «дорогие вызовы внутри утверждения выносите в пусть» (он стоит в postcondition-runs-on-nested-calls-so-some-functions-cannot-be-stated-about) на этом двоичном НЕ РАБОТАЕТ: пусть в обеспечивает не разбирается ни с переносом («не разобрана конструкция: неожиданное»), ни в одну строку — в однострочной записи следующее за значением слово съедается как часть значения, а если поставить скобки, встроенные формы внутри перестают связываться («имя «длина» не связано»). Пробовано тремя записями. Значит вынести повторный вызов некуда, и единственный способ не считать дважды — не называть его дважды.
Связано: what-the-kernel-proves-is-almost-exactly-what-is-gratis, dve-mery-stroki-delyat-vstroennye-formy
Поправка 20 августа 2026: из четырёх границ осталась одна
Перемерено на bootstrap/flang 0.5.1, ветка u/steny-peremer, основание ff8ad5d0. Пробы — по одному файлу на границу, вердикт брался из bootstrap/flang check … --proof.
Пункт 1 («постусловие не может звать свою же функцию — проверка ВИСНЕТ») — неверен. Контракт больше не проверяется, пока считается контракт. Проба: обеспечивает «переворот переворота — исходное» («Обратить» от результат) равен элементы на структурно-рекурсивной «Обратить» — check отвечает за 0,1 с, примеры проходят, вердикт «сетка»; запуск даёт правильный ответ. Пара взаимных постусловий («Меньшее» говорит о «Большее», «Большее» — о «Меньшее») не только не виснет, но и ДОКАЗЫВАЕТСЯ обе стороны правилом «разбор цели по условию». Разбор — the-postcondition-loop-is-untied-by-a-program-transform-not-a-runtime-flag.
Пункт 2 («списки нельзя сравнивать на равенство») — неверен в позиции утверждения. результат равен элементы над список числа проходит типы и закрывается ядром. В ТЕЛЕ запрет остался. Разбор — equality-on-a-type-parameter-is-banned-only-in-bodies.
Пункт 3 («перебрать список внутри обеспечивает нечем») — неверен, и упал он вместе с пунктом 1. Помощник в утверждении теперь не зацикливает проверку, поэтому квантор пишется парой функций и отбором. Проба, прошедшая целиком:
обеспечивает «каждый не больше следующего»
пусто (отфильтровать («Разности соседей» от результат и («Отбросить первый» от результат))
где р → 0 больше р)Утверждение работает СТОРОЖЕМ: на теле, отдающем неотсортированный список, check краснеет FLANG_PROPERTY: нарушено свойство «каждый не больше следующего». Ядро его не доказывает — вердикт «сетка», — но «написать нечем» и «доказать нечем» это разные беды, и раньше они были записаны как одна.
Пункт 4 («нат минус нат даёт целое») — держится. Проба: «Взять сколько» от ((длина текст) минус (длина суффикс)) при принимает н: нат → FLANG_TYPE: аргумент «н» функции «Взять сколько»: ожидался нат, получен целое. Встроенные формы при этом разность принимают: подстрока текст с ((длина текст) минус сколько плюс 1) по (длина текст) проходит.