Система автоматизации доказательства PVS Prover Основные принципы Дерево доказательства Команды доказательства. Пример Система правил вывода – команд provera Автоматизация доказательства программ вычисления целочисленного квадратного корня, целой части вещественного числа и целочисленного двоичного логарифма Лекция 10 Предикатное программирование

Prover -- сочетание в PVS языка логики высокого уровня и мощного автоматического provera -- комплекс средств поддержки построения доказательств в форме, удобной для восприятия, в целях разработки, отладки, анализа и визуализации доказательств -- реализует значительно большую степень автоматизации и большую степень контроля, по сравнению с другими proverами Команды доказательства могут быть скомбинированы в стратегии доказательства. Доказательства можно редактировать запускать вновь. Семантический анализ (Type checking) реализуется посредством автоматического доказательства Proverом истинности условий, называемых type correctness conditions (TCCs)

Дерево доказательства, вершина цель доказательства, дуга шаг доказательства Каждая цель секвент (sequent) состоит из посылок (antecedents) и следствий (consequents) {-1} A 1 {-2} A 2 [-3] A 3 ……… (A 1 & A 2 & A 3 & …) (B 1 B 2 B 3 …) {1} B 1 [2] B 2 {3} B 3 ……….. A 1, A 2, A 3, … B 1, B 2, B 3,… [-3], [2] формулы из родительского секвента, {-1}, {-2}, {1}, {3} новые формулы Корневая вершина цель вида A, где A теорема, которую нужно доказать. Если доказано, что секвент истинный, то ветвь дерева на нем заканчивается. Есть разные правила. Наиболее простое: если одна из посылок ложная, то секвент истинный. Задача provera построить полное дерево доказательства

Пусть имеется секвент A B & C Команда split порождает два секвента-потомка: A B и A C Команда правило (шаг) доказательства Применяемые команды доказательства сохраняются. Команды могут быть введены пользователем или применяться при работе по некоторой стратегии Некоторые команды достаточно гибкие и мощные

Логика PVS -- исчисление секвентов Г, - последовательности формул, A, B – отдельные формулы Структурные правила Пропозиционные правила Правила для равенства Правила для кванторов Правила для IF

Иллюстрация методов верификации и синтеза Построение и верификация быстрых программ для стандартных функций: floor – целая часть плавающего числа, представленного в бинарном формате в соответствии со стандартом IEEE ; isqrt – целочисленный квадратный корень; ilog2 – целочисленный двоичный логарифм. Программы данных стандартных функций на языке C++ используются в отечественной системе спутниковой навигации Навител Навигатор для автомобилей (корпорация Центр Навигационных Технологий).

static const uint32_t small_limit = 17; static const uint32_t small_sqrts[small_limit] = // {0, 1, 1, 2, 2, 2, 2, 3, 3, 3, 3, 3, 3, 4, 4, 4, 4}; #define sqrtBit(k)\ t = s + (1UL

Синтез программы вычисления целочисленного квадратного корня Спецификация isqrt : m = isqrt(x) = floor(sqrt(x)), где z = floor(t) – целая часть вещественного аргумента t со спецификацией t

Построение (синтез) программы для предиката isqrt 1. Необходимо доказать тотальность спецификации, т.е. лемму: Isqrt_total: lemma exists nat m. Isqrt(x, m) 2. Построить оператор S(x: m), реализующий предикат isqrt, и доказать формулу корректности: Isqrt(x, m) LS(S(x: m)). Синтезируем простейшую программу, вычисляющую результат m последовательным перебором с нуля. Применяется метод обобщения исходной задачи isqrt. Рассмотрим задачу sq0, определяемую спецификацией: formula P_sq0(nat x, k) = k^2

formula Isqrt(nat x, m) = m^2

Построение программы для предиката sq0 formula Isqrt(nat x, m) = m^2

Доказательство корректности программы для sq0 formula Isqrt(nat x, m) = m^2

Доказательство корректности программы для sq0 (2) formula Isqrt(nat x, m) = m^2

Более эффективная версия программы isqrt sq0(nat x, k : nat m) pre P_sq0(x, k) { if (x < (k + 1)^2) m = k else sq0(x, k + 1: m) } post Isqrt(x, m); Недостаток вычисление квадрата в (k + 1)^2. (k + 1)^2=p =k^2 + 2* k + 1 Дополнительный параметра n = k^2. Параметр d = 2* k + 1 позволяет заменить умножение сложением. x < (k + 1)^2 эквивалентно x - k^2 < 2* k + 1 Вместо x и n можно перейти к одному параметру y = x - k^2. Соответствующее обобщение задачи sqrt есть предикат sq1: formula P_sq1(nat x, y, k, d) = k^2

