Первый интерпретатор просто использует эти функции напрямую для рекурсивного аннотирования программы, не пытаясь вывести инварианты циклов (подставляя вместо них тривиально истинные формулы). Его корректность сводится к трем свойствам: (1) наислабейшее предусловие, полученное из вычисленного конечного состояния, действительно слабее предусловия, полученного из начального состояния, (2) все условия проверки, полученные из вычисленной аннотированной программы и конечного состояния, являются валидными и (3) вычисленная аннотированная программа идентична исходной программе после стирания аннотаций. Пример работы этого интерпретатора проиллюстрирован на домене битов четности со свободно добавленным верхним элементом (кодирующим отсутствие информации).

Второй интерпретатор более серьезно подходит к работе с циклами, используя информацию о том, что тест цикла всегда истинен внутри его тела и ложен на выходе. Незавершимость кодируется обертыванием конечного состояния в опциональный тип в выдаче интерпретатора. К параметрам добавляются две новые функции, которые вычисляют уточнения абстрактного состояния в зависимости от успешно и неуспешно пройденного теста цикла соответственно; именно эти функции берут на себя основную сложность задачи, в частности, они пытаются выводить информацию о незавершимости, и эта же информация позволяет пометить мертвый код тривиально ложными аннотациями. Схема процесса вывода инварианта цикла (в общем случае эта задача неразрешима!) выглядит так: (1) несколько абстрактных прогонов тела цикла (их количество контролируется эвристикой) с нарастающим расширением множества значений переменных - если процесс стабилизировался, инвариант найден; (2) если инвариант не найден, запускаем процесс 1 еще раз с переаппроксимацией для значений некоторых переменных - это позволяет ускорить процесс схождения (количество этих повторов также контролируется отдельной эвристикой); (3) если инвариант всё еще не найден, выбрать гарантированный инвариант (первый интерпретатор сразу же делает это, используя тривиальную истину); (4) сужение переаппроксимированных инвариантов повторным запуском интерпретатора (наличие этого шага приводит к определению интерпретатора через вложенную рекурсию).

Реализация этих шагов требует введения ряда вспомогательных функций-параметров, например, для сравнения количества информации в двух абстрактных значениях. Для доказательства корректности второго интерпретатора (состоящего из тех же трёх частей, что и в первом случае) также требуются 14 новых условий, описывающих все эти новые функции и их взаимодействие. Обе реализации интерпретаторов и их доказательства упакованы в модули, параметризующие их по абстрактному домену. Первый интерпретатор уже был ранее инстанцирован доменом чётности, а для второго описано кодирование домена числовых интервалов с потенциально бесконечными границами, где роль верхнего элемента играет интервал (-∞,+∞), а переаппроксимация заключается в замене одной из границ на -/+∞.

В заключение автор отмечает, что статью не следует рассматривать как полноценное введение в теорию АИ, а реализованные интерпретаторы являются моделями, т.к. оставляют желать лучшего в плане производительности - например, при вычислении аннотаций повторяется работа, уже проделанная ранее при поиске инварианта цикла. Кроме того, статический анализ может быть эффективнее, если рассматривать не отдельные переменные, а отношения между несколькими переменными.

#automatedreasoning