1. Пределы тестирования и стена неразрешимости: почему 1 000 000 успешных тестов ничего не доказывают

1.1 Бессмертный афоризм Дейкстры и комбинаторный взрыв пространства входов

В 1969 году на конференции НАТО по программной инженерии лауреат премии Тьюринга Эдсгер В. Дейкстра (Edsger W. Dijkstra) сформулировал самый известный тезис в истории информатики:

“Program testing can be used to show the presence of bugs, but never to show their absence!" (Тестирование программ может использоваться для демонстрации наличия ошибок, но никогда — для демонстрации их отсутствия!)

Рассмотрим простейшую чистую функцию f(x, y), принимающую два 64-битных знаковых целых числа (int64_t). Общее число возможных входных пар составляет:

Даже если суперкомпьютер будет выполнять один миллиард ($10^9$) тестов в секунду, полный перебор всех входов займёт около $1{,}08 \times 10^{22}$ лет — в 780 миллиардов раз больше возраста Вселенной! С учётом динамической памяти, сетевых пакетов и недетерминированного переключения потоков (interleaving) число путей выполнения уходит в бесконечность ($\infty$).

В 2006 году Джошуа Блох (Joshua Bloch) из Google обнаружил ошибку, которая скрывалась 9 лет в стандартной библиотеке Java (java.util.Arrays.binarySearch) — знаменитый баг целочисленного переполнения в бинарном поиске:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12

public static int binarySearch(int[] a, int key) {
    int low = 0;
    int high = a.length - 1;
    while (low <= high) {
        int mid = (low + high) / 2; // ★ ФАТАЛЬНЫЙ БАГ: отрицательное переполнение при low + high >= 2^31!
        int midVal = a[mid];
        if (midVal < key) low = mid + 1;
        else if (midVal > key) high = mid - 1;
        else return mid;
    }
    return -(low + 1);
}

Когда сумма low + high превышает максимум 32-битного знакового целого ($2^{31} - 1 = 2\,147\,483\,647$), в дополнительном коде происходит переполнение в отрицательную область, вызывая ArrayIndexOutOfBoundsException.

1.2 Проблема остановки Тьюринга (1936) и теорема Райса (1953)

Почему бы не написать универсальный анализатор, который по исходному коду любой программы $P$ со 100%-ной точностью определит, есть ли в ней ошибки? Этому препятствуют проблема остановки Алана Тьюринга (1936) и теорема Райса (1953):

Ни один инструмент не может одновременно обеспечить (1) полную автоматизацию, (2) корректность / надёжность (Soundness: ноль ложноотрицательных срабатываний) и (3) полноту (Completeness: ноль ложноположительных тревог).

1.3 Как формальная верификация обходит теорему Райса: надёжная аппроксимация сверху

Формальная верификация никогда не жертвует надёжностью (Soundness): если верификатор выдаёт вердикт "SAFE", программа математически на 100% свободна от ошибок на всех $\infty$ путях выполнения. Для этого вычисляется надёжная аппроксимация сверху (Sound Over-Approximation) $\mathcal{R}_{\text{approx}} \supseteq \mathcal{R}_{\text{exact}}$ всех достижимых состояний и доказывается пустота её пересечения с множеством аварийных состояний $\mathcal{B}$:

  flowchart TD
    A["Точное множество достижимых состояний R_exact программы P (Неразрешимо по Райсу)"] --> B["4 Столпа Формальной Верификации"]
    B --> C["Столп 1: Дедуктивная верификация (Логика Хоара и SMT)"]
    B --> D["Столп 2: Проверка моделей / Model Checking (LTL/CTL и TLA+)"]
    B --> E["Столп 3: Абстрактная интерпретация (Связи Галуа и Astrée)"]
    B --> F["Столп 4: Интерактивное доказательство теорем (Coq / Lean 4 / Isabelle)"]
    C --> C1["Инварианты цикла I + автоматическое доказательство VC решателем Z3 SMT"]
    D --> D1["Структура Крипке M; символический обход 10^20 состояний через BDD/SAT/IC3"]
    E --> E1["Автоматическая аппроксимация сверху R_exact ⊆ γ(a#), доказывающая γ(a#) ∩ Bad = ∅"]
    F --> F1["Изоморфизм Карри — Ховарда: проверка математических доказательств микроядром"]