Корректность второй версии программы isqrt formula Isqrt(nat x, m) = m^2

Алгоритм вычисления целочисленного квадратного корня через двоичное разложение Спецификация: formula Isqrt(nat n, s) = s^2 0 & n < 2^(2*p); isqrt1(nat n, p: nat s) pre P_sqp(n, p) post Isqrt(n, s); s состоит не более чем из p двоичных цифр !! Значение старшей цифры равно 0, если n < 2^(2*(p-1)) и 1 в противном случае. Алгоритм определяет цифры начиная со старшей и далее. Пусть q очередное приближение для результата s в виде старших двоичных цифр с номерами от p до k+1. Тогда должно выполняться условие q^2

Спецификация обобщающей задачи: formula P_sq2(nat n, p, k, q) = P_sqp(n, p) & k

formula P_sq2(nat n, p, k, q) = P_sqp(n, p) & k

formula e2(nat k: nat) = k; sq2_rec: lemma P_sq2(n, p, k, q) & Isqrt(n, s) (k = 0)? s = q : (n < (q + 2^(k-1))^2)? e2(k-1) < e2(k) & P_sq2(n, p, k-1, q) & Isqrt(n, s) : e2(k-1) < e2(k) & P_sq2(n, p, k-1, q + 2^(k-1)) & Isqrt(n, s) Разработчик должен доказать лемму, а система, используя в качестве шаблонов правила FC и FB3, должна автоматически синтезировать программу: sq2(nat n, p, q, k: nat s) pre P_sq2(n, p, k, q) { if (k = 0) s = q else if ( n < (q + 2^(k-1))^2 ) sq2(n, p, k - 1, q : s) else sq2(n, p, k - 1, q + 2^(k-1) : s) } post Isqrt(n, s);

Оптимизации программы предиката sq2 В выражении q + 2^(k-1) заменим + побитовой операциейor. Чтобы обеспечить корректность такой замены, необходимо доказать лемму: or_eq_plus: lemma k > 0 & k < p & mod(q, 2^k) = 0 & q < 2^p (q or 2^(k - 1)) = q + 2^(k - 1) Необходимое условие mod(q, 2^k) = 0 проще обеспечить включением его в предусловие. Упростить вычисление n < (q + 2^(k-1))^2 (q + 2^(k-1))^2 = q^2 + 2^((k-1)*2) + q * 2^k Тогда условие n < (q + 2^(k-1))^2 эквивалентно: n - q^2 < 2^((k-1)*2) + q * 2^k Обозначим y = n - q^2.

Синтез программы sq3 Синтезируем программу с указанными оптимизациями sq2: formula P_sq3(nat n, p, k, q, y) = P_sq2(n, p, k, q) & y = n - q^2 & mod(q, 2^k) = 0; isqrt1(nat n, p: nat s) pre P_sqp(n, p) { sq3(n, p, p, 0, n: s) } post Isqrt(n, s); sq3(nat n, p, k, q, y: nat s) pre P_sq3(n, p, k, q, y) { if (k = 0) s = q else { nat t = 2^((k-1)*2) + q * 2^k; if (y < t) sq3(n, p, k - 1, q, y: s) else sq3(n, p, k - 1, q or 2^(k-1), y – t : s) } } post Isqrt(n, s);

Трансформация программы isqrt1 Этап 1. Склеивание переменных: sq3: n y; s q; sq3(nat n, p, k, s, n: nat s) { if (k = 0) s = s else { nat t = 2^((k-1)*2) + s * 2^k; if (n < t) sq3(n, p, k – 1, s, n: s) else sq3(n, p, k - 1, s or 2^(k-1), n – t : s) } } Этап 2. Замена хвостовой рекурсии циклом. sq3(nat n, p, k, s, n: nat s) { M: if (k = 0) s = s else { nat t = 2^((k-1)*2) + s * 2^k; if (n < t) { |n, p, k, s, n| = |n, p, k – 1, s, n|; goto M } else {|n, p, k, s, n| = |n, p, k-1, s or 2^(k-1), n - t|; goto M}} }

Трансформация программы isqrt1 (прод1.) Этап 2a. Оформление цикла и раскрытие мульти-присваиваний sq3(nat n, p, k, s, n: s) {for (;;) { if (k = 0) break; nat t = 2^((k-1)*2) + s * 2^k; if (n < t) k = k – 1 else { s = s or 2^(k-1); k = k – 1; n = n – t } } } Этап 2б. Оформление цикла и упрощения sq3(nat n, p, k, s, n: s) { for ( ; k = 0; k = k – 1) { nat t = 2^((k-1)*2) + s * 2^k; if (n >= t) { n = n – t ; s = s or 2^(k-1); } }

Трансформация программы isqrt1 (прод2.) isqrt1(nat n, p: nat s) { sq3(n, p, p, 0, n: s) } Этап 3. Подстановка определения предиката на место вызова isqrt1(nat n, p: nat s) { nat k; |n, p, k, s, n| = |n, p, p, 0, n|; for ( ; k = 0; k = k – 1) { nat t = 2^((k-1)*2) + s * 2^k; if (n >= t) { n = n – t ; s = s or 2^(k-1); } } } Программа на императивном расширении языка P nat n, p; nat s = 0; for (nat k = p ; k = 0; k = k – 1) { nat t = 2^((k-1)*2) + s * 2^k; if (n >= t) { n = n – t ; s = s or 2^(k-1); } }

Преобразования императивной программы nat n, p; nat s = 0; for (nat k = p; k = 0; k = k - 1) { nat t = 2^((k-1)*2) + s * 2^k; if (n >=t) { n = n – t; s = s or 2^(k-1); } } Введем макрос для тела цикла: sq(k) = { t = 2^((k-1)*2) + s * 2^k; if (n >=t) { n = n – t; s = s or 2^(k-1); } } Проведем развертку цикла. Получим: nat n, p; nat s = 0; sq(p); sq(p – 1); …; sq(2); sq(1) Проведем подстановку тела для sq(p) и sq(1). Получим программу, тождественную исходной: sq(k){ t = 2^((k-1)*2) + s * 2^k; if (n >=t) { n = n – t; s = s or 2^(k-1); } } nat n, p; nat s = 0; if (n >= 2^((p-1)*2)) { n = n – 2^((p-1)*2); s = 2^(p-1); } sq(p – 1); …; sq(2); if (n >= s * 2) s = s or 1

static const uint32_t small_limit = 17; static const uint32_t small_sqrts[small_limit] = // {0, 1, 1, 2, 2, 2, 2, 3, 3, 3, 3, 3, 3, 4, 4, 4, 4}; #define sqrtBit(k)\ t = s + (1UL

Доказательство формул корректности на PVS isqrt : THEORY BEGIN IMPORTING fl, bit_nat n, s, x, k, m: VAR nat Isqrt(n, s): bool = s = floor(sqrt(n)) Isqrt_eq: LEMMA Isqrt(n, s) IFF s^2

Доказательство формул корректности (пр1) P_sq1(x, y, k, d: nat): bool = k^2 0 & n < 2^(2*p) P_sq2(n, p, k, q: nat): bool = P_sqp(n, p) & k

Доказательство формул корректности (пр2) sq2_rec: lemma FORALL (n, p, k, q, s: nat): P_sq2(n, p, k, q) & Isqrt(n, s) IMPLIES IF k = 0 THEN s = q ELSIF n < (q + 2^(k-1))^2 THEN e2(k-1) < e2(k) & P_sq2(n, p, k-1, q) & Isqrt(n, s) ELSE e2(k-1) < e2(k) & P_sq2(n, p, k-1, q + 2^(k-1)) & Isqrt(n, s) ENDIF P_sq3(n, p, k, q, y: nat): bool = P_sq2(n, p, k, q) & y = n - q^2 & mod(q, 2^k) = 0 p_2_2: LEMMA (2^p)^2 = 2^(2*p) Isqrt3_fb1: LEMMA P_sqp(n, p) & Isqrt(n, s) IMPLIES P_sq3(n, p, p, 0, n) & Isqrt(n, s)

Доказательство формул корректности (пр3) k2_1: LEMMA k > 0 IMPLIES 2 * 2^(k-1) = 2^k sq3_rec: lemma FORALL (n, p, k, q, y, s, t: nat): P_sq3(n, p, k, q, y) & Isqrt(n, s) IMPLIES IF k = 0 THEN s = q ELSE t = 2^((k-1)*2) + q * 2^k IMPLIES IF y < t THEN e2(k-1) < e2(k) & P_sq3(n, p, k - 1, q, y) & Isqrt(n, s) ELSE e2(k-1) < e2(k) & P_sq3(n, p, k - 1, bit_or(p, q, 2^(k-1)), y - t) & Isqrt(n, s) ENDIF END isqrt

Теория bit_nat bit_nat: THEORY BEGIN IMPORTING fl bit_or(n: posnat, a, b: below(exp2(n))): below(exp2(n)) = bv2nat[n](nat2bv[n](a) OR nat2bv[n](b)) concat_or: LEMMA FORALL (n, m: nat, x, z: bvec[n], y, t: bvec[m]): ((x o y) OR (z o t)) = ((x OR z) o (y OR t)) bvcomp: LEMMA FORALL (n, k: posnat, a: below(exp2(n))): k

Итоги В процессе верификации обнаружено 5 ошибок. Из них 4 чисто технические. Принципиальная ошибка: результат функции floor не помещается в отведенные для него 32 бита. Затраты на доказательство формул корректности в системе PVS примерно в 5 раз больше времени обычного программирования. 30% – время доказательства собственно формул корректности 70% – время доказательства дополнительных лемм Среди более десятка работ по верификации и синтезу isqrt имеется лишь одна работа, в которой верифицируется алгоритм isqrt сравнимой эффективности. Новая версия языка предикатного программирования языка P Учебное пособие по предикатному программированию для студентов НГУ Система предикатного программирования.

Алгоритм вычисления целой части плавающего числа formula flp(real x, int i) = i

const nat p, bias, w, m; const nat m = p + w; type bit = {nat a | a = 0 or a = 1}; type intm = {int x | - 2^(m-1) < x & x < 2^(m-1)}; formula val(bit S, nat E, T) = (-1)^S * 2^(E - bias) * (1 + 2^(1 - p) * T); floor(bit S, nat E, T: intm y) pre T < 2^(p-1) post flp(val(S, E, T), y); val(bit S, nat E, T) = (-1)^S * 2^(E – bias – p + 1) * (2^(p-1) + T) = sg 2^d z; sg= (-1)^S; sg = 1 or sg = -1 & d = E – bias – p + 1 & z = 2^(p-1) + T & z >= 2^(p-1) d = 0 => y = z * sg d > 0 => сдвиг вправо, однако d не может быть больше 7; сдвиг на 8 дает отрицательное целое. d сдвиг влево, но не дальше, чем на 23, поскольку далее получим нулевое значение

const nat p, bias, w, m; const nat m = p + w; type bit = {nat a | a = 0 or a = 1}; type intm = {int x | - 2^(m-1) < x & x < 2^(m-1)}; floor(bit S, nat E, T: intm y) pre T < 2^(p-1) & E – bias – p + 1 < w { floor1(S, E – bias – p + 1, 2^(p-1) + T: y) } post flp(val(S, E, T), y); val1(bit S, nat d, z) = (-1)^S * 2^d z; floor1(bit S, nat d, z: intm y) pre z >= 2^(p-1) & z < 2^p & d < w { if (S = 0) if (d >= 0) y = 2^d * z else y = div(z, 2^(-d)) else if (d >= 0) y = - 2^d * z else if (mod(z, 2^(-d)) = 0) y = - div(z, 2^(-d)) else y = - div(z, 2^(-d)) – 1 } post flp(val1(S, d, z), y);

Представим теорию main для определения предиката floor. main: THEORY BEGIN IMPORTING fl p, bias, w, m: nat %constants m: nat = p + w nbit: TYPE = {n: nat | n = 0 OR n = 1} x: VAR real intm: TYPE = {x | - 2^(m-1) < x & x < 2^(m-1)} y: VAR intm S: VAR nbit E, T, d, z: VAR nat val(S, E, T) = (-1)^S * 2^(E - bias) * (1 + 2^(1 - p) * T) val1(S, d, z) = (-1)^S * 2^d * z END main

floor_val: THEORY BEGIN IMPORTING main, floor1 y: VAR intm E, T: VAR nat S: VAR nbit P_floor(E, T): bool = T < 2^(p-1) & E – bias – p + 1 < w Q_floor(S, E, T, y): bool = flp(val(S, E, T), y) satisfy_spec: LEMMA P_floor(E, T) IMPLIES EXISTS y: Q_floor(S, E, T, y) Целью является доказательство истинности правила: P_floor(E, T) & Q_floor(S, E, T, y) LS(floor1(S, E – bias – p + 1, 2^(p-1) + T)) В соответствии с правилом FB1 генерируется лемма: FB1: LEMMA P_floor(E, T) & Q_floor(S, E, T, y) IMPLIES P_floor1(E – bias – p + 1, 2^(p-1) + T) & Q_floor1(S, E – bias – p + 1, 2^(p-1) + T, y)

floor1(bit S, nat d, z: intm y) pre z >= 2^(p-1) & z < 2^p & d < w { if (S = 0) if (d >= 0) y = 2^d * z else y = div(z, 2^(-d)) else if (d >= 0) y = - 2^d * z else if (mod(z, 2^(-d)) = 0) y = - div(z, 2^(-d)) else y = - div(z, 2^(-d)) – 1 } post flp(val1(S, d, z), y); Представим начальную часть теории floor1. floor1: THEORY BEGIN IMPORTING main y: VAR intm E, T, d, z: VAR nat S: VAR nbit P_floor1(d, z): bool = z >= 2^(p-1) & z < 2^p & d < w Q_floor1(S, d, z, y): bool = flp(val1(S, d, z), y) satisfy_spec: LEMMA P_floor1(d, z) IMPLIES EXISTS r: Q_floor1(S, d, z, y) Целью является доказательство истинности правила: FB1: P_floor1(d, z) & Q_floor1(S, d, z, y) LS( ).

В соответствии с правилом FC1 для первой альтернативы условного оператора генерируется цель: FC1: P_floor1(d, z) & Q_floor1(S, d, z, y) & S = 0 LS( ) В соответствии с правилом FC1 для первой альтернативы первого условного оператора генерируется лемма: FC1: LEMMA P_floor1(d, z) & Q_floor1(S, d, z, y) & S = 0 & & d > 0 IMPLIES y = 2^d * z В соответствии с правилом FC2 для второй альтернативы первого условного оператора генерируется лемма: FC2: LEMMA P_floor1(d, z) & Q_floor1(S, d, z, y) & S = 0 & & NOT d > 0 IMPLIES y = div(z, 2^(-d))

else if (d >= 0) y = - 2^d * z else if (mod(z, 2^(-d)) = 0) y = - div(z, 2^(-d)) else y = - div(z, 2^(-d)) – 1 В соответствии с правилом FC2 для второй альтернативы условного оператора генерируется цель: FC2: P_floor1(d, z) & Q_floor1(S, d, z, y) & NOT S = 0 LS( ) В соответствии с правилом FC1 для первой альтернативы второго условного оператора генерируется лемма: FC11: LEMMA P_floor1(d, z) & Q_floor1(S, d, z, y) & NOT S = 0 & d >= 0 IMPLIES y = - 2^d * z В соответствии с правилом FC2 для второй альтернативы второго условного оператора генерируется цель: FC2: P_floor1(d, z) & Q_floor1(S, d, z, y) & NOT S = 0 & NOT d > 0 LS( )

else if (mod(z, 2^(-d)) = 0) y = - div(z, 2^(-d)) else y = - div(z, 2^(-d)) – 1 В соответствии с правилом FC1 для первой альтернативы третьего условного оператора генерируется лемма: FC12: LEMMA P_floor1(d, z) & Q_floor1(S, d, z, y) & NOT S = 0 & NOT d > 0 & mod(z, 2^(-d)) = 0 IMPLIES y = - div(z, 2^(-d)) В соответствии с правилом FC2 для второй альтернативы третьего условного оператора генерируется лемма: FC21: LEMMA P_floor1(d, z) & Q_floor1(S, d, z, y) & NOT S = 0 & NOT d >= 0 & NOT mod(z, 2^(-d)) = 0 IMPLIES y = - div(z, 2^(-d)) – 1

В программе, находящейся в файле fast_floor.cpp обнаружено две ошибки: 1. При E – bias >= m – 2 (или d >= w) сдвигаемое влево значение выходит за пределы m – 1 битов. В частности, при d = w старшая единица попадает в позицию знака в представлении целого числа, в результате чего результат floor становится отрицательным. В реализации следовало бы запретить использовать функцию floor при d > 0, т.е. при E – bias – p + 1 > 0 из-за экспоненциально растущей погрешности. 2. Ненормализованное сверхмалое число обрабатывается также, как нормализованное (с добавление 1 в разряд p). Тем не менее, это не меняет значение функции floor из-за малости числа. Однако при вычислении других функций результат был бы ошибочным.