Основы формальной верификации в Coq

Введение в Coq: функциональное программирование на языке Gallina и базовые типы

Добро пожаловать в курс «Основы формальной верификации в Coq». Это первая статья, в которой мы познакомимся с инструментом Coq, его внутренним языком Gallina и начнем писать первые функциональные программы. Если вы привыкли к императивным языкам вроде Python или C++, подход Coq может показаться вам необычным, но именно он лежит в основе создания математически надежного программного обеспечения.

Что такое Coq и зачем он нужен?

Coq — это интерактивная система доказательства теорем (proof assistant). В отличие от обычных компиляторов, которые просто превращают код в инструкции для процессора, Coq позволяет вам формулировать математические утверждения и писать формальные доказательства того, что эти утверждения верны.

В основе Coq лежит язык Gallina. На этом языке мы делаем две вещи:

Пишем программы и определяем типы данных.

Формулируем теоремы и доказательства.

Это возможно благодаря мощной теоретической базе, называемой исчислением конструкций (Calculus of Constructions). В этой системе «программы» и «доказательства» — это, по сути, одно и то же. Но пока мы не будем углубляться в теорию типов, а сосредоточимся на программировании.

!Схема показывает, как код на Gallina проходит через ядро Coq для получения верифицированной программы.

Первые шаги: Определение типов данных

В функциональном программировании мы начинаем с описания данных. В Coq создание нового типа данных осуществляется с помощью ключевого слова Inductive. Давайте определим простой тип, представляющий дни недели.

Разберем этот код: * Inductive означает, что мы определяем индуктивный тип данных. * day — это имя нашего нового типа. * : Type указывает, что day сам по себе является типом. * После := мы перечисляем конструкторы (monday, tuesday и т.д.). Это единственные возможные значения для типа day.

Теперь, когда у нас есть тип, мы можем написать функцию, которая работает с ним. Например, функцию, вычисляющую следующий рабочий день.

Функции и сопоставление с образцом

Для определения функций в Coq используется ключевое слово Definition. Язык Gallina является строго типизированным, поэтому мы должны указывать типы аргументов и возвращаемого значения.

Здесь мы видим конструкцию match ... with ... end. Это сопоставление с образцом (pattern matching). Это аналог switch или case в других языках, но гораздо более мощный. Coq строго следит за тем, чтобы вы рассмотрели все возможные варианты значений d. Если вы забудете, например, sunday, Coq выдаст ошибку.

Проверка работы кода

В Coq есть команды для взаимодействия с окружением. Они называются «Vernacular commands» и часто начинаются с заглавной буквы. Три самые важные:

Check — показывает тип выражения.

Compute — вычисляет значение выражения.

Print — показывает определение функции или типа.

Пример использования:

Булев тип (Booleans)

В стандартной библиотеке Coq булев тип определен точно так же, как мы определили дни недели — через перечисление:

Функции над булевыми значениями также определяются через сопоставление с образцом. Напишем функцию отрицания negb (логическое НЕ):

И функцию конъюнкции andb (логическое И):

Обратите внимание на лаконичность andb. Если b1 ложно, нам не важно, чему равно b2 — результат все равно будет false. Если b1 истинно, то результат полностью зависит от b2.

Натуральные числа: арифметика Пеано

Самый интересный базовый тип в Coq — это натуральные числа (nat). В обычных языках программирования числа — это 32 или 64 бита в памяти процессора. В Coq числа — это математическая абстракция, основанная на аксиомах Пеано.

Определение выглядит так:

Это рекурсивное определение:

O (заглавная буква O, не ноль) — это конструктор, представляющий ноль.

S — это конструктор, который принимает натуральное число и возвращает «следующее» за ним число (Successor).

Математически это записывается так:

Где — это базовый элемент, обозначающий ноль.

Где — это функция следования, примененная к нулю, что дает единицу.

Где — это функция следования, примененная к единице, что дает двойку.

И так далее для любого числа :

Где — это число, следующее за .

!Визуализация структуры натуральных чисел в Coq как вложенных конструкторов.

Такое представление кажется неэффективным для вычислений (и это правда для больших чисел), но оно идеально подходит для доказательств по индукции, чем мы займемся в следующих статьях.

Рекурсивные функции

Поскольку числа определены рекурсивно, функции для работы с ними тоже должны быть рекурсивными. В Coq для определения рекурсивной функции используется ключевое слово Fixpoint вместо Definition.

Давайте определим функцию проверки на четность evenb:

Разбор логики: * Если число — это O (0), то оно четное (true). * Если число — это S O (1), то оно нечетное (false). * Если число имеет вид S (S n') (то есть ), то его четность совпадает с четностью . Мы рекурсивно вызываем evenb для .

Сложение чисел

Теперь определим сложение. Вспомним математическое определение сложения через инкремент:

Где — любое число, а прибавление не меняет его значение.

Где — следующее число за , а означает, что мы переносим операцию инкремента наружу суммы.

В Coq мы обычно делаем рекурсию по первому аргументу:

Как это работает для plus 2 3 (то есть plus (S (S O)) (S (S (S O))))?

n не O, это S (S O). n' становится S O. Результат: S (plus (S O) 3).

Рекурсивный вызов. n теперь S O. n' становится O. Результат: S (S (plus O 3)).

Рекурсивный вызов. n теперь O. Срабатывает первая ветка match. Возвращаем m (то есть 3).

Собираем результат: S (S 3) -> S (S (S (S (S O)))) -> 5.

Важное правило завершения (Termination)

Coq требует, чтобы все функции завершались. Вы не можете написать бесконечный цикл while(true). Это необходимо для логической непротиворечивости системы.

При использовании Fixpoint Coq автоматически проверяет, что рекурсивный вызов происходит над «меньшим» аргументом (structural recursion). В примере с plus, на каждом шаге n уменьшается (от S n' к n'), поэтому Coq гарантирует, что вычисление когда-нибудь достигнет O и остановится.

Заключение

Мы познакомились с основами языка Gallina: * Определили перечислимые типы (day, bool). * Узнали, как устроены натуральные числа Пеано (nat). * Научились писать простые (Definition) и рекурсивные (Fixpoint) функции. * Использовали сопоставление с образцом (match).

Это фундамент, на котором строится вся формальная верификация. В следующей статье мы перейдем от написания программ к написанию доказательств их свойств, используя тактики Coq.

Логика и доказательства: тактики, пропозициональное исчисление и соответствие Карри-Говарда

В предыдущей статье мы научились определять типы данных и писать функции на языке Gallina. Мы увидели, что Coq — это мощный язык программирования. Однако главная сила Coq заключается не в вычислениях, а в доказательствах.

Сегодня мы перейдем от написания программ к доказательству теорем. Мы узнаем, как математическая логика представляется в Coq, познакомимся с фундаментальным принципом, связывающим программы и доказательства, и изучим основные инструменты для проведения доказательств — тактики.

Соответствие Карри-Говарда

Прежде чем написать первое доказательство, нужно понять, что именно мы делаем. В большинстве систем верификации логика и программирование — это разные слои. Но в Coq они едины. Это единство описывается изоморфизмом Карри-Говарда.

Суть его проста и красива: Утверждение — это Тип, а Доказательство — это Программа.

!Визуализация соответствия между логическими и программными концепциями в Coq.

Рассмотрим это подробнее:

Утверждения (Propositions) — это типы. Когда мы пишем теорему, мы на самом деле определяем тип. В Coq есть специальный сорт типов, называемый Prop, в котором живут логические утверждения.

Доказательства — это значения. Доказать утверждение — значит написать программу (терм), которая имеет тип . Если компилятор принимает эту программу, значит, доказательство верно.

Например, импликация в логике:

Где — посылка, а — следствие.

В Coq это записывается как P -> Q. С точки зрения программирования, это тип функции, которая принимает аргумент типа P (доказательство ) и возвращает результат типа Q (доказательство ).

Режим доказательства и тактики

Хотя доказательства являются программами, писать их вручную (как мы писали функции Definition) бывает сложно и утомительно. Поэтому в Coq используется интерактивный режим доказательства.

Вместо того чтобы писать весь код сразу, мы используем тактики — команды, которые шаг за шагом строят доказательство за нас. Мы формулируем цель (Goal), а тактики разбивают её на подцели или решают её.

Начнем с простейшего примера. Докажем, что для любого утверждения , из следует .

Разберем этот скрипт построчно:

Theorem (или Lemma, Example) объявляет имя my_first_proof и тип утверждения. forall — это квантор всеобщности.

Proof. переводит Coq в режим доказательства.

intros P p_hypothesis. — тактика введения. Она берет переменные из квантора forall и посылки импликации -> и переносит их в контекст (список известных нам фактов). Теперь у нас есть предположение, что истинно (обозначим это доказательство как p_hypothesis).

apply p_hypothesis. — тактика применения. Наша цель — доказать . У нас в контексте есть p_hypothesis, тип которого как раз . Мы применяем его, и цель решена.

Qed. (Quod Erat Demonstrandum) — завершает доказательство, проверяет построенный терм и сохраняет теорему.

Что происходит «под капотом»?

Если после Qed мы напишем Print my_first_proof, мы увидим:

Это обычная лямбда-функция (аналог lambda P, x: x в Python). Тактики просто помогли нам её написать.

Пропозициональная логика

Теперь рассмотрим основные логические связки и тактики для работы с ними.

Импликация (Implication, ->)

Импликация означает «если , то ».

* Как доказать: Используйте intros. Это перемещает в контекст, и целью становится . * Как использовать: Если у вас есть гипотеза и цель , используйте apply H. Это сменит цель на (ведь чтобы получить , нам теперь достаточно доказать ).

Пример (Modus Ponens):

Здесь H_imp имеет тип P -> Q, а H_p имеет тип P. Мы применяем функцию H_imp к аргументу H_p и получаем результат типа Q.

Конъюнкция (And, /\)

Конъюнкция означает «и , и ».

В Coq она обозначается A /\\\ B.

* Как доказать: Если текущая цель A /\\\ B, используйте тактику split. Это разобьет доказательство на две подцели: отдельно доказать и отдельно доказать . * Как использовать: Если у вас есть гипотеза , используйте destruct H as [HA HB]. Это разобьет гипотезу на две отдельные: (доказательство ) и (доказательство ).

Пример коммутативности И:

Дизъюнкция (Or, \/)

Дизъюнкция означает «или , или ».

В Coq она обозначается A \/ B.

* Как доказать: Если цель A \/ B, вы должны выбрать, какую часть доказывать. Тактика left меняет цель на , тактика right меняет цель на . * Как использовать: Если у вас есть гипотеза , используйте destruct H as [HA | HB]. Это создаст два варианта развития событий (case analysis). В одной ветке доказательства мы считаем, что верно , в другой — что верно . Мы обязаны доказать цель в обоих случаях.

!Схема работы тактики destruct для дизъюнкции: разбор случаев.

Ложь и Истина (False, True)

* True: Утверждение, которое всегда истинно. Оно не несет информации. Доказывается тактикой trivial или reflexivity (хотя редко бывает целью). * False: Логическое противоречие. У этого типа нет конструкторов, то есть невозможно создать значение типа False (если только вы не ввели противоречивые аксиомы).

Принцип взрыва (Ex Falso Quodlibet):

Где — ложь, а — любое утверждение.

Если у вас в контексте появилось противоречие (гипотеза типа False), вы можете доказать что угодно. Для этого используется тактика exfalso (меняет цель на False) или destruct H (если имеет тип False).

Отрицание (Not, ~)

Отрицание в Coq определяется через импликацию и ложь:

Где — отрицание , которое эквивалентно следованию лжи из .

Это означает: «Если мы предположим , мы придем к противоречию». В Coq это пишется как ~P.

* Как доказать: Так как ~P — это просто P -> False, используйте intros H, чтобы перенести в контекст, и затем пытайтесь вывести False (найти противоречие). * Как использовать: Если у вас есть H: ~P и вы доказали HP: P, то apply H in HP даст вам False.

Автоматизация: первые шаги

Coq предоставляет мощные тактики автоматизации, которые сами ищут доказательства.

assumption: Ищет в контексте гипотезу, которая в точности совпадает с целью.

reflexivity: Доказывает равенства вида .

auto: Пытается применить intros, apply и assumption на ограниченную глубину, чтобы решить простые логические задачи.

Пример с использованием автоматизации:

Здесь auto самостоятельно находит, что нужно ввести переменные и применить импликацию.

Заключение

Мы рассмотрели основы пропозициональной логики в Coq. Главное, что нужно запомнить:

* Доказательства — это программы (функции), строящие термы типов-утверждений. * Тактики (intros, apply, split, destruct) помогают нам строить эти программы интерактивно. * Логические связки имеют прямые аналоги в типах данных (конъюнкция — пара, дизъюнкция — сумма типов).

В следующей статье мы вернемся к натуральным числам и изучим доказательство по индукции — один из самых мощных инструментов верификации программ.

Индуктивные типы данных и доказательство методом математической индукции

Добро пожаловать в третью часть курса «Основы формальной верификации в Coq». В предыдущих статьях мы научились определять типы данных, писать рекурсивные функции и доказывать простые логические утверждения с помощью тактик destruct, intros и apply.

Однако, когда мы работаем с рекурсивными структурами данных — такими как натуральные числа или списки — простой разбор случаев (destruct) часто оказывается недостаточным. Нам нужен более мощный инструмент, который является сердцем математики и информатики — математическая индукция.

Почему destruct недостаточно?

Вспомним определение сложения plus, которое мы разбирали в первой статье. Оно определено рекурсивно по первому аргументу:

Благодаря этому определению, Coq автоматически может вычислить, что plus 0 m равно m. Но что насчет plus n 0? Интуитивно мы знаем, что . Попробуем доказать это с помощью destruct.

Почему мы застряли? destruct разбил задачу на два случая. В случае S n' мы должны доказать, что S (n' + 0) = S n'. Чтобы это доказать, нам нужно знать, что n' + 0 равно n'. Но destruct не дает нам этой информации — он просто «снимает» верхний конструктор.

Нам нужно предположение, что свойство уже выполняется для меньшего числа n'. Это и есть индуктивная гипотеза.

Принцип математической индукции

Математическая индукция похожа на принцип домино. Чтобы уронить бесконечный ряд костяшек, нужно сделать две вещи:

Уронить первую костяшку (База индукции).

Доказать, что если падает костяшка , то она обязательно уронит костяшку (Индуктивный переход).

!Визуализация принципа индукции: доказательство базы и шага гарантирует истинность для всех элементов.

Формально для натуральных чисел это записывается так:

Где: * — это свойство, которое мы хотим доказать (предикат). * — утверждение, что свойство верно для нуля (база). * — индуктивная гипотеза (предположение, что свойство верно для ). * — утверждение, что свойство верно для следующего числа (шаг). * — вывод, что свойство верно для всех чисел.

Тактика induction

В Coq для этого используется тактика induction. Она работает похоже на destruct, но добавляет в контекст индуктивную гипотезу при рассмотрении рекурсивного случая.

Синтаксис: induction n as [| n' IHn'].

Здесь: * n — переменная, по которой ведется индукция. * [| ...] — разделяет случаи (как в destruct). * Первая часть (до |) пуста, так как у конструктора O нет аргументов. * Во второй части n' — это «предыдущее» число, а IHn' — имя для индуктивной гипотезы (Inductive Hypothesis for n').

Доказательство

Вернемся к нашей теореме.

После simpl наша цель выглядит так:

Обратите внимание на новую строку в контексте: IHn'. Она говорит нам, что равенство верно для n'. Нам нужно использовать этот факт, чтобы заменить n' + 0 на n' внутри нашей цели.

Для подстановки равенств используется тактика rewrite.

Тактика rewrite

Тактика rewrite изменяет цель (или гипотезу), используя доказанное равенство.

* rewrite -> H (или просто rewrite H): находит в цели левую часть равенства и заменяет её на правую. * rewrite <- H: находит правую часть и заменяет на левую.

Завершим доказательство:

Ассоциативность сложения

Рассмотрим более сложный пример: доказательство того, что . В определении plus рекурсия идет по первому аргументу, поэтому индукцию тоже выгодно проводить по первому аргументу ().

Без индукции мы бы застряли на шаге simpl, получив выражение с S снаружи, которое нельзя упростить дальше без знания о внутренней структуре.

Индукция для других типов данных

Индукция работает не только для чисел, но и для любых индуктивных типов (отсюда и название). Рассмотрим списки.

Определение списка

В Coq списки определяются как:

* nil (или []) — пустой список. * cons x l (или x :: l) — список, где x — первый элемент (голова), а l — остальной список (хвост).

Принцип индукции для списков звучит так: «Если утверждение верно для пустого списка [], и если из того, что оно верно для списка l, следует, что оно верно для списка x :: l, то утверждение верно для любого списка».

Пример: Свойства длины списка

Пусть у нас есть функция length, вычисляющая длину, и app (++), соединяющая два списка. Докажем, что длина конкатенации равна сумме длин.

Где — функция длины, а — операция объединения списков.

Обратите внимание: структура доказательства идентична доказательству для чисел. nil соответствует O, а cons соответствует S.

Вложенная индукция

Иногда одной индукции недостаточно. Бывают теоремы, где нужно проводить индукцию внутри индукции или индукцию по одной переменной, а затем разбор случаев по другой.

Главное правило: если функция рекурсивна по аргументу n, то и доказывать свойства этой функции чаще всего нужно индукцией по n.

Заключение

Мы изучили один из самых важных инструментов в Coq:

Индукция позволяет доказывать утверждения для бесконечных множеств данных (все натуральные числа, все возможные списки).

Тактика induction генерирует базовый случай и индуктивный шаг с гипотезой.

Тактика rewrite позволяет использовать равенства (в том числе индуктивную гипотезу) для преобразования цели.

Теперь вы можете доказывать фундаментальные свойства арифметики и структур данных, которые невозможно проверить простым тестированием. В следующей статье мы поговорим о полиморфизме и функциях высшего порядка, чтобы писать более универсальный код.

Автоматизация доказательств и продвинутые тактики для упрощения верификации

В предыдущих статьях мы прошли путь от определения простых типов данных до доказательства свойств рекурсивных функций методом математической индукции. Вы наверняка заметили, что доказательства могут становиться длинными и повторяющимися. Часто нам приходится делать очевидные вещи: многократно применять intros, rewrite или разбирать тривиальные случаи.

В этой статье мы перейдем на новый уровень владения Coq. Мы изучим тактики, которые позволяют автоматизировать рутинную работу, и познакомимся с инструментами для работы с равенствами конструкторов. Это сделает ваши доказательства короче, чище и устойчивее к изменениям в коде.

Работа с конструкторами: discriminate и injection

Когда мы определяем индуктивный тип (например, натуральные числа nat или списки list), Coq автоматически гарантирует два фундаментальных свойства конструкторов:

Различимость (Disjointness): Значения, созданные разными конструкторами, никогда не могут быть равны.

Инъективность (Injectivity): Если значения, созданные одним конструктором, равны, то и аргументы этого конструктора равны.

Для использования этих свойств существуют специальные тактики.

Тактика discriminate

Рассмотрим утверждение: . В терминах Coq это . Интуитивно мы знаем, что это ложь. Но как это доказать формально?

В логике Coq ложное утверждение в посылке позволяет доказать что угодно (принцип взрыва). Если у нас в контексте появляется гипотеза вида O = S n, это логическое противоречие.

Тактика discriminate смотрит на уравнение в гипотезе или цели. Если в уравнении с разных сторон стоят разные конструкторы (например, O и S, или true и false), она сообщает Coq, что это ситуация невозможна.

Пример:

Здесь discriminate H замечает, что O не может быть равно S n, находит противоречие и завершает доказательство, так как из лжи следует что угодно.

Тактика injection

Второе свойство — инъективность. Рассмотрим уравнение:

Где — следующее число за , а — следующее число за .

Из этого равенства логично следует, что . Тактика injection позволяет «снять» внешние конструкторы и получить равенство аргументов.

!Визуализация работы тактик discriminate (обнаружение противоречия) и injection (извлечение аргументов).

Пример использования:

Конструкция as Hnm позволяет сразу дать имя новому полученному факту. Без неё равенство добавилось бы в цель доказательства как посылка.

Автоматизация поиска: auto

До сих пор мы применяли тактики вручную. Однако Coq обладает встроенным механизмом поиска доказательств. Самая базовая тактика автоматизации — auto.

auto пытается решить текущую цель, комбинируя: * intros * apply (используя гипотезы из контекста и базу данных известных лемм) * reflexivity

Она строит дерево поиска, пытаясь применить эти тактики на определенную глубину (по умолчанию 5 шагов).

Пример, где auto экономит время:

Вместо того чтобы писать intros P Q R HPQ HQR HP. apply HQR. apply HPQ. apply HP., мы просто пишем auto. Coq сам находит цепочку применений.

Важно: auto не умеет делать induction или сложный destruct, так как это может привести к бесконечному ветвлению. Также auto не переписывает равенства (rewrite) по умолчанию.

Арифметика: тактика lia

При работе с натуральными числами часто возникают задачи, тривиальные для школьника, но сложные для формального вывода через аксиомы Пеано. Например:

Где — числа, а — отношение строгого порядка.

Доказывать это через индукцию утомительно. Для таких задач в Coq (через подключение библиотеки Require Import Lia.) существует тактика lia (Linear Integer Arithmetic).

Она решает любые системы линейных уравнений и неравенств над целыми и натуральными числами.

Если ваше утверждение касается сложения, вычитания, умножения на константу и сравнения чисел — lia почти всегда решит его мгновенно.

Управление потоком доказательства

Продвинутые пользователи Coq редко применяют тактики по одной. Они комбинируют их, создавая скрипты, похожие на программы.

Оператор ; (Точка с запятой)

Это самый мощный инструмент для сокращения кода. Запись tactic1; tactic2 означает:

Применить tactic1.

Применить tactic2 ко всем подцелям, которые породила tactic1.

Вспомним доказательство ассоциативности сложения из прошлой статьи. С использованием ; и auto оно становится тривиальным:

Мы можем переписать это еще короче:

Тактика try

Иногда мы хотим применить тактику, но не уверены, сработает ли она. Если обычная тактика падает с ошибкой, скрипт останавливается. try tactic пытается выполнить тактику: если получается — отлично, если нет — ничего не делает и не выдает ошибку.

Это идеально сочетается с ;.

Эта строка означает: «Проведи индукцию, затем упрости выражение во всех случаях, и попытайся завершить доказательство рефлексивностью там, где это возможно».

Тактика apply ... with ...

Иногда Coq не может автоматически догадаться, какое значение подставить вместо переменной при применении леммы. Рассмотрим свойство транзитивности равенства:

Где — элементы некоторого типа, а стрелки обозначают импликацию.

Допустим, у нас есть цель a = c, и мы хотим использовать транзитивность. Coq видит x (это a) и z (это c), но он не знает, чем должно быть y. В этом случае мы должны подсказать:

Мы явно указываем with (y := b), чтобы Coq понял, через какой промежуточный элемент мы строим доказательство.

Тактика replace

Иногда rewrite бывает недостаточно гибким, или вы хотите заменить конкретное подвыражение на другое, доказав их равенство позже. Для этого используется replace.

Синтаксис: replace (old_term) with (new_term).

Это действие:

Заменяет в цели old_term на new_term.

Создает новую подцель, где вы обязаны доказать, что old_term = new_term.

Это очень полезно для «расчистки» сложных выражений перед применением основной логики.

Заключение

Мы рассмотрели инструменты, которые превращают Coq из строгого экзаменатора в мощного помощника:

* discriminate и injection позволяют использовать свойства конструкторов типов. * auto берет на себя рутинный поиск доказательств. * lia мгновенно решает арифметические задачи. * ; и try позволяют структурировать доказательство и применять тактики массово.

Использование этих тактик не делает доказательство менее строгим — ядро Coq все равно проверяет каждый шаг. Они лишь помогают вам быстрее объяснить свои намерения машине.

Теперь вы обладаете достаточным арсеналом, чтобы верифицировать нетривиальные алгоритмы. В следующих частях курса мы применим эти знания для создания и верификации структур данных.

Практическое применение: верификация алгоритмов и экстракция исполняемого кода

Поздравляю! Вы прошли путь от знакомства с базовыми типами данных до автоматизации доказательств с помощью тактик. Мы научились говорить на языке Gallina и убеждать Coq в нашей правоте. Но до сих пор наши программы жили только внутри среды доказательства.

В этой, заключительной статье курса, мы ответим на главный вопрос: как использовать Coq для создания реального, работающего программного обеспечения?

Мы пройдем полный цикл разработки верифицированного алгоритма:

Напишем функцию сортировки.

Формализуем требования к ней (спецификацию).

Докажем, что функция соответствует требованиям.

Экстрагируем (извлечем) из Coq код на языке OCaml или Haskell, готовый к компиляции.

Постановка задачи: Сортировка вставками

Для примера мы возьмем классический алгоритм — сортировку вставками (Insertion Sort). Он прост в реализации и идеально подходит для демонстрации принципов верификации.

Наша цель — написать функцию sort, которая принимает список натуральных чисел и возвращает этот же список, но упорядоченный по возрастанию.

!Процесс превращения спецификации и кода в верифицированную программу.

Шаг 1: Реализация алгоритма

Сначала напишем код, как если бы мы программировали на обычном функциональном языке. Нам понадобятся две функции:

insert: вставляет число в уже отсортированный список на нужное место.

sort: рекурсивно сортирует хвост списка и вставляет голову на нужное место.

Мы написали код. В обычном программировании мы бы написали пару тестов и успокоились. Но в Coq мы идем дальше.

Шаг 2: Формальная спецификация

Что значит «список отсортирован»? Нам нужно определить это понятие математически. В Coq мы можем определить предикат sorted индуктивно.

Разберем это определение:

sorted_nil: Пустой список отсортирован.

sorted_1: Список из одного элемента отсортирован.

sorted_cons: Если у нас есть список, начинающийся с , который уже отсортирован, и мы добавляем в начало, то новый список будет отсортирован только если .

Математически это условие для конструктора sorted_cons выглядит так:

Где — добавляемый элемент, — первый элемент текущего списка, — хвост списка, — логическое И, а — импликация.

Шаг 3: Верификация (Доказательство корректности)

Теперь самое интересное. Нам нужно доказать теорему: «Для любого списка l, результат функции (sort l) является sorted».

Доказательство разбивается на две части (леммы).

#### Лемма 1: Корректность вставки

Сначала докажем, что если мы вставляем число в уже отсортированный список, результат остается отсортированным.

Здесь мы используем индукцию по доказательству того, что список отсортирован. Это мощный прием: мы разбираем не структуру списка, а структуру причины, почему он отсортирован.

#### Теорема: Корректность сортировки

Имея лемму insert_sorted, доказать основную теорему очень просто.

Разберем логику доказательства:

База: sort [] возвращает []. sorted [] верно по определению (sorted_nil).

Шаг: Пусть хвост t после сортировки sort t дает отсортированный список (индуктивная гипотеза IH).

Нам нужно доказать, что insert h (sort t) тоже отсортирован.

Мы применяем лемму insert_sorted. Она требует, чтобы аргумент (sort t) был отсортирован.

Но это и есть наша гипотеза IH! Доказательство завершено.

Теперь мы математически гарантируем: наша функция sort никогда не вернет неотсортированный список. Никаких багов с порядком элементов.

> Важное замечание: Полная корректность сортировки требует доказательства еще одного факта: результирующий список должен быть перестановкой (permutation) исходного. Иначе функция, которая всегда возвращает пустой список [], тоже считалась бы корректной (ведь пустой список отсортирован). В рамках этой статьи мы опустим доказательство перестановки, но в реальных проектах оно обязательно.

Экстракция кода (Extraction)

Мы написали алгоритм на языке Gallina. Но Gallina не выполняется на процессоре напрямую. Чтобы запустить нашу программу, нам нужно перевести её на язык общего назначения, такой как OCaml, Haskell или Scheme.

Coq имеет встроенный механизм экстракции. Его гениальность заключается в использовании соответствия Карри-Говарда и разделении типов на Set (данные) и Prop (логические утверждения).

При экстракции Coq:

Берет все определения из Set и Type (числа, списки, функции sort, insert) и транслирует их в целевой язык.

Удаляет все, что относится к Prop (теоремы, доказательства, леммы). Доказательства нужны только для уверенности в момент компиляции, в рантайме они не нужны.

Пример экстракции в OCaml

Добавим в конец нашего файла следующие команды:

Coq выведет в консоль сгенерированный код на OCaml:

Обратите внимание: в этом коде нет ни следа от sorted, insert_sorted или sort_is_sorted. Весь «строительный лес» доказательств убран, осталось только чистое, эффективное и гарантированно правильное здание алгоритма.

Вы можете сохранить этот код в файл .ml и скомпилировать его обычным компилятором OCaml.

Оптимизация и типы данных

В примере выше натуральные числа nat транслировались в индуктивный тип O | S of nat. Это очень медленно для больших чисел (число 1000 будет занимать 1000 вложенных конструкторов).

Мы можем настроить экстракцию так, чтобы типы Coq отображались в эффективные типы целевого языка.

Эта команда говорит Coq: «Когда видишь nat, используй стандартный int из OCaml». Теперь наша сортировка будет работать с быстрыми машинными целыми числами.

Заключение курса

Мы завершаем курс «Основы формальной верификации в Coq». Давайте оглянемся назад.

Мы начали с того, что программирование может быть математикой. Мы узнали, что: * Типы — это утверждения. * Программы — это доказательства. * Coq — это инструмент, который проверяет эти доказательства.

В этой статье мы увидели конечную цель всего процесса: получение доверенного кода.

В индустрии такой подход применяется там, где цена ошибки слишком высока: * CompCert: полностью верифицированный компилятор языка C. Он гарантирует, что оптимизации не меняют семантику программы. * Project Everest: верифицированный стек протокола HTTPS. * Криптография: алгоритмы шифрования, в которых математически доказано отсутствие утечек данных по сторонним каналам.

Формальная верификация требует времени и усилий. Но взамен она дает то, чего не могут дать тесты: абсолютную гарантию того, что программа делает именно то, что от неё требуется. Ни больше, ни меньше.

Спасибо, что прошли этот путь. Пусть ваш код всегда компилируется, а тактики всегда находят решение!