3. Математические основы 3.3. Матиндукция 5. Построение языка предикатного программирования. Методы доказательства корректности предикатных программ Методы. - презентация

1 3. Математические основы 3.3. Матиндукция 5. Построение языка предикатного программирования. Методы доказательства корректности предикатных программ Методы доказательства корректности рекурсивных программ 6. Язык предикатного программирования Лексемы, предикаты, операторы, выражения, типы, массивы, императивное расширение Примеры Лекция 6 Предикатное программирование

2 3.Математические основы 3.3. Математическая индукция

3 Математическая индукция метод доказательства некоторого утверждения P(n) для всех значений натурального параметра n; n = 0, 1, 2, …. Схема доказательства: Начальный шаг: утверждение P(n) доказывается для n = 0 (база индукции); Индуктивный шаг: утверждение P(n) считается истинным для значения n (индуктивное предположение) и доказывается для значения n + 1. Переменная n называется индукционной переменной. Метод математической индукции базируется на аксиоме индукции: ( P(0) & k.[ P(k) P(k + 1) ] ) n.P(n) (3.2) Обобщения. База индукции может быть отлична от нуля. Шаг индукции может быть отрицательным. Индукционных переменных может быть несколько. Эти и другие особенности учитываются методами полной индукции и структурной индукции

4 Индукционное предположение для полной индукции определяет истинность P(j) для всех j k; используя его требуется доказать P(k + 1). Метод, сочетающий структурную и полную индукцию. На множестве X задан строгий частичный порядок, удовлетворяющий свойству (3.1) обрыва бесконечных убывающих цепей (well-founded partial order) всякое непустое подмножество S имеет минимальный элемент, т.е. S X. (S a S s S. s a). (3.1) Пусть утверждение, которое требуется доказать, есть W(t); t X. Параметр t определяет одну или несколько индукционных переменных. t X. [ ( y X. y t W(y) ) W(t) ] u X. W(u) (3.3)

5 Если элемент t в формуле (3.3) минимальный, то формула (3.3) вырождается в t X. W(t). Это значит, что для минимальных элементов доказательство W(t) надо проводить отдельно, что соответствует начальному шагу классической схемы. Пусть истинное значение предиката (t) определяет набор значений t, составляющих базу индукции, которая, по меньшей мере, должна содержать все минимальные элементы. Тогда формула (3.3) переписывается в виде: t X.( (t) W(t)) & & t X. [ ( y X. (t) & y t W(y) ) W(t) ](3.4) (t) W(t) (t) & y t W(y) W(t)

6 Метод индукции, использующий меру t X. [ ( y X. m(y) < m(t) W(y) ) W(t) ] u X. W(u) (3.5) Функция m: X nat называется мерой Вместо типа nat может использоваться ЧУМ со свойством обрыва бесконечно убывающих цепей (well-founded partial order)

7 5. Построение языка предикатного программирования. Методы доказательства корректности предикатных программ (продолжение )

