> -- Rifat писал(а):
> И если кто-то знает где можно почитать не про инвариант цикла, а про другие инварианты, то был бы благодарен за ссылку.
Единой теории не укажу (да и вряд ли такова существует). Ниже эмпирические наблюдения (впрочем, в сопутствующих материалах полно теоретических изложений разного толка).
> -- Rifat писал(а):
> Например, зачем нужен инвариант рекурсии, когда у рекурсивной функции может быть предусловие и постусловие? (В принципе для рекурсии была бы полезна ограничивающая функция, которая бы показывала, что рекурсия завершается, а не "зацикливается" и не вылетает при исчерпании стека.)
Ограничение рекурсии (цикла) необходимая вещь. В качестве примера -- современный "мейнстрим" в области верификации  --
проект Dafny:
https://www.microsoft.com/en-us/researc ... rrectness/

проект F-Star:
https://fstar-lang.org/

где имеется директива "decreases" (в мощной системе вывода типа как в F-Star условие рекурсии в ряде случаев определяется автоматом, также как и остальные ограничения типа).

Можно обратить внимание, что в Dafny нет инварианта для класса, и используются контракты состояния объекта (косвенно через функции/методы) для каждого необходимого метода класса (как универсальный способ, поскольку состояние объекта изменяется). В F-Star имеются ограничения для типов данных (в общем-то, здесь явно декларируются "зависимые типы"), но нет инвариантов для операторов цикла (да и не нужны они). Техники F-Star мощнее, и требуется явное именование объектов для контракта (собственно, там именно ограничения типов). К примеру, "леммы" там указывают на качество конкретных объектов.

У F-Star имеются неплохие расширения, как "реляционные контракты":
https://www.microsoft.com/en-us/researc ... 02/rrf.pdf

где в дополнение к "классическим" пред/постусловиям используется отношение между результатами двух вычислений выражения. Это техника в т.ч. и для анализа условно "неограниченной" рекурсии.

Следует отметить, что контракты операций могут выражать не только пред/постусловия как таковые (т.е. инвариант "прикладного", "предметного" состояния), но и качественные свойства. В том же F-Star таковым активно занимаются, или вот примеры "аксиом" здесь (что есть в т.ч. и подсказки для компилятора для правильных или эффективных реализаций/оптимизаций):
http://felix-lang.org/share/src/web/tut ... sm_03.fdoc