Классический «трюк» - развернуть петли в пределах границ.Эта идея возникла в сообществе аппаратного обеспечения, где ограниченные доказательства встречаются гораздо чаще.Но это также относится и к программному обеспечению.CBMC (https://www.cprover.org/cbmc/) - это система, которая делает это для программ на языке C. Очевидно, что это предоставит «доказательство» только в тех случаях, когда достаточно номера развёртывания.
Обратите внимание, что развёртывание может быть непрактичным, так какэто может привести к взрыву кода, в таких случаях вы можете использовать трюк "uninterpreted-function": то есть вы развернете фиксированное число раз, а затем абстрагируетесь до конца вычисления. Это может привести к ложноположительным результатам,т. е. решатель может возвращать фиктивную модель, но эту идею можно использовать в системе, основанной на CEGAR (counter-example-guided-abstraction-уточнение).
В общем случае циклы подразумевают инварианты и доказательства для программс использованием циклов (или рекурсии) требуется выяснить, что это за инварианты, и доказать их с помощью индукции. Решатели SMT не делают индуктивных доказательств. Для таких задач лучше использовать подлинный инструмент для доказательства теорем (Изабель, HOL, HOL-Light, Coq, Agda, Lean; выбирайте сами) Обратите внимание, что большинство этих систем в наши дни могут использовать SMT-решатель в качестве «оракула» для ускорения.Доказательства для подцелей, так что в этом смысле вы получаете лучшее из обоих миров.В частности, Lean происходит из линии z3 и определенно стоит проверить: https://leanprover.github.io/