Постусловие исполняется на каждом вызове, поэтому граф вызовов между постусловиями обязан быть без петель — и петля идёт через ТЕЛО тоже

обеспечивает — не только предмет доказательства. Оно печатается в код ($post в JavaScript, fl_post в C) и считается вычислителем при каждом вызове функции, в том числе при прогоне примеров. Отсюда два следствия, и второе неочевидно.

Хорошее следствие. Ложное постусловие КРАСНЕЕТ на примерах, а не молчит до доказательства. Значит утверждение можно проверять прогоном на враждебной сетке: пишешь функцию-пробу, которая зовёт проверяемую на сотне входов, и любое нарушение выпадает как FLANG_PROPERTY. Это дешевле и надёжнее чтения глазами.

Плохое следствие. Если постусловие функции А зовёт функцию Б, а Б (прямо или через своё тело) зовёт А, вычисление не кончится. Проверено:

тотальная функция «Раньше»
  принимает а: число, б: число
  возвращает признак
  обеспечивает «строгий порядок» результат равен ((не («Раньше» от б и а)) и притом (не (а равен б)))
  а меньше б

даёт FLANG_RECURSION_LIMIT: функция «Прогон» исчерпала лимит шагов (40000000) на глубине вызовов 1. Тотальность тут доказана, типы сошлись, и всё равно программа не работает.

Петля бывает через тело, а не только через постусловие. Это и есть та половина, о которой легко забыть. Постусловие «Ключ связи» (dictionary.flang) хотелось написать через «Ключи»: «ключ связи есть среди ключей словаря из одной связи». Постусловия у «Ключи» такого вызова нет — а ТЕЛО «Ключи» зовёт «Ключ связи» на каждой связи, и постусловие «Ключ связи» срабатывает снова. Бесконечность.

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

• «Есть ключ в дереве» не могла сказать про «Положить в дерево», потому что «Положить в дерево» говорит про неё. Сказано наоборот через «Найти в дереве»: «ключ есть ровно тогда, когда поиск отдаёт своё, а не запасное»;
• «Размер дерева» и «Ключи дерева» не могут говорить друг о друге — цепочка выстроена «Глубина дерева» → «Ключи дерева» → «Размер дерева» → «Приоритет».

Чем подтверждено. Ветка vypusk/utv-derevya на основании github/main df055a6b. Семь модулей flang/stdlib, 100 постусловий, прогон bootstrap/flang test на пробных файлах с враждебными сетками — ни одного исчерпания предела, то есть порядок сложился. Отдельный прогон на трёхстрочном примере выше показывает, что предел исчерпывается, когда порядка нет.

Чем ограничено. Речь только о постусловиях. Предусловие (требует) доказывает вызывающий, и в напечатанном коде оно занимает ноль байт — про него сказанное здесь неверно.

Цена, измеренная заодно. bootstrap/flang test flang/stdlib на 1216 примерах: 37,0 с до 100 постусловий, 39,9 с после. Плюс 7,8 %. Но цена не равномерна: постусловие «Найти в дереве», зовущее «Ключи дерева», делает поиск из O(log n) в O(n log n), и на большом дереве это будет видно.

Связано: tautologies-close-for-free, substantive-and-provable-claims-barely-overlap