Система автоматизации доказательства PVS Prover Основные принципы Дерево доказательства Команды доказательства. Пример Система правил вывода – команд provera. - презентация

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

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

3 Дерево доказательства, вершина цель доказательства, дуга шаг доказательства Каждая цель секвент (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 построить полное дерево доказательства

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

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

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

7 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

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

9 Построение (синтез) программы для предиката 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

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

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

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

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

14 Более эффективная версия программы 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

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

16 Алгоритм вычисления целочисленного квадратного корня через двоичное разложение Спецификация: 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

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

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

19 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);

20 Оптимизации программы предиката 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.

21 Синтез программы 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);

22 Трансформация программы 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}} }

23 Трансформация программы 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); } }

24 Трансформация программы 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); } }

25 Преобразования императивной программы 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

26 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

27 Доказательство формул корректности на 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

28 Доказательство формул корректности (пр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

29 Доказательство формул корректности (пр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)

30 Доказательство формул корректности (пр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

31 Теория 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

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

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

34 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, поскольку далее получим нулевое значение

35 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);

36 Представим теорию 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

37 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)

38 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( ).

39 В соответствии с правилом 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))

40 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( )

41 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

42 В программе, находящейся в файле 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 из-за малости числа. Однако при вычислении других функций результат был бы ошибочным.