2. Столп 1: Дедуктивная верификация — Логика Флойда — Хоара, слабейшее предусловие и SMT-решатели

2.1 Тройка Хоара, инварианты цикла и ранговые функции

В 1969 году Чарльз Энтони Ричард Хоар (C. A. R. Hoare) создал логику Флойда — Хоара, в основе которой лежит тройка Хоара:

• Частичная корректность: Если до выполнения команды $C$ истинно предусловие $P$, и если $C$ завершается, то после выполнения истинно постусловие $Q$.
• Полная корректность: При предусловии $P$ команда $C$ гарантированно завершается за конечное число шагов и устанавливает $Q$.

Ключевые правила вывода включают аксиому присваивания $\{\,Q[E/x]\,\}\; x := E \;\{\,Q\,\}$ и правило цикла while с инвариантом цикла $I$ и строго убывающей натуральной ранговой функцией (вариантом) $V \in \mathbb{N}$:

С помощью исчисления слабейшего предусловия (Weakest Precondition, $\text{wp}(C, Q)$, Дейкстра 1975) верификация программы сводится к математическим условиям верификации (VCs): $P \implies \text{wp}(C, Q)$.

2.2 Доказательство корректности бинарного поиска в Dafny и Z3

Заменив вычисление середины на mid := low + (high - low) / 2 в языке Dafny, SMT-решатель Z3 (архитектура DPLL(T), объединяющая неинтерпретируемые функции EUF, линейную целочисленную арифметику LIA, битовые векторы $\mathcal{T}_{\text{BV}}$ и массивы $\mathcal{T}_{\text{A}}$) за миллисекунды автоматически доказывает полное отсутствие переполнений и выход за границы массива:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19

method BinarySearch(a: array<int>, key: int) returns (index: int)
  requires forall i, j :: 0 <= i < j < a.Length ==> a[i] <= a[j]
  ensures 0 <= index ==> index < a.Length && a[index] == key
  ensures index < 0 ==> forall k :: 0 <= k < a.Length ==> a[k] != key
{
  var low := 0;
  var high := a.Length;
  while low < high
    invariant 0 <= low <= high <= a.Length
    invariant forall i :: 0 <= i < a.Length && !(low <= i < high) ==> a[i] != key
    decreases high - low
  {
    var mid := low + (high - low) / 2; // Z3 доказывает: переполнения нет и 0 <= mid < a.Length!
    if a[mid] < key { low := mid + 1; }
    else if key < a[mid] { high := mid; }
    else { return mid; }
  }
  return -1;
}

3. Столп 2: Проверка моделей (Model Checking) и темпоральная логика

3.1 Структуры Крипке и темпоральная логика LTL / CTL

В 1981 году Кларк, Эмерсон и Сифакис (премия Тьюринга 2007) изобрели проверку моделей (Model Checking), а Лесли Лэмпорт (премия Тьюринга 2013) создал TLA+. Система моделируется как структура Крипке $M = (S, S_0, R, L)$, а её свойства записываются в LTL или CTL:

1. Безопасность (Safety — «Ничего плохого никогда не происходит»): Взаимное исключение: $$\text{LTL}: \quad \mathbf{G}\, \neg (\text{crit}_1 \land \text{crit}_2) \qquad \text{CTL}: \quad \mathbf{AG}\, \neg (\text{crit}_1 \land \text{crit}_2)$$
2. Живость (Liveness — «Что-то хорошее в итоге обязательно произойдёт»): Отсутствие голодания (Starvation Freedom): $$\text{LTL}: \quad \mathbf{G}\, (\text{req}_1 \implies \mathbf{F}\, \text{crit}_1) \qquad \text{CTL}: \quad \mathbf{AG}\, (\text{req}_1 \implies \mathbf{AF}\, \text{crit}_1)$$

3.2 Автоматы Бюхи, BDD, IC3 и применение TLA+ в Amazon Web Services (AWS)

Верификатор переводит отрицание спецификации $\neg \varphi$ в автомат Бюхи $A_{\neg \varphi}$ и проверяет пустоту синхронного произведения ($\mathcal{L}(M \times A_{\neg \varphi}) = \emptyset$). Для борьбы со взрывом пространства состояний используются бинарные диаграммы решений (BDD, Брайант 1986 / Макмиллан 1990), охватывающие более $10^{20}$ состояний, Bounded Model Checking (BMC) и алгоритм IC3 / PDR.

В Amazon Web Services (AWS) применение TLA+ (TLC) при проектировании S3 и DynamoDB позволило ещё до написания производственного кода выявить сложнейшую ошибку потери данных, требовавшую точной последовательности из 35 переплетённых шагов (разделение сети, задержки пакетов и смена лидера).

4. Столп 3: Абстрактная интерпретация и урок катастрофы ракеты Ариан-5

4.1 4 июня 1996 года: Почему ракета Ариан-5 стоимостью 370 млн долларов взорвалась через 37 секунд

4 июня 1996 года первый полёт (Flight 501) европейской ракеты-носителя Ariane 5 закончился самоуничтожением на 37-й секунде, что привело к потере 370 миллионов долларов. Инерциальная навигационная система (SRI) повторно использовала код на языке Ada от Ariane 4, где 64-битная вещественная переменная горизонтальной скорости (BH) преобразовывалась в 16-битное знаковое целое ($-32\,768 \dots +32\,767$). Из-за более мощного ускорения Ariane 5 значение BH превысило $32\,767$, вызвав необработанное аппаратное исключение переполнения (Operand Error). Резервный и основной компьютеры SRI отключились и отправили на шину диагностическую битовую последовательность, которую бортовой компьютер (OBC) принял за реальные данные об экстремальном крене и повернул сопла двигателей до упора, разрушив ракету.

4.2 Абстрактная интерпретация Кузо (1977), связи Галуа и триумф Astrée на Airbus A380

Созданная в 1977 году Патриком Кузо и Радией Кузо абстрактная интерпретация связывает конкретную решётку состояний $(\mathcal{C}, \subseteq) = (\mathcal{P}(\Sigma), \subseteq)$ с абстрактной областью $(\mathcal{A}, \sqsubseteq^\#)$ (интервалы $[a,b]$, октагоны $\pm x \pm y \le c$, выпуклые многогранники) через связь Галуа (Galois Connection):

При соблюдении условия локальной корректности $\alpha(F(\gamma(a^\#))) \sqsubseteq^\# F^\#(a^\#)$ и применении оператора расширения (Widening $\nabla$) абстрактная неподвижная точка гарантированно накрывает все достижимые состояния:

  flowchart TD
    subgraph Concrete["Конкретная область C = P(Σ) (Бесконечна / Неразрешима)"]
        S["Множество состояний S"] -->|"Конкретный переход F"| FS["Следующие состояния F(S)"]
        LFP_C["Достижимые состояния R_exact = lfp F"]
    end
    subgraph Abstract["Абстрактная область A (Интервалы / Октагоны / Эллипсоиды)"]
        A_elem["Абстрактное состояние a#"] -->|"Абстрактный переход F#"| FA["Следующее состояние F#(a#)"]
        LFP_A["Абстрактная неподвижная точка lfp F# (Сходимость через Widening ∇)"]
    end
    S -->|"Абстракция α(S)"| A_elem
    FA -->|"Конкретизация γ(F#(a#)) ⊇ F(S)"| FS
    LFP_A -->|"100% Гарантия: R_exact ⊆ γ(lfp F#)"| LFP_C

Статический анализатор Astrée полностью автоматически проверил бортовое ПО управления полётом Fly-by-Wire авиалайнера Airbus A380 (около 1 000 000 строк кода на C) с нулём ложных тревог, математически доказав полное отсутствие любых ошибок времени выполнения!

5. Столп 4: Интерактивное доказательство теорем (Coq / Lean 4 / Isabelle) и сравнение подходов

Основанные на изоморфизме Карри — Ховарда (высказывания как типы, доказательства как программы), интерактивные системы (Coq / Rocq, Lean 4, Isabelle/HOL) породили два шедевра:

1. CompCert (Ксавье Леруа, INRIA): Оптимизирующий компилятор C, формально верифицированный в Coq. При фаззинг-тестировании Csmith (PLDI 2011) в GCC и LLVM нашли более 325 ошибок компиляции, а в верифицированном ядре CompCert — ни одной!
2. seL4 (Гервин Кляйн и др.): Первое в мире микроядро ОС, формально верифицированное в Isabelle/HOL вплоть до бинарного кода ARM/RISC-V.