Три из пяти названных стен постусловия на нынешнем двоичном уже сняты: сумма сравнивается, разбор разбирается, поле варианта читается точкой
Заметки a-declared-sum-cannot-be-spoken-about-in-a-postcondition и chto-nelzya-napisat-v-obespechivaet называли границы, из-за которых целые классы функций считались немыми. На двоичном из bootstrap/ (дерево 702a3602) три из них не воспроизводятся:
| что считалось невозможным | что на самом деле |
|---|---|
равен берёт только скаляры | берёт объявленные суммы, списки и параметры типа: результат равен (вариант «Не число»), результат равен пустой список, опция равен (вариант «Нет») — всё проходит типизацию и проверяется при работе |
разбор в постусловии не разбирается | разбирается, если записать с переносом и отступом. В одну строку по-прежнему отвергается словами «у „разбор“ нет ни одного „случай“» — отсюда и старый вывод |
| про поле варианта сказать нечего | читается точкой: звено.ключ, результат.расписание.с15. Условие одно: у типа ровно один вариант, иначе отказ «доступ к полю требует записи или суммы из одного варианта, а у «Дерево» вариантов 2» |
Ловушка, из-за которой это не заметили раньше. Сравнение сумм разрешено только внутри обеспечивает. В обычном теле функции то же выражение отвергается дословным «сравнивать на равенство можно только скаляры, а не «Разбор тела»». Проба, написанная в теле, даёт старый отказ и подтверждает старую заметку — а в постусловии работает.
Что это открыло на настоящем корпусе. 119 функций flang/stdlib/ не имели ни одного утверждения. Закрыты все 119, 169 новыми строками обеспечивает. Пять из них считались немыми «в принципе» и названы такими в комментариях самой библиотеки — «Приоритет» (tree), «Успешно» (result), «Ключ звена» и «Значение звена», «Искать признак» и «Звенья словаря» (hashmap), «Разобрать отметку» (datetime). Каждая заговорила одним из трёх приёмов выше.
Чего снять НЕ удалось, проверено заново:
- постусловие, зовущее свою функцию, по-прежнему виснет, а не отказывает. Поэтому у пары «через кого выражено всё» (
«Звенья словаря»,«Искать признак») утверждение написаноразбором, не зовущим никого; - квантора по списку нет, но
отфильтровать … гдев постусловии работает и даёт счёт:(длина (отфильтровать заголовки где з → …)) больше 0.
Чем подтверждено. Ветка u/golye над github/main 702a3602, двоичный собран make -C bootstrap -j8. Каждый приём проверен пробным модулем на пять строк и подменой тела заглушкой: заглушка роняет утверждение (FLANG_PROPERTY), значит оно про эту функцию, а не про подпись.
Чем ограничено. Мерено на одном двоичном. Реализация на JavaScript в дереве отсутствует, поэтому «раньше было нельзя, теперь можно» — про сегодняшний bootstrap/flang, а не про историю правок ядра.
Связано: a-declared-sum-cannot-be-spoken-about-in-a-postcondition, chto-nelzya-napisat-v-obespechivaet, postcondition-runs-on-nested-calls-so-some-functions-cannot-be-stated-about, darovoe-utverzhdenie-uznayotsya-podmenoy-tela-zaglushkoy