Даровое утверждение узнаётся подменой тела заглушкой, и в двух модулях библиотеки таких оказалось 17 из 32
tautologies-close-for-free назвала классы утверждений — полное, частичное, тавтология — но различать их предлагала руками. Есть механическая проверка, и она ловит не только тавтологию.
Подмените тело функции заглушкой той же подписи — пустым списком, нулём, нет. Если утверждение при этом осталось истинным, оно верно про ЛЮБУЮ функцию такой подписи и о проверяемой не говорит ничего. Такое утверждение даровое, и доказанность его ничего не стоит.
Проверка ловит оба вырождения сразу: тавтологию (постусловие есть само тело) и ослабление (утверждение слабее смысла функции).
Замер. В flang/stdlib/lists.flang и flang/stdlib/higher-order.flang было 32 утверждения на 62 функции. Даровых — 17 из 32, и все одного покроя:
| форма | сколько | почему даровая |
|---|---|---|
(длина результат) не больше (длина <входа>) | 10 | заглушка «пустой список» даёт длину 0, а 0 не больше любой длины |
результат не меньше 0 | 7 | заглушка 0 неотрицательна |
Поимённо даровыми оказались: «Длина», «Отбросить первые», «Взять первые», «Срез», «Индекс», «Двоичный поиск», «Уникальные», «Считать вхождения» (оба), «Без значения», «Сжать в пары», «Сжать суммами», «Отфильтровать», «Считать где» (оба), «Позиция где», «Сжать».
Тут и объясняется, почему ведомость выглядела хорошо. Из 19 доказанных ядром утверждений этих двух файлов даровыми были 10 — то есть ядро закрывало ровно то, что закрыть легче всего, и число «доказано» росло от этого, а знание о библиотеке нет. Содержательных И доказанных было 9, стало 14. Общее «доказано» при этом упало с 19 до 14, а число утверждений выросло с 32 до 73. Падение «доказано» здесь признак работы, а не регресса, и отчитываться одним этим числом нельзя.
Что ставить взамен. Работают четыре приёма, все проверены на этих файлах:
- равенство вместо границы: не «удаление не удлиняет», а «удалено ровно столько, сколько было вхождений»;
- сверка двух реализаций одного смысла: «счёт подходящих равен длине отобранного», «встроенная форма и обход по индексу согласны»;
- условие вместо оговорки в прозе: «если значение в списке, то на найденном месте оно и стоит, иначе ответ ноль»;
- место, а не наличие: «первый элемент остаётся первым» вместо «первый элемент есть в результате» — сильнее и дешевле (a-postcondition-runs-on-every-call-so-a-walk-inside-it-changes-the-cost-order).
Чем подтверждено. Ветка vypusk/utv-lists на основании df055a6b, восемь коммитов. Ведомость flang check --proof до и после; каждое новое утверждение прогнано на враждебных входах (пустой список, один элемент, список из одинаковых, не число, минус ноль, дробный и отрицательный номер) двенадцатью погонщиками — нарушений ноль.
Чем ограничено. Проверка ручная: языку нечем подменить тело заглушкой автоматически. Сделать её автоматической стоило бы: это ровно та проверка, которая отличает рост числа доказанного от роста знания о библиотеке.
Связано: tautologies-close-for-free, claims-about-length-are-two-thirds-of-what-the-kernel-refuses, a-postcondition-runs-on-every-call-so-a-walk-inside-it-changes-the-cost-order