Статья предполагает, что читатель имеет опыт работы с интерактивным программным средством доказательства теорем — Coq.
Статья является адаптированной русскоязычной версией моей статьи, написанной во время работы над формальной верификацией протокола криптовалюты Tezos.
В данной статье мы рассмотрим прием, который используется для работы с рекурсивными функциями, которые не проходят проверку завершаемости (тотальности) в Coq. Под «горючим» мы будем понимать натуральное число, которое вводится как дополнительный параметр в тело функции, чтобы обозначить верхнюю границу числа итераций, которые функция может совершить. Таким образом функция трансформируется в завершаемую, удобную для работы, и радушно принимаемую компилятором Coq. В литературе термин встречается под названиями: petrol, fuel, gas и т.д.
Положим, перед нами стоит задача: необходимо верифицировать функцию, написанную на каком-либо языке программирования. Мы разбираемся в том, что делает эта функция, уже прикидываем, какие леммы сформулируем, чтобы доказать, что она ведет себя именно так как ожидается. Переводим функцию на Coq (вручную, или с помощью автоматических переводчиков, если только таковые имеются для требуемого языка), и видим, что проверка Coq на завершаемость нашей функции (termination check) провалилась.
Это значит Coq не может определить какой аргумент на каждом шаге итерации будет уменьшаться. Можно попробовать явно указать Coq на аргумент, который, мы точно знаем будет уменьшаться на каждом шаге {struct уменьшаемый_аргумент}: