Практическое введение

Данная статья является введением в язык ACSL и набор инструментов Astraver. Для получения более подробной информации рекомендуется обратиться, например, к руководству ACSL by Example.

Доказательство полной корректности программы целочисленного деления на языке Си

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

struct div_result {
    int z1;
    int z2;
};

struct div_result div(int x1, int x2) {
    int y1 = 0;
    int y2 = x1;
    struct div_result res;

    while (y2 >= x2) {
        y1++;
        y2 -= x2;
    }

    res.z1 = y1;
    res.z2 = y2;
    return res;
}

В наборе инструментов Astraver для разработки спецификаций используется язык ACSL (ANSI/ISO C Specification Language). Спецификации задаются внутри комментариев специального вида, начинающихся с символа @, например, /*@ */ или //@. Для задания предусловия используется ключевое слово requires, для задания постусловия — ensures. Единственная выходная переменная имеет специальное имя \result. Ниже приведен пример пред- и постусловий для функции целочисленного деления.

/*@ requires x1 >= 0;
    requires x2 > 0;
    ensures \result.z1 * x2 + \result.z2 == x1;
    ensures 0 <= \result.z2 <= x2;
*/
struct div_result div(int x1, int x2);

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

Помимо пред- и постусловий, в спецификации необходимо задать для цикла инвариант, а также так называемый вариант, являющийся оценочной функцией на фундированном множестве, являющемся множеством натуральных чисел с отношением порядка <. Для этого используются соответственно ключевые слова loop invariant и loop variant. Точки сечения для программы выбираются инструментом автоматически.

/*@ loop invariant y2 + x2 * y1 == x1;
    loop invariant y2 >= 0;
    loop variant y2 - x2;
*/
while (y2 >= x2);

Теперь можно запустить набор инструментов astraver (предполагается, что он установлен, а программа целочисленного деления со спецификациями находится в текущей директории в файле div.c).

$ frama-c -jessie div.c

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

Окно данной среды разделено на три части.

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

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

В правой части окна можно просмотреть исходный код функции, код сгенерированных условий верификации и т. д.

Для доказательства выберем условие верификации «Function div, default behavior» и разобьем его на более мелкие условия двумя нажатиями кнопки Split.


После первого нажатия кнопки Split условие Default behavior будет разбито на три условия: инициализация инварианта цикла (loop invariant init), сохранение инварианта цикла (loop invariant preservation) и выполнение постусловия (postcondition). После второго нажатия каждое из них разобьется на более мелкие условия, соответствующие выполнению каждой части условия на каждом возможном пути. Выбрав отдельное условие и вкладку Task в правой части окна, можно просмотреть условие, которое будет доказываться, и путь, на котором оно будет доказываться. В примере, приведенном ниже, будет доказываться выполнение постусловия \( z_1 x_2 + z_2 = x_1 \).

Наконец, для доказательства следует выбрать условие верификации и запустить средство доказательства (например, Alt-Ergo) нажатием соответствующей кнопки. При выборе уже разбитого кнопкой Split условия оно будет доказано по частям путем доказательства каждого из более мелких условий в отдельности. На снимке экрана ниже полностью доказаны частичная и полная корректность функции целочисленного деления (условия верификации behaviors и safety). Можно видеть, что для safety доказана правильность обращения к структуре div_result (Pointer index bounds), отсутствие переполнений целочисленных значений (integer overflow), уменьшение варианта цикла (т. е. завершаемость функции) и т. д.; для behaviors доказано выполнение инварианта цикла перед началом цикла (loop invariant init), сохранение инварианта на каждом шаге цикла (loop invariant preservation) и выполнение постусловия функции (Postcondition (Ensures clause)). В правом столбце таблицы указано итоговое время работы средств доказательства для каждого условия верификации.




Другие возможности языка ACSL

Далее будут рассмотрены некоторые конструкции языка ACSL, необходимые для разработки спецификаций.

Указатели

Помимо знакомой по языку Си арифметики указателей, в языке ACSL задан встроенный предикат \valid, позволяющий задать в качестве предусловия корректность переданного в качестве параметра указателя и его размер. В приведенном ниже простейшем примере параметрами функции являются два указателя p и q; в качестве предусловия указана их корректность. Как следует из постусловия, функция при необходимости меняет местами значения в ячейках памяти по двум указателям таким образом, чтобы второе было больше либо равно первому.

/*@ requires \valid(p) && \valid(q);
    ensures *p<=*q;
*/
void max_ptr(int *p, int *q);

Поведения

В следующем примере спецификация описывает функцию более подробно. Выделено два варианта поведения функции: p_minimum, когда первое значение меньше второго, и q_minimum в противоположном случае. С помощью встроенной функции \old, описывающей значение переменной в момент начала выполнения функции, указывается, что в первом варианте поведения значения по указателям после выполнения функции равны значениям до ее выполнения, а во втором — поменяны местами. Конструкции complete behaviors и disjoint behaviors говорят о том, что поведения являются соответственно исчерпывающими и взаимоисключающими.

/*@ requires \valid(p) && \valid(q);
    ensures *p <= *q;
    behavior p_minimum:
        assumes \old(*p) <= \old(*q);
        ensures *p == \old(*p);
        ensures *q == \old(*q);
    behavior q_minimum:
        assumes \old(*p) <= \old(*q);
        ensures *p == \old(*q);
        ensures *q == \old(*p);
complete behaviors p_minimum, q_minimum; 
disjoint behaviors p_minimum, q_minimum; 
*/ 
void max_ptr(int *p, int *q);

Массивы

В данном примере рассматривается спецификация для функции поиска максимального значения в массиве. С помощью конструкции \valid(p + (0..n-1)) задается область корректных значений по переданному указателю p. Кроме того, в примере содержится две новых конструкции: \forall и \exists. В данном случае они используются для задания соответствия между значениями переданного массива и выходной переменной функции. Конструкция \forall указывает, что для всех значений i, соответствующих корректным индексам в массиве, выполняется условие: выходная переменная больше либо равна элементу массива с индексом i. Конструкция \exists указывает, что существует хотя бы один элемент массива, значение которого равно выходной переменной.

/*@ requires n > 0;
    requires \valid(p + (0..n-1));
    ensures \forall int i; 0 <= i <= n - 1 ==> \result >= p[i];
    ensures \exists int e; 0 <= e <= n - 1 && \result == p[e];
*/
int max_seq(int *p, int n);

Побочные эффекты

Приведенная выше спецификация может выполняться, например, в случае, если функция обнулит все значения в массиве, а затем вернет 0. Кроме того, функция может модифицировать глобальные переменные, что никак не указано в ее спецификации. Чтобы избежать этого, можно использовать функцию \old, однако проверить значения всех глобальных переменных далеко не всегда представляется возможным. В таких случаях можно использовать конструкцию assigns, которой передается список переменных, изменяемых функцией, либо \nothing, если побочные эффекты отсутствуют.

/*@ requires n > 0;
    requires \valid(p + (0..n-1));
    assigns \nothing;
    ensures \forall int i; 0 <= i <= n - 1 ==> \result >= p[i];
    ensures \exists int e; 0 <= e <= n - 1 && \result == p[e];
*/
int max_seq(int *p, int n);

Предикаты и логические функции

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

typedef struct _list { int element; struct _list *next; } list;


Можно определить отношение достижимости для списка и его элемента следующим образом:

/*@ inductive reachable{L} (list *root, list *node) {
        case root_reachable{L}:
            \forall list *root; reachable(root, root);
        case next_reachable{L}:
            \forall list *root, *node;
            \valid(root) ==> reachable(root->next, node) ==>
                reachable(root,node);
    }
*/

Нотация {L} говорит о том, что предикат принимает в качестве параметра метку, соответствующую состоянию памяти. В подобных случаях ее обычно не требуется задавать явным образом, она будет выведена из контекста (например, при использовании предиката в предусловии будет использовано состояние памяти на момент начала выполнения функции).

Используя этот предикат, можно определить, например, предикат, различающий конечные и кольцевые списки:

/*@ predicate finite{L}(list *root) = reachable(root, \null);
*/

Также можно определить логическую функцию, определяющую длину списка:

/*@ axiomatic Length {
        logic integer length{L}(list *l);
        axiom length_nil{L}: length(\null) == 0;
 
        axiom length_cons{L}: 
            \forall list *l, integer n;
                finite(l) && \valid(l) ==> 
                    length(l) == length(l->next) + 1;
}
*/

Теперь можно использовать определенные выше предикаты и логическую функцию при написании спецификации для функции поиска максимального элемента в списке. Ключевое слово terminates говорит об условии, которое должно выполняться, чтобы функция завершалась; в данном случае список должен являться конечным.

/*@ requires \valid(root);
    assigns \nothing;
    terminates finite(root);
    ensures \forall list *l; 
        \valid(l) && reachable(root,l) ==>
            \result >= l->element;
    ensures \exists list *l;
        \valid(l) && reachable(root,l) &&
        \result == l->element;
*/
int max_list(list *root);

Вызовы функций

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

#define UINT_MAX (~0U)

/*@ logic integer logic_square(integer x) = x * x; */
/*@ requires logic_square(x) < UINT_MAX;
    ensures \result == logic_square(x);
*/
unsigned int square(unsigned int x) {
    return x*x;
}

/*@ requires logic_square(x) < UINT_MAX;
    requires logic_square(y) < UINT_MAX;
    requires logic_square(x) + logic_square(y) < UINT_MAX;
    ensures \result == logic_square(x) + logic_square(y);
*/
unsigned int sum_of_squares(unsigned int x, unsigned int y) {
    return square(x) + square(y);
}

При запуске astraver после нажатия кнопки split можно видеть, что условие верификации Function_sum_of_squares_safety состоит из двух условий Precondition for square, каждое из которых соответствует выполнению предусловия функции при одном из двух ее вызовов, и условия integer overflow, соответствующего отсутствию переполнения. Условие Function_square_safety состоит только из одного условия integer overflow, т.к. вызовы других функций в ней отсутствуют.

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

#define UINT_MAX (~0U)

/*@ logic integer logic_square(integer x) = x * x; */
/*@ requires logic_square(x) < UINT_MAX;
    ensures \result == logic_square(x);
*/
unsigned int square(unsigned int x) {
    return x*x + 1;
}

/*@ requires logic_square(x) < UINT_MAX;
    requires logic_square(y) < UINT_MAX;
    requires logic_square(x) + logic_square(y) < UINT_MAX;
    ensures \result == logic_square(x) + logic_square(y);
*/
unsigned int sum_of_squares(unsigned int x, unsigned int y) {
    return square(x) + square(y);
}