Кратко: в формальной верификации программ предикатная логика служит для формального задания спецификаций (пред- и постусловий, инвариантов), моделирования семантики команд и порождения условий проверки (verification conditions, VC). Автоматические доказатели (SMT/ATP) пытаются доказать эти условий; успешное доказательство означает корректность программы относительно спецификации.
Примеры (исчисление предикатов / Hoare‑логика):
- Присваивание. Hoare‑тройка $\{P\}x:=x+1\{Q\}$. Проверочное условие сводится к подстановке:
$$P(x)\to Q(x+1).$$ Доказатель проверяет формулу в предикатной/теоретической логике (обычно арифметика целых/реальных чисел).
- Последовательность и условие. Для $C_1;C_2$ набираются VC для каждого фрагмента; для условного оператора $\text{if}B\text{then}{C}_t\text{else}{C}_e$ требуется показать оба пути:
$$P\wedge B\to {\text{post}}_{C_t},P\wedge \neg B\to {\text{post}}_{C_e}.$$
- Цикл и инвариант. Для цикла $\text{while}B\text{do}C$ нужно предложить инвариант $I$ и проверить:
$$P\to I,I\wedge B\to \text{wp}(C,I),I\wedge \neg B\to Q,$$ где $\text{wp}(C,I)$ — слабое предусловие команды $C$ относительно $I$. Чаще всего доказывается индуктивно.
Как код переводят в формулы: состояние программы представляют суммой переменных; переходы — отношениями $T(s,s^{\prime })$ (в логике вводят «праймованные» переменные для постсостояния). VC — это замкнутая формула в первом‑порядковой логике с теориями (арифметика, массивы, структуры и т. п.).
Ограничения и типичные проблемы автоматических доказателей:
- Теоретические ограничения:
- Первопорядковая логика с арифметикой и комбинированными теориями в общем случае неразрешима; для многих фрагментов нет гарантии автоматического завершения.
- Необходимость индукции: свойства циклов/рекурсии часто требуют индуктивных рассуждений, которые автоматически не выводятся.
- Практические проблемы:
- Кванторы и их инстанциация: SMT‑солверы используют эвристики (триггеры). Неправильные триггеры приводят к неэффективности или промахам; перебор инстанций может не завершиться.
- Нелинейная арифметика и целочисленное умножение: сложны для автоматов, часто требуют ручных лемм или редукции.
- Плавающая точка и битовые векторы: точная модель часто приводит к сложным задачам; солверы частично поддерживают эти теории, но дорого.
- Массивы, указатели и куча: аппроксимации или аксиоматизации приводят к ложным контрпримером или к трудным к доказанию формулам; нужна специальная логика (например, separation logic).
- Конкурентность: множество интерлеивингов приводит к экспоненциальному взрыву состояний; нужны инварианты/рещимы для взаимодействия (rely/guarantee, абстракции).
- Комбинаторная сложность и масштабируемость: большие верификационные условия приводят к перебору, таймаутам, памяти.
- Неправильные или неполные аксиоматизации: ручные аксиомы могут сделать систему несогласованной (опасно) или недоказательной.
- Абстракции и ложные контрпримеры: CEGAR‑подходы дают спурриозные контрприменты, требующие уточнения абстракции.
- Характерные поведения автоматов:
- SMT эффективны для кванторно‑свободных задач в решаемых теориях (QF_...), но с кванторами и сложными теориями часто нужна помощь пользователя.
- ATP (Vampire, E prover) сильны в чистой FOL, но при теоретических аксиоматиках и арифметике хуже.
- Комбинация автоматического и интерактивного доказательства (Isabelle, Coq) — частая практика: автоматизируются простые шаги, а человек даёт индукции/леммы.
Практические рекомендации:
- Формулируйте спецификации так, чтобы попадать в решаемые фрагменты (квантор‑минимизация, линейная арифметика).
- Подбирайте инварианты и леммы заранее; используйте шаблоны индукции.
- Пробуйте разные солверы/параметры и давайте «помогающие» леммы или тактики.
- Для указателей/кучи применяйте специализированные логики (separation logic) или сериализацию модели в SMT‑удобные представления.
Вывод: предикатная логика — основа формальной верификации: спецификации, семантика и VC выражаются в ней. Автоматические доказатели сильно помогают, но сталкиваются с недетерминированностью инстанциации кванторов, нуждой в индукции, сложными теориями и масштабируемостью; потому верификация обычно сочетает автоматику с ручной помощью и подходящими абстракциями.