Про значение объявленной суммы в постусловии нельзя сказать ничего: ни сравнить, ни разобрать
В постусловии равен работает только на скалярах — число, строка, признак. Попытка сличить два значения объявленного типа отвергается дословно: «сравнивать на равенство можно только скаляры, а не «Звено»». Разобрать значение по вариантам там тоже нельзя: разбор внутри постусловия не разбирается — ни в строку, ни с переносом («у „разбор“ нет ни одного „случай“»).
Отсюда: о функции, отдающей объявленную сумму, запись, запись или параметр типа, сказать можно ровно столько, сколько скажут ДРУГИЕ функции, берущие такое значение на вход. Нет таких функций — сказать нельзя ничего.
Чем подтверждено. Ветка vypusk/utv-hashmap, основание github/main df055a6b. Два разных исхода на настоящем корпусе:
«Дата из дней»отдаёт«Календарный день»— и утверждение при ней есть, сильное:(«Дней от эпохи» от результат) равен дни. Круг замкнулся ПОТОМУ, что рядом лежит функция, берущая«Календарный день»и отдающая число;«Разобрать отметку»отдаёт«Итог даты»— и утверждения при ней нет вовсе. Ни одна функция модуля«Итог даты»на вход не принимает, значит ни «разобралось», ни «причина такая-то» не записываются. Круг «напечатать и разобрать» упирается в то же самое.
То же обходили и в hashmap.flang: «звено собирается обратно из ключа и значения» записать нельзя — собранное звено сличить не с чем; «дата верна» и «часы верны» записаны через ПЕЧАТЬ, потому что строка — скаляр.
Что из этого следует для языка. Дешёвая правка, закрывающая целый класс невыразимого: разрешить разбор в постусловии. Тогда при «Разобрать отметку» встанет ровно одно утверждение — что печать и разбор взаимно обратны на верных отметках, — и отпадут обходы через печать у «Дата верна» и «Часы верны».
Чем ограничено. Проверено на двоичном компиляторе (flang 0.5.1) двумя формами записи разбор в постусловии — однострочной и с переносом; обе отвергнуты разбором языка. Возможно ли это в записи, которую я не пробовал, — не знаю.
Поправка от 20 августа 2026. Заголовок этой заметки на нынешнем двоичном (bootstrap/flang, дерево 702a3602) НЕВЕРЕН. равен в постусловии берёт объявленные суммы, списки и параметры типа, а разбор в постусловии разбирается, если записать его с переносом и отступом — в одну строку он и правда отвергается теми словами, которые здесь приведены, и на этом строился прежний вывод. Отдельно: у суммы из ОДНОГО варианта поле читается точкой (звено.ключ), и этого хватает на все проекции. Разбор случая — в three-of-five-named-postcondition-walls-are-already-gone; там же названы 119 функций библиотеки, закрытых благодаря этому, включая «Разобрать отметку», о которой здесь сказано «утверждения нет вовсе».
Что осталось верным: сравнение сумм разрешено только внутри обеспечивает. В обычном теле функции то же выражение по-прежнему отвергается дословным «сравнивать на равенство можно только скаляры».
Связано: postcondition-runs-on-nested-calls-so-some-functions-cannot-be-stated-about, bottleneck-moved-to-claim-shape