8 Методы доказательства корректности рекурсивных программ Определения предикатов рекурсивного кольца A 1, A 2,…, A n : A j (x j : y j ) P j (x j ) {K j (x j : y j )} Q j (x j, y j ); j=1…n; n > 0 (3.36) Здесь P j и Q j предусловие и постусловие предиката A j ; x j, y j различающиеся наборы переменных. Индукционные переменные A j (x: y j ) P j (x) {K j (x: y j )} Q j (x, y j ); j=1…n; n > 0 (5.17) Набор x объединяет все наборы x j ; j=1…n. Корректность определений предикатов кольца (5.17): W(x) j=1..n.{ P j (x) ( y j. LS(K j (x: y j ))) & (LS(K i (x: y j )) Q j (x, y j )) } (5.18) V(x) j=1..n.{P j (x) & Q j (x, y j ) LS(K j (x: y j )} (5.19) Правило RR.Induct(t, W) W(t). Правило LR.Induct(t, V) V(t). Индукционное предположение Induct(t, W) u. u t W(u) или Induct(t, W) u. m(u) < m(t) W(u). На значениях набора t определен строгий частичный порядок, удовлетворяющий свойству обрыва бесконечных убывающих цепей. Либо определена мера m(t)

9 Рекурсивное кольцо состоит из единственного определения предиката: A(x: y) P(x) { K(x: y) } Q(x, y)(5.20) Здесь K(x: y) оператор, в котором имеются рекурсивные вызовы предиката A. Формула корректности определения (5.20): W(x) P(x) ( y. LS(K(x: y))) & (LS(K(x: y)) Q(x, y)) Правило RR для (5.20) принимают следующий вид: Правило RR1*. Induct(t,W) & P(x) ( y. LS(K(x: y))) & (LS(K(x: y)) Q(x, y)) Лемма 13. Если правило RR1* истинно, то рекурсивное определение (5.20) корректно. Формула корректности определения (5.20) для серии L принимает вид: V(x) P(x) & Q(x, y) LS(K(x: y))(2) Правила корректности LR для (5.20) принимает вид: Правило LR1. Induct(t, V) & P(x) & Q(x, y) LS(K(x: y)). Лемма 14. Допустим, спецификация [P(x), Q(x, y)] является тотальной, а оператор K(x: y) однозначный. Если правило LR1 истинно, то определение (5.20) корректно.

10 Правило для рекурсивного вызова предиката Пусть имеется рекурсивный вызов предиката A(u: y1) в составе оператора K(x: y) в определении (5.20) предиката A. Для рекурсивного вызова A(u: y1) определим правило: Правило FB3. R(u, x, y1) Less(u, x) & P(u) & Q(u, y1) Предикат Less(u, x) обозначает отношение u x или m(u) < m(x), находящееся в составе предиката Induct(x, V). Лемма 17. Если истинно правило FB3, то истинна следующая формула: Induct(x, V) & R(u, x, y1) LS(A(u: y1)) Доказательство. Пусть истинно Induct(x, V) & R(u, x, y1). Докажем истинность LS(A(u: y1)). Из истинности предиката R по правилу FB3 следует истинность отношения Less(u, x) и формулы P(u) & Q(u, y1). Из истинности Induct(x, V) и Less(u, x) следует истинность формулы V(u) (см. (2)), т.е.: P(u) & Q(u, y) LS(K(u: y)) Из истинности формулы P(u) & Q(u, y1) следует истинность LS(K(u: y1)), т.е. истинна правая часть определения. Следовательно, истинна и LS(A(u: y1)). A(x: y) P(x) { K(x: y) } Q(x, y)(5.20) Induct(t, V) u. m(u) < m(t) V(u)

11 A0(n: f) A1( : c0, c1); A2(n, c0, c1: f) A1( : c0, c1) ConsIntZero( : c0) || ConsIntOne( : c1) A2(n, c0, c1: f) =(n, c0: b); A3(n, c1, b: f) A3(n, c1, b: f) if (b) =(c1: f) else A4(n, c1: f) A4(n, c1: f) -(n, c1: n1); A5(n, n1: f) A5(n, n1: f) A0(n1: f1); (n, f1: f) Подставим A1 A0; преобразуем к функциональному виду. A0(n: f) A2(n, 0, 1: f) A2(n, c0, c1: f) A3(n, c1, n = c0: f) A3(n, c1, b: f) if (b) f =c1 else A4(n, c1: f) A4(n, c1: f) A5(n, n - c1: f) A5(n, n1: f) f = n A0(n1) Подставим A3 A2, а A2 A0, A5 A4. if A0(n: f) if (n = 0) f =1 else A4(n, 1: f) A4(n, c1: f) f = n A0(n - c1) A4 A0, получим программу факториала на языке P3. A0(n: f) if (n = 0) f =1 else f = n A0(n - 1)

12 6. Язык предикатного программирования

13 Лексемы ЛЕКСЕМА ::= ИДЕНТИФИКАТОР | КЛЮЧЕВОЕ-СЛОВО | КОНСТАНТА | ОПЕРАЦИЯ | РАЗДЕЛИТЕЛЬ| МЕТКА ИДЕНТИФИКАТОР ::= ( _ | [:alpha:] ) (_ | [:alnum:])* КЛЮЧЕВОЕ-СЛОВО ::= int | nat | real | inf | nan | char | string | bool | true | false | nil | type | in | subtype | enum | struct | union | array | | set | predicate | lambda | module | measure | import | if | else | for | switch | case | pre | post| or | xor ОПЕРАЦИЯ ::= + | - | * | / | % | ^ | ! | > | ~ | & | | | ? | = | | = | != |

14 Определение предиката ( : ) [ pre ] [ { } ] [post ; ] sign(real x: int s) { if (x>0) s = 1 else if (x = 0) s = 0 else s = -1 } post s = sign(x)

15 Операторы Оператор = присваивания Вызов ([ ]: ) предиката ([ ]: ) Параллельный ||…|| оператор Условный if ( ) операторelse Оператор switch ( ) { выбора case выр 1 : ……………………………. case выр N : default : } Оператор суперпозиции ;…;

16 Выражения ::= | | | ::= + | - | ! | ~ ::= * | / | % | + | - | > | in | > | = | = | != | & | ^ | or | xor ::= | | | | | ( ) | | | | | a & b if (a) b else false a or b if (a) true else b

17 Описания переменных real pi = 3.14, x, y, z; A(real x, y: nat n) { Complex φz; B(x, y: φz); C(φz: n) } A(real x, y: nat n) { B(x, y: Complex φz); C(φz: n) } A(real x, y: nat n) { Complex φz = B(x, y); C(φz: n) }

18 Структура предикатной программы module [( ) ]; Модуль последовательность импорта, описаний типов, глобальных переменных и определений предикатов Области локализации

19 Определения типов type [( )] = ; Базисные типы bool, nat, int, real, char Структурные типы struct (, … ) set ( ) array (, ) predicate ( : ) pre … post … type Complex = struct(real re, im ) ; type Diapason( nat n) = 1..n+1; type Ar( nat n) = array ( real, Diapason(n), 1..5);

20 Алгебраические типы union ( ) ::= [ ( ) ] ::= [ ( ) ] ::= ? [ ( ) ] ::=.

21 Списки Seq(T) = NIL + (T Seq ) type list (type T) = union ( nil, cons (T car, list(T) cdr) ); switch (s) { case nil: 0 case cons(h, t): 1 + length(t) }; list(T) x, y, z; T a; z = a z = x + y z = a + y z = x + y + a x.car x.cdr last(x) len(x) z.car = { CompUnion(z: i, x, y) ; CompStruct(y: u, v); u }

22 Массивы type ar1_5 = array (int, 1..5); ar1_5 squ; squ = for (var i) i*i; ar1_5 r = for (i) i; type Ar(nat k) = array (real, 1..k); F (nat n, Ar(n) x: Ar(n+1) x') { x' = for (var j) { case 1..n : x[j] + 1 case n + 1 : 0 } } type MATR(nat k) = array(real, 1..k, 1..k); perm_lines(nat n, MATR(n) a, nat k, m : MATR(n) a' ) pre 1

23 [ ] ( [ ] ) + ::= [ ] ::=

24 Формулы ФОРМУЛА ::= ЛОГИЧЕСКОЕ-ВЫРАЖЕНИЕ | ( ФОРМУЛА ) | [КВАНТОРНАЯ-ЧАСТЬ] ФОРМУЛА | ! ФОРМУЛА | ФОРМУЛА & ФОРМУЛА | ФОРМУЛА or ФОРМУЛА | ФОРМУЛА -> ФОРМУЛА | ФОРМУЛА ФОРМУЛА ЛОГИЧЕСКОЕ-ВЫРАЖЕНИЕ ::= ВЫРАЖЕНИЕ КВАНТОРНАЯ-ЧАСТЬ ::= ( КВАНТОР СПИСОК-ПОДКВАНТОРНЫХ-ПЕРЕМЕННЫХ ) [КВАНТОРНАЯ-ЧАСТЬ] КВАНТОР ::= ! | ? | forall | exists ! - квантор всеобщности, а ? - квантор существования. СПИСОК-ПОДКВАНТОРНЫХ-ПЕРЕМЕННЫХ ::= [ИЗОБРАЖЕНИЕ-ТИПА [:blank:]] ПОДКВАНТОРНАЯ-ПЕРЕМЕННАЯ (, ПОДКВАНТОРНАЯ-ПЕРЕМЕННАЯ)* ПОДКВАНТОРНАЯ-ПЕРЕМЕННАЯ ::= ИДЕНТИФИКАТОР

25 Императивное расширение операторы перехода и помеченные операторы Для предиката-функции допускается отсутствие результатов ОПЕРАТОР-ИМПЕРАТИВНОГО-РАСШИРЕНИЯ ::= ГРУППОВОЙ-ОПЕРАТОР-ПРИСВАИВАНИЯ | break | ОПЕРАТОР-FOR | ОПЕРАТОР-ЕСЛИ ГРУППОВОЙ-ОПЕРАТОР-ПРИСВАИВАНИЯ ::= | СПИСОК-ПЕРЕМЕННЫХ | = | СПИСОК-ВЫРАЖЕНИЙ | ОПЕРАТОР-FOR ::= for ( ЗАГОЛОВОК-ЦИКЛА ) { ОПЕРАТОР [; ОПЕРАТОР] } ЗАГОЛОВОК-ЦИКЛА ::= [[ИЗОБРАЖЕНИЕ-ТИПА] ПАРАМЕТР-ЦИКЛА = ВЫРАЖЕНИЕ] ; [УСЛОВИЕ-ЗАВЕРШЕНИЯ] ; [ПЕРЕСЧЕТ-ПАРАМЕТРА] ПАРАМЕТР-ЦИКЛА ::= ИДЕНТИФИКАТОР УСЛОВИЕ-ЗАВЕРШЕНИЯ ::= ВЫРАЖЕНИЕ ПЕРЕСЧЕТ-ПАРАМЕТРА ::= ОПЕРАТОР

26 Пример 5.1. Программа умножения через сложение. formula m(nat a: nat) = a; Умн(nat a, b: nat c) pre a 0 & b 0 { if (a = 0) c = 0 else c = b + Умн(a – 1, b) } post c = a b measure m(a); Доказательство корректности. Тотальность спецификации: mult_total: lemma exists c. c = a b; LR1. Induct(t, V) & P(x) & Q(x, y) LS(K(x: y)). Целью является доказательство истинности правила: LR1: Induct(t, V) & a 0 & b 0 & c = a b LS( )). Правила для условного оператора if (C) A(x: y) else B(x: y): Правило FC1.R(x, y) & C LS(A(x: y)) Правило FC2.R(x, y) & C LS(B(x: y)) FC1_mul: lemma Induct(a, V) & a 0 & b 0 & c = a b & a=0 => c =0; Для второй альтернативы формируется цель: FC2_mul: Induct(a, V) & a 0 & b 0 & c = a b & not a=0 LS(c = b + Умн(a – 1, b));

27 FC2_mul: Induct(a, V) & a 0 & b 0 & c = a b & not a=0 LS(c = b + Умн(a – 1, b)); Пусть имеется рекурсивный вызов функции A(u) в определении предиката A: A(x: y) P(x) {… B(u, x, A(u): z)...} Q(x, y) (16) Правило FF3.R(u, x, z) Less(u, x) & P(u) Правило FF4.R(u, x, z) & Q(u, y1) LS(B(u, x, y1: z)) Лемма 36. Допустим, спецификация предиката A является тотальной. Если истинны правила FF3 и FF4, то истинна следующая формула: Induct(x, V) & R(u, x, z) LS(B(u, x, A(u): z)) В соответствии с правилами FF3 и FF4 достаточно доказать две леммы: FF3_mul: lemma a 0 & b 0 & c = a b & not a=0 => m(a - 1) < m(a) & a & b 0; FF4_mul: lemma a 0 & b 0 & c = a b & not a=0 & (a - 1) b = y => c = b + y ;

28 Пример 5.2. Программа D(a, b: c) вычисления наибольшего общего делителя (НОД) положительных a и b. x делитель a divisor(x, a) z 0. x z = a divisor2(с, a, b) divisor(с, a) & divisor(с, b) НОД(c, a, b) divisor2(с, a, b) & x. (divisor2(x, a, b) x c) Свойства НОД: a = b НОД(a, a, b) (5.21) a > b & НОД(c, a, b) НОД(c, a - b, b) (5.22) НОД(c, a, b) НОД(c, b, a) (5.23)

29 D(nat a, b: nat c) pre a 1 & b 1 {if (a = b) c = a else if (a < b) D(a, b-a: c) else D(a-b, b: c) } post НОД(c, a, b) measure a+b; formula m(nat a, b: nat) = a+b; formula P(nat a, b) = a 1 & b 1; Доказательство корректности. Тотальность спецификации: total_НОД: lemma exists c. НОД(c, a, b); Основная цель доказательства: LR1: Induct(V) & P(a, b) & НОД(c, a, b) LS( )). Правила для условного оператора if (C) A(x: y) else B(x: y): Правило FC1.R(x, y) & C LS(A(x: y)) Правило FC2.R(x, y) & C LS(B(x: y)) FC1_gcd: lemma Induct(V) & P(a, b) & НОД(c, a, b) & a = b => c = a; Для второй альтернативы формируется цель: FC2_ gcd : Induct(V) & P(a, b) & НОД(c, a, b) & not a = b LS( if (a < b) D(a, b-a: c) else D(a-b, b: c) );

30 FC2_gcd: Induct(V) & P(a, b) & НОД(c, a, b) & not a = b LS(if (a < b) D(a, b-a: c) else D(a-b, b: c)); В соответствии с правилами FC1 и FC2 формируются две цели: FC1_1: Induct(V) & P(a, b) & НОД(c, a, b) & not a = b & a < b LS(D(a, b-a: c)) ; FC2_1: Induct(V) & P(a, b) & НОД(c, a, b) & not a = b & not a < b LS(D(a-b, b: c)) ; Правило FB3. R(u, x, y1) m(u) < m(x) & P(u) & Q(u, y1) Лемма 17. Induct(x, V) & R(u, x, y1) LS(A(u: y1)) FB3_1: lemma P(a, b) & НОД(c, a, b) & not a = b & a m(a, b-a) < m(a, b) & P(a, b-a) & НОД(c, a, b-a); FB3_2: lemma P(a, b) & НОД(c, a, b) & not a = b & not a m(a-b, b) < m(a, b) & P(a-b, b) & НОД(c, a-b, b);