Постусловие считается при КАЖДОМ вызове и печатается в код, поэтому обход внутри него меняет порядок цены функции

Постусловие в flang — не проверка при разработке. Оно печатается в сгенерированный код («Тело с постусловиями», flang/self/emit-c.flang) и считается после каждого вызова, в том числе у постусловий, доказанных ядром: отсева по вердикту в печати нет вовсе. Из этого следуют три вещи, и все три кусаются.

1. Обход внутри постусловия рекурсивной функции даёт квадрат вместо линии

Замер на промежутке из 200 чисел (сортировка обратного промежутка, двоичный поиск, поиск индекса, сжатие двух промежутков), одно и то же дерево, разница только в тексте постусловий:

Шестикратное подорожание дали три утверждения: «результат содержит значение» у рекурсивной «Вставить по порядку» (обход на каждом витке, а «Сортировать» зовёт её n раз), «Отбросить первые», звавшее «Взять первые», и «Двоичный поиск», звавший обход «Элемент» — тем самым убивая логарифм, ради которого середина берётся встроенной формой.

Лечится без потери смысла: то же самое почти всегда говорится за постоянное время, а иногда СИЛЬНЕЕ. «Во главе результата встало меньшее из вставляемого и прежней головы» и содержательнее «вставленное стоит в списке» (говорит о месте, а не только о наличии), и дешевле — читает голову встроенной формой.

Правило. Постусловие на РЕКУРСИВНОЙ функции обязано считаться за постоянное время: длина, элемент N в список, сравнение. Вызов, обходящий список, внутри такого постусловия — ошибка проектирования, а не вкусовщина.

2. Постусловие, зовущее свою же функцию, зацикливается насмерть

обеспечивает «список равен сам себе» («Списки равны» от первый и первый) равен да уходит в бесконечную рекурсию: проверка постусловия зовёт функцию, та проверяет своё постусловие, и так далее. Прогон падает с исчерпанием лимита шагов (40 000 000).

То же у ВЗАИМНЫХ ссылок, и они не бросаются в глаза: «Меньшее», говорящее о «Большее», плюс «Большее», говорящее о «Меньшее». Так же зацепились «По возрастанию» ↔ «По убыванию» и «Составить» ↔ «Отобразить составом».

Правило. Ссылку между двумя функциями в постусловиях оставлять только в одну сторону.

3. То же самое ломает и проверку доказательств, а не только прогон

Пара «Отбросить первые» и «Взять первые», сославшись друг на друга в постусловиях, съела тот же лимит шагов на этапе flang check — до всякого прогона примеров. Сообщение при этом называет функцию САМОГО КОМПИЛЯТОРА («Найти в обстановке исчерпала лимит шагов»), а не место в проверяемом файле, поэтому по тексту ошибки причина не читается — искать надо подменой утверждений по одному.

Чем подтверждено. Ветка vypusk/utv-lists на основании df055a6b, коммит «Утверждения удешевлены». Замер времени — /usr/bin/time на одном и том же двоичном, файлы отличаются только постусловиями; по три прогона, разброс меньше 5 %.

Чем ограничено. Числа сняты интерпретатором (flang test). В напечатанном C доля проверок может отличаться, но порядок цены — тот же: проверка стоит там же, где стоит вызов.

Связано: tautologies-close-for-free, left-fold-is-blocked-because-the-fold-rule-does-not-read-the-callee-postcondition

Что из этого починено 20 августа

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

Первый абзац заметки — «печатается в код и считается после каждого вызова, В ТОМ ЧИСЛЕ у постусловий, доказанных ядром: отсева по вердикту в печати нет вовсе» — БОЛЬШЕ НЕ ВЕРЕН. Отсев есть, и условий у него два: вердикт «доказано» и наличие примеров у функции. Разбор — a-proved-postcondition-no-longer-reaches-printed-code.

Пункт 2 («постусловие, зовущее свою же функцию, зацикливается насмерть») закрыт: контракт больше не проверяется, пока считается контракт. Правило «ссылку между двумя функциями в постусловиях оставлять только в одну сторону» отменяется — пара «Меньшее»↔«Большее» проверяется. Разбор — the-postcondition-loop-is-untied-by-a-program-transform-not-a-runtime-flag.

Пункт 3 («то же ломает и проверку доказательств») на пробе не воспроизвёлся: flang check зацикливался на ПРОГОНЕ ПРИМЕРОВ, а ядро успевало ответить. Мерено на «Переворот» и на паре «Меньшее»↔«Большее»; на паре «Отбросить первые»↔«Взять первые» проба не повторялась.