Содержательное и доказуемое почти не пересекаются: 83 содержательных утверждения, 19 доказанных, общих девять

Замер на семи модулях flang/stdlib (tree, numbers, numtree, result, optional, sets, dictionary): 73 функции, было 30 постусловий, стало 100.

То есть больше половины доказанного — даровое, а больше девяти десятых содержательного ядро не берёт. Это не «пока не написали теорему»: теорему в flang/stdlib писать нельзя, там у ядра только автоматический путь.

Даровое утверждение узнаётся по ЗНАКУ сравнения

Прежних утверждений было 30, даровыми оказались 17 — и все 17 одной формы: «результат не длиннее входа».

(длина результат) не больше (длина элементы)     ← даром
результат не меньше 0                            ← даром
результат не больше 1                            ← даром
(длина результат) не меньше (длина множество)    ← НЕ даром

Причина одна: заглушка «пустой список» даёт длину 0, а 0 не больше чего угодно; заглушка 0 неотрицательна и не больше любого положительного литерала. А вот «не меньше длины входа» заглушка нарушает сразу.

Правило на будущее, стоящее одной строки: утверждение вида «результат не больше чего-то из входа» или «результат не меньше нуля» писать можно, но в счёт содержательного оно не идёт; его противоположность по знаку — идёт.

Разложение по файлам (даровых из прежних): tree 2 из 2, numbers 2 из 2, numtree 1 из 2, result 2 из 4, optional 0 из 4, sets 6 из 8, dictionary 4 из 8.

Где всё-таки пересеклось, и два хода, которыми это достигнуто

Девять содержательных доказанных: 4 в result.flang, 2 в optional.flang, 2 в dictionary.flang, 1 в numbers.flang. Два хода найдены прогоном:

1. Голый вызов целью не считается, а равен да — считается.

обеспечивает «…» «Есть значение» от результат                → сетка
обеспечивает «…» («Есть значение» от результат) равен да     → ДОКАЗАНО

У ядра есть вид цели «равно» и нет вида «вызов». Три знака переводят утверждение в доказанное. Граница: сработало на «Обернуть» (тело — конструктор). На рекурсивных «Есть ключ в дереве» и «Есть число» тот же приём не сработал — проверено обоими.

2. Цель, зеркалящая дерево условий ТЕЛА. Утверждение

(«Успешно» от результат) равен (((длина текст) равен 1) и притом ("0123456789" содержит текст))

ядро не берёт. То же самое, переписанное деревом условий тела —

если ((длина текст) не равен 1) то (не («Успешно» от результат))
  иначе (если ("0123456789" содержит текст) то («Успешно» от результат) иначе (не («Успешно» от результат)))

— доказывается правилом «разбор цели по условию». Граница измерена: из двенадцати проб на четырёх файлах перевело три, все три в result.flang. Не переводит, когда в ветви тела стоит арифметика или рекурсия; на «Безопасном делении» перебрано четыре формы — все четыре сетка, и почему, не выяснено.

Отрицательный результат про деревья

На tree.flang (13 функций, 18 утверждений) доказано ядром ноль. Разложение: единственный вид цели, который ядро на пользовательской сумме закрывает, — результат не меньше 0 (индукцией по «Дерево», база 1 случай, шаг на частях; проверено подстановкой такого постусловия в «Размер дерева»). А этот вид цели переживает заглушку 0 по определению. На деревьях множество доказуемого и множество содержательного не пересекаются вовсе.

Чем подтверждено. Ветка vypusk/utv-derevya на основании github/main df055a6b, замер bootstrap/flang check ФАЙЛ --proof по каждому из семи файлов. Содержательность проверена прогоном: у каждого утверждения посчитано его тело с заглушкой той же подписи на месте результат, и от него потребовано нет (у даровых — да).

Связано: tautologies-close-for-free, claims-about-length-are-two-thirds-of-what-the-kernel-refuses, postconditions-run-so-their-call-graph-must-be-loop-free, the-type-holds-no-invariant-so-obvious-claims-about-a-search-tree-are-false

Замер 20 августа по ВСЕЙ библиотеке: две трети доказанного содержательны

Заголовок этой заметки описывает состояние семи модулей до того, как ядро научилось пяти видам цели и трём ходам, а библиотека — писать утверждения под них. Счёт по всем двадцати модулям flang/stdlib (node benchmarks/proof-cost/count-library.mjs, подмена тела заглушкой той же подписи) даёт другую картину:

То есть доказанное на две трети содержательно, и это перестало быть новостью про даровые формы. Не изменилось другое: доказанное — малая доля высказанного (87 из 475), и распределено оно крайне неровно. higher-order — 15 из 40, lists — 10 из 38, а http (0 из 25), json (0 из 12) и postgres (0 содержательных из 65) стоят на нуле, потому что считают по знакам строки, а строке начальная алгебра не дана: FLANG_PROOF_INDUCTION_TYPE — у этого типа (строка) принципа индукции нет.