PHDays VII: lightning: Как доказывать программы

Небольшой доклад, который был прочитан мной на секции Lightning Talks конференции PHDays VII. Я постарался сделать из него анонс к часовому докладу на секции PDUG "Формальная верификация кода на языке Си". Думаю, что видеозапись этого пятиминутного доклада будет вряд ли выложена отдельным файлом. Здесь я приведу подробную расшифровку доклада.

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

Код: бинарный поиск нижней границы

Давайте на простом примере рассмотрим то, как это делается. Всем известная функция двоичного поиска с нижней границей. То есть, для входного массива [1,2,2,3] и искомого элемента 2, будет возвращён индекс 1(индексация с нуля). Все знают этот алгоритм, никто с первого раза правильно написать не может :) Давайте примерно вспомним как алгоритм работает.

Бинарный поиск нижней границы. Индексы.

В алгоритме две сходящихся границы: верхняя (right) и нижняя (left). Мы помним, что входной массив отсортирован по возрастанию.

Бинарный поиск нижней границы. Средний элемент.

В цикле поиска элементов вычисляется средний индекс (middle) между верхней и нижней границами. Здесь индекс вычисляется заведомо корректным образом, так чтобы не произошло ошибки целочисленного переполнения как это может быть в коде (left + right) / 2.

Бинарный поиск нижней границы. Обновление индексов.

В зависимости от того, в каком отношении порядка элемент в массиве по среднему индексу (middle) находится с искомым элементом (val), мы подвигает либо верхнюю, либо нижнюю границу поиска.

В каком контексте код работает корректно.

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

Входные данные. Массив. Память.

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

Входные данные. Массив. Структура.

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

Что делает код. Побочные действия.

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

Что делает код. Диапазон возвращаемого значения.

Вторым условием мы говорим, что возвращаемое значение функции находится в пределах границ массива. Что естественно, так как функция ищет индекс нижней границы элемента с значением val в отсортированном по возрастанию массиве a. Кто-то может заметить, что индексация в языке Си начинается с 0 и в таком случае \result == n выходит за границы массива a, и будет прав. Посмотрите внимательнее на код функции и поймите, в каком случае функция вернет подобный результат. (Ответ: когда все элементы массива a меньше val)

Что делает код. Смысл возвращаемого значения. Элементы массива до индекса-результата.

Третьим постусловием мы говорим, что все элементы во входном массиве по индексам до возвращенного (\result) строго меньше искомого элемента val.

Что делает код. Смысл возвращаемого значения. Элементы массива после индекса-результата.

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

Внутренний цикл.

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

Инварианты внутреннего цикла. Соотношение с постусловиями.

Если обратить внимание на то, как сформулированы второй и третий инвариант, то можно увидеть, что они практически цитируют два последних постусловия, за одним исключением. В постусловиях мы писали, что возвращённый функцией результат (индекс) разделяет массив на два подмассива: первый – с элементами строго до искомого, второй – с элементами не меньшими по значению, чем искомый. На цикле соблюдаются те же самые условия, только с двумя разными индексами: верхним (right) и нижним (left). То есть мы пишем, что на каждой итерации цикла выполнено: все элементы в массиве строго левее нижнего индекса строго меньше искомого элемента, а все элементы правее верхнего индекса – не меньше искомого. Из таких двух условий и из того, что верхний и нижний индексы сходятся друг к другу, будут доказаны постусловия.

Вариант внутреннего цикла. Оценочная функция. Завершимость цикла.

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

Как показывается соответствие кода спецификациям. Инструменты дедуктивной верификации.

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

На слайдах используется язык ACSL для спецификаций и инструменты Frama-C+Why3+Jessie2(AstraVer Fork).

Более серьезные примеры доказательств можно посмотреть по ссылкам:

  • https://github.com/evdenis/verker - доказательства корректности некоторых функций ядра Linux (здесь же готовая виртуальная машина с инструментами)
  • https://github.com/evdenis/acsl-proved - небольшие функции (некоторые - реальные алгоритмы, остальное - обучающие примеры) со спецификациями к ним и протоколами доказательств

Comments

comments powered by Disqus