Однозначность предикатов Однозначность предикатов рекурсивного кольца Теорема об однозначности предикатов 4. Система правил доказательства корректности. - презентация

1 Однозначность предикатов Однозначность предикатов рекурсивного кольца Теорема об однозначности предикатов 4. Система правил доказательства корректности программы Правила для однозначной спецификации Правила для общего случая Правила декомпозиции доказательства для однозначной спецификации Правила декомпозиции доказательства для общего случая Задачи верификации и синтеза 5. Построение языка предикатного программирования. Методы доказательства корректности предикатных программ Язык P1: подстановка определения предиката на место вызова Язык P2: оператор суперпозиции и параллельный оператор общего вида Язык P2: другое обобщение оператора суперпозиции Язык P3: выражения Лекция 5 Предикатное программирование

2 Пусть рекурсивный предикат D(z: u) принадлежит кольцу (3.36), т.е. D = A j для некоторого j. Логическая семантика предиката D определяется следующим образом: LS(D(z: u)) (z, u) pr(j, m 0 G m ) (3.40) Систему (3.36) определений кольца предикатов запишем в векторном виде: A K(A), где A = (A 1, A 2,…, A n ), K = (K 1, K 2,…, K n ). Определим цепь векторов предикатов {A m } m 0 : A 0 Ф, A m+1 K(A m ), m 0, (3.41) где Ф (F, F, …, F) вектор тотально ложных предикатов. Цепь {A m } m 0 соответствует цепи (3.39) вектор-графиков {G m } m 0, поскольку G m = (Gr(A m 1 ), Gr(A m 2 ),…, Gr(A m n )). G 0 =, G m+1 = V(G m ), m 0 (3.39) A i (x i : y i ) K i (x i : y i ); i = 1…n; n > 0, (3.36)

3 Рекурсивное кольцо предикатов представим в виде: A K(A 1, A 2,…, A n, E 1, E 2,…, E s ) (3.42) E 1, E 2,…, E s, s > 0, предикаты, используемые в правых частях определений (3.36), но не принадлежащих данному кольцу. Лемма Пусть предикаты E 1, E 2,…, E s, используемые в системе (3.42), обладают свойством согласованности. Тогда рекурсивные предикаты A 1, A 2,…, A n кольца (3.42) обладают свойством согласованности.

4 3. Язык исчисления вычислимых предикатов (продолжение 3)

5 Однозначность предикатов Лемма Оператор суперпозиции (3.16), параллельный оператор (3.19) или условный оператор (3.20) является однозначным, если вызываемые в операторе предикаты B и C являются однозначными. Лемма Пусть имеется рекурсивное кольцо предикатов (3.42). Кроме рекурсивных предикатов A 1, A 2,…,A n в правых частях определений кольца предикатов используются предикаты E 1, E 2,…, E s. Предположим, что предикаты E 1, E 2,…, E s являются однозначными. Если аргумент определения кольца имеет предикатный тип, то предикат, являющийся значением аргумента, считается однозначным. Тогда рекурсивные предикаты A 1, A 2,…,A n кольца (3.42) являются однозначными. Доказательство. Из-за ограничений на сложные формы рекурсии предикат, являющийся значением аргумента, не может входить в кольцо предикатов. Поэтому можно считать, что такой предикат находится среди E 1, E 2,…, E s. A K(A 1, A 2,…, A n, E 1, E 2,…, E s ) (3.42)

6 Пусть D(u: v) рекурсивный предикат кольца, т.е. D = A j для некоторого j. Допустим, истинны D(u: v1) и D(u: v2). Необходимо доказать, что v1 = v2. В соответствии с леммой 3.13 существует m, при котором D m (u: v1) и D m (u: v2) истинны. Поэтому достаточно доказать, каждый элемент A m цепи {A m } m 0, определенной в (3.41), является вектором однозначных предикатов. Доказательство проводится индукцией по m. Элемент A 0 является вектором однозначных предикатов, поскольку тотально ложный предикат F является однозначным. Допустим, по индуктивному предположению, A m-1 является вектором однозначных предикатов. Докажем это свойство для A m. В правой части каждого определения из A m используется оператор суперпозиции, параллельный оператор или условный оператор. Вызываемые предикаты в правой части: A m-1 1, A m-1 2,…, A m-1 n и E 1, E 2,…, E s однозначны. Однозначность компонент A m следует из леммы Базисные предикаты ConsPred и ConsArray не являются однозначными. В двух разных исполнениях вызова ConsPred(x, B: A) (при совпадающих x и B) в качестве значения переменной A будут получены разные имена.

7 Лемма Вызов C(…), где C переменная предикатного типа, является однозначным, если для каждого вызова конструктора ConsPred(x, B: A) или ConsArray(x, B: A) предикат B является однозначным. Теорема 3.2. Допустим, всякий базисный предикат языка CCP, кроме ConsPred и ConsArray, является однозначным. Пусть имеется программа на языке CCP, и ее исполнение реализуется вызовом предиката D(u: v), причем в наборе v нет переменных предикатного типа. Тогда предикат D является однозначным. Доказательство. Сначала доказательство проводится для программы, в которой нет переменных предикатного типа. Рассмотрим случай, когда программа не содержит рекурсивно определяемых предикатов. Если предикат D базисный, то его однозначность гарантируется условием теоремы. Пусть предикат D имеет определение в виде оператора суперпозиции, параллельного оператора или условного оператора. В соответствии с леммой 3.17 достаточно установить однозначность предикатов B и C, вызываемых в правой части определения. Если эти предикаты базисные, то их однозначность является условием теоремы. Если один из них определяемый, то его полное замкнутое определение программа меньшего размера. Далее по индукции.

8 Имеется рекурсивных дерево колец (теорема 3.1). Для колец, являющихся листьями, однозначность следует из леммы Применяется индукция по длине пути в дереве колец. Доказательство легко обобщается для случая, когда в программе имеются переменные предикатного типа, а их значения однозначные предикаты. Допустим, в программе П имеются переменные предикатного типа. Обозначим через SUBS(П) набор предикатов, являющийся объединением множеств заместителей для всех переменных предикатного типа в программе П. Для набора предикатов M из П обозначим через П[M] минимальную программу, являющуюся частью П и содержащую определения предикатов набора M. Пусть П 0 = П, П j+1 = П j [SUBS(П j )], j=0, 1, 2, …. В теореме 3.1 доказано, что для некоторого k программа П k, а П k+1 =. Программа П k не содержит переменных предикатного типа. Однозначность предикатов программы П k доказана выше. Тогда предикаты B 1, B 2,…, B n, входящие в SUBS(П k-1 ), являются однозначными. В соответствии с леммой 3.19 любой вызов вида C(…) в программе П k-1, где C переменная предикатного типа, является однозначным. Доказательство теоремы, представленное выше, обобщается для программы П k-1, поскольку согласно принятым ограничениям вызов вида C(…) не может участвовать в рекурсии. Доказательство теоремы для произвольной программы П i, i = k-1, …, 0, проводится по индукции.

9 4. Система правил доказательства корректности операторов 4.1. Правила для однозначной спецификации

10 Предикат B(x, y) корректен относительно [P B (x), Q B (x, y)], если: P(x) [L k (x, y) Q(x, y)] & y. L k (x, y) (2.5) P(x) [LS(B(x, y)) Q(x, y)] & y. LS(B(x, y) (4.1) Corr(B, P, Q) (4.1) Правила для корректного оператора Лемма 4.3. Пусть имеется оператор B со спецификацией в виде тройки Хоара {P B (x)} B {Q B (x, y)}. Предполагается, что оператор B является корректным Тогда истинны следующие правила вывода: Правило E1. P B (x) y. Q B (x, y) Правило E2. P B (x) y. LS(B(x, y)) Правило E3. P B (x) LS(B(x, y)) Q B (x, y)

11 Теорема 2.1 тождества спецификации и программы P(x) { S (x, y) k } Q(x, y) (2.1) Оператор S(x, y) является однозначным, а спецификация [P(x), Q(x, y)] тотальной. Пусть истина формула: P(x) & Q(x, y) LS(S(x, y))(4.6) Тогда программа (2.1) является корректной. Лемма 2.8. В условиях теоремы 2.1 истинна ф-ла: P(x) (LS(S(x, y)) Q(x, y)) Лемма 2.9. Допустим, программа (2.1) является корректной, а ее спецификация однозначной. Тогда истинна формула (4.6), т.е. LS(S(x, y)) выводима из спецификации.

12 Правила для параллельного оператора {P(x)} A || B {Q(x, y, z)}(4.17) {P A (x)} A {Q A (x, y)}, {P B (x)} B {Q B (x, z)} Правило LP1. P(x) P B (x) P C (x) Правило LP2. P(x) & Q(x, y, z) Q A (x, y). Правило LP3.P(x) & Q(x, y, z) Q B (x, z). Лемма Пусть спецификация параллельного оператора (4.17) реализуема, операторы A и B однозначны в области предусловий и корректны, а их спецификации однозначны. Если правила LP1, LP2 и LP3 истинны, то параллельный оператор (4.17) является корректным. Доказательство. Операторы A и B однозначны оператор (4.17) однозначный. Поскольку спецификация оператора (4.17) реализуема, в соответствии с теоремой 2.1 достаточно доказать: P(x) & Q(x, y, z) LS(A || B)(x, y, z) LS(A || B)(x, y, z) LS(A)(x, y) LS(B)(x, z) (4.2) Пусть истинны P(x) и Q(x, y, z). Докажем истинность LS(A)(x, y) и LS(B)(x, z). Из истинности предусловия P(x) по правилу LP1 следует истинность P A (x) и P B (x). По правилам LP2 и LP3 становятся истинными Q A (x, y) и Q B (x, z). Для предикатов A и B выполняются условия леммы 2.9. Поэтому истинны формулы: P A (x) & Q A (x, y) LS(A)(x, y) P B (x) & Q B (x, z) LS(B)(x, z) Посылки этих формул истинны истинны LS(A)(x, y) и LS(B)(x, z).

13 Правила для оператора суперпозиции {P(x)} A; B {Q(x, y)}(4.18) {P A (x)} A {Q A (x, z)}, {P B (z)} B {Q B (z, y)} Правило LS1. P(x) P A (x) Правило LS2. P(x) & Q(x, y) & Q A (x, z) P B (z) & Q B (z, y) Лемма Пусть спецификация оператора суперпозиции (4.18) реализуема, операторы A и B однозначны в области предусловий и корректны, а их спецификации однозначны. Если правила LS1 и LS2 истинны, то оператор суперпозиции (4.18) является корректным. Доказательство. Поскольку операторы A и B однозначны, то и оператор суперпозиции (4.18) является однозначным. В соответствии с теоремой 2.1 для доказательства леммы достаточно доказать истинность формулы: P(x) & Q(x, y) LS(A; B)(x, y) LS(A; B)(x, y) z.(LS(A)(x, z) LS(B)(z, y)) (4.1)

14 Пусть истинны P(x) и Q(x, y). Докажем истинность z.(LS(A)(x, z) LS(B)(z, y)). Из истинности предусловия P(x) по правилу LS1 следует истинность P A (x). Из корректности оператора A по правилу E2 следует истинность формулы z. LS(A)(x, z). Допустим для некоторого z 0 истинно LS(A)(x, z 0 ). Для оператора A истинны условия леммы 2.8. Поэтому истинно Q A (x, z 0 ). В соответствии с правилом LS2 истинна формула P B (z 0 ) & Q B (z 0, y). В соответствии с леммой 2.9 истинна формула P B (z) & Q B (z, y) LS(B)(z, y) Тогда истинна LS(B)(z 0, y). В итоге, будет истинна формула z.(LS(A)(x, z) LS(B)(z, y)).

15 Правила для условного оператора {P(x)} if (C) A else B {Q(x, y)}(4.19) {P A (x)} A {Q A (x, y)}, {P B (x)} B {Q B (x, y)} Правило LC1. P(x) & Q(x, y) & C P A (x) Q A (x, y) Правило LC2. P(x) & Q(x, y) & C P B (x) Q B (x, y) Лемма Пусть спецификация условного оператора (4.19) реализуема, операторы A и B однозначны в области предусловий и корректны, а их спецификации однозначны. Если правила LC1 и LC2 истинны, то условный оператор (4.19) является корректным. Доказательство. Поскольку операторы A и B однозначны, то и условный оператор (4.19) является однозначным. В соответствии с теоремой 2.1 для доказательства леммы достаточно доказать: P(x) & Q(x, y) LS( if (C) A else B ) (x, y) LS(if (C) A else B)(x, y) (C LS(A)(x, y)) ( C LS(B)(x, y)) (4.3)

16 Пусть истинны P(x) и Q(x, y). Докажем истинность формулы C LS(A)(x, y). Пусть истинно C. Докажем истинность LS(A)(x, y). Можно применить правило LC1, поскольку истинны P(x), Q(x, y) и C. Получим истинность формулы P A (x) Q A (x, y). В соответствии с леммой 2.9 истинна формула P A (x) Q A (x, y) LS(A)(x, y) Поскольку истинна посылка, то истинно LS(A)(x, y). Следовательно, доказана истинность формулы C LS(A)(x, y). Истинность формулы C LS(B)(x, y) доказывается аналогично.

17 4. Система правил доказательства корректности программы 4.2. Правила для общего случая

18 Правила для параллельного оператора {P(x)} A || B {Q(x, y, z)} (4.11) {P A (x)} A {Q A (x, y)}, {P B (x)} B {Q B (x, z)} Правило RP1. P(x) P A (x) P B (x) Правило RP2. Q A (x, y), Q B (x, z) Q (x, y, z) Лемма 4.4. Пусть предусловие P(x) истинно. Допустим, операторы A и B корректны. Если правила RP1 и RP2 истинны (т.е. правая часть доказуема из левой части для каждого правила), то параллельный оператор (4.11) является корректным. Доказательство. В соответствии с формулой (4.1) достаточно доказать реализуемость LS(A || B) и выводимость постусловия Q(x, y, z) из LS(A || B). LS(A || B) (x, y, z) LS(A)(x, y) LS(B)(x, z).

19 Из истинности предусловия P(x) по правилу RP1 следует истинность P A (x) и P B (x). Далее, по правилу E2 становятся истинными формулы y. LS(A)(x, y) и z. LS(B)(x, z). Их конъюнкция определяет реализуемость LS(A || B)(x, y, z). Докажем выводимость постусловия Q(x, y, z) из LS(A)(x, y) LS(B)(x, z). Допустим, истинна LS(A)(x, y) LS(B)(x, z). Применим правило E3 для P A (x) и P B (x), истинность которых определена выше. Получаем истинность формул LS(A)(x, y) Q A (x, y) и LS(B)(x, z) Q B (x, z). Как следствие, будут истинны Q A (x, y) и Q B (x, z). Применяя правило RP2, получаем истинность постусловия Q(x, y, z).

20 Правила для оператора суперпозиции {P(x)} A; B {Q(x, y)}(4.12) {P A (x)} A {Q A (x, z)},{P B (z)} B {Q B (z, y)} Правило RS1. P(x) P A (x) z (Q A (x, z) P B (z)) Правило RS2. P(x) & z (Q A (x, z) & Q B (z, y)) Q(x, y) Лемма 4.5. Пусть предусловие P(x) истинно. Допустим, операторы A и B корректны. Если правила RS1 и RS2 истинны, то оператор суперпозиции (4.12) является корректным. Доказательство. В соответствии с формулой (4.1) достаточно доказать реализуемость LS(A; B)(x, y) и выводимость постусловия Q(x, y) из LS(A; B)(x, y). LS(A; B)(x, y) z.(LS(A)(x, z) LS(B)(z, y)).

21 Из истинности предусловия P(x) по правилу RS1 следует истинность формул P A (x) и z (Q A (x, z) P B (z)). Из истинности P A (x) и правила E2 следует истинность формулы z. LS(A)(x, z). Допустим для некоторого z 0 формула LS(A)(x, z 0 ) истинна. Из истинности P A (x) и правила E3 следует истинность LS(A)(x, z 0 ) Q A (x, z 0 ). Как следствие, истинно Q A (x, z 0 ). Далее, из истинности формулы z (Q A (x, z) P B (z)) следует истинность P B (z 0 ). По правилу E2 истинна формула y LS(B)(z 0, y). Далее, истинна конъюнкция LS(A)(x,z 0 ) & y LS(B)(z 0, y), и затем формула y. z. (LS(A)(x, z) & LS(B)(z, y)), т.е. доказана реализуемость LS(A; B)(x, y).

22 Докажем выводимость постусловия Q(x, y) из LS(A; B)(x, y). Пусть LS(A; B)(x, y) истинно, т.е. истинна формула z.(LS(A)(x, z) LS(B)(z, y)). Пусть формула истинна для некоторого z 1. По правилу E3 истинна формула LS(A)(x, z 1 ) Q A (x, z 1 ) и далее Q A (x, z 1 ). Истинность Q A (x, z 1 ) и z (Q A (x, z) P B (z)) влечет истинность P B (z 1 ). По правилу E3 истинно LS(B)(z 1, y) Q B (z 1, y). Поскольку LS(B)(z 1, y) истинно, то истинно Q B (z 1, y). Таким образом, истинна правая часть правила RS2, а значит и левая, т.е. истинно постусловие Q(x, y).

23 Правила для условного оператора {P(x)} if (C) A else B {Q(x, y)}(4.13) {P A (x)} A {Q A (x, y)}, {P B (x)} B {Q B (x, y)} Правило RC1. P(x) C P A (x) Правило RC2. P(x) C P B (x) Правило RC3. P(x) & C & Q A (x, y) Q(x, y) Правило RC4. P(x) & C Q B (x, y) Q(x, y) Лемма 4.6. Пусть предусловие P(x) истинно. Допустим, операторы A и B корректны. Если правила RC1, RC2, RC3 и RC4 истинны, то условный оператор (4.13) является корректным. Доказательство. Для оператора (4.13) необходимо доказать формулу (2.10). В ней дважды встречается подформула LS(if (C) A else B)(x, y), определяемая в виде: (C LS(A)(x, y)) ( C LS(B)(x, y))(4.14) Достаточно доказать реализуемость формулы (4.14) и выводимость постусловия Q(x, y) из (4.14).

24 Допустим, что условие C истинно. Из истинности предусловия P(x) по правилу RC1 следует истинность P A (x). По правилу E2 истинна формула y. LS(A)(x, y). Далее будет истинной формула y. (C LS(A)(x, y)). Из истинности C следует истинность формулы C LS(B)(x, y), и следовательно, формулы y. [(C LS(A)(x, y)) & ( C LS(B)(x, y))]. Это обеспечивает реализуемость формулы (4.14) в случае истинности C. Реализуемость (4.14) в случае ложности C доказывается аналогичным образом. Докажем выводимость постусловия Q(x, y) из формулы (2.14). Допустим, истинна формула (4.14). Пусть C истинно. Тогда истинно LS(A)(x, y). По правилу RC1 истинно P A (x). По правилу E3 истинна формула LS(A)(x, y) Q A (x, y), а значит и Q A (x, y). Таким образом, истинна правая часть правила RC3. Тогда истинна левая часть правила, т.е. истинно постусловие Q(x, y). Доказательство истинности постусловия Q(x, y) для случая, когда C ложно, проводится аналогично с использованием правила RC4.

25 4. Система правил декомпозиции доказательства корректности операторов 4.3. Правила для однозначной спецификации

26 Правила для параллельного оператора Для параллельного оператора A(x: y) || B(x: z) определим правила: Правило FP1.R(x, y, z) LS(A(x, y)) Правило FP2.R(x, y, z) LS(B(x, z)) Лемма 7. Если истинны правила FP1 и FP2, то истинна формула: R(x, y, z) LS(A(x: y) || B(x: z)) Доказательство. Формула LS(A(x: y) || B(x: z)) эквивалентна LS(A(x: y)) LS(B(x: z)). Поэтому достаточно доказать истинность двух формул: R(x, y, z) LS(A(x: y)) R(x, y, z) LS(B(x: z)) Эти формулы эквивалентны правилам FP1 и FP2. P(x) & Q(x, y) LS(S(x, y))(4.6)

27 Правила для условного оператора Для условного оператора 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)) Лемма 9. Если истинны правила FC1 и FC2, то истинна следующая формула: R(x, y) LS(if (C) A(x: y) else B(x: y)) Доказательство. Формула LS(if (C) A(x: y) else B(x: y)) эквивалентна (C LS(A(x: y))) ( C LS(B(x: y))) Таким образом, требуется доказать истинность: R(x, y) (C LS(A(x: y))) ( C LS(B(x: y))) Последняя формула эквивалентна конъюнкции формул: R(x, y) (C LS(A(x: y))) R(x, y) ( C LS(B(x: y))) А эти формулы эвивалентны правилам FC1 и FC2.

28 Правила для оператора суперпозиции Для оператора суперпозиции A(x: z); B(x, z: y) определим правила: более общего вида Правило FS1.R(x, y) z. LS(A(x: z)) Правило FS2.R(x, y) & LS(A(x: z)) LS(B(x, z: y)) Лемма 3. Если истинны правила FS1 и FS2, то истинна следующая формула: R(x, y) LS(A(x: z); B(x, z: y)) Доказательство. Формула LS(A(x: z); B(x, z: y)) эквивалентна z.(LS(A(x: z)) LS(B(x, z: y))). Пусть истинно R(x, y). Докажем истинность z.(LS(A(x: z)) LS(B(x, z: y))). По правилу FS1 истинна формула z. LS(A(x: z)). Допустим для некоторого z0 истинно LS(A(x: z0)). По правилу FS2 истинна формула LS(B(x, z0: y)). В итоге, будет истинна формула z.(LS(A(x: z)) LS(B(x, z: y))). позиция квантора существования вхождение LS(…) в левой части

29 Правила для нерекурсивного вызова Пусть имеется нерекурсивный вызов предиката A(x: y) со спецификацией: {P(x)} A(x: y) {Q(x, y)} (3) Для нерекурсивного вызова предиката A(x: y) определим правило: Правило FB1.R(x, y) P(x) & Q(x, y) Лемма 15. Допустим, нерекурсивный вызов предиката A(x: y) является корректным, а его спецификация (3) однозначна. Если истинно правило FB1, то истинна следующая формула: R(x, y) LS(A(x: y)) Доказательство. Пусть истинно R(x, y). Докажем истинность LS(A(x: y)). Поскольку истинна правая часть правила FB1, то истинна формула P(x) & Q(x, y) в правой части. В соответствии с леммой 2.9 истинна формула P(x) & Q(x, y) LS(A(x: y)) и, следовательно, LS(A(x: y)).

30 4. Система правил декомпозиции доказательства корректности операторов 4.4. Правила для общего случая

31 Декомпозиция для параллельного оператора {P(x)} B(x: y) {Q(x, y)} Corr(B, P, Q) P(x) [LS(B(x, y)) Q(x, y)] & y. LS(B(x, y) (4.1) {P(x)} A(x: y) || B(x: z) {Q(x, y, z)} Q(x, y, z) Q1(x, y) & Q2(x, z) Лемма. Corr(A(x: y) || B(x: z), P, Q) = Corr(A(x: y), P, Q1) & Corr(B(x: z), P, Q2)

32 Декомпозиция для условного оператора {P(x)} B(x: y) {Q(x, y)} Corr(B, P, Q) P(x) [LS(B(x, y)) Q(x, y)] & y. LS(B(x, y) (4.1) {P(x)} if (C) A(x: y) else B(x: y) {Q(x, y)} Лемма. Corr(if (C) A(x: y) else B(x: y), P, Q) = Corr(A(x: y), P & C, Q) & Corr(B(x: y), P & C, Q)

33 Декомпозиция для оператора суперпозиции Рассмотрим спецификацию оператора суперпозиции в виде тройки Хоара: {P(x)} A; B {Q(x, y)}.(2.12) Предположим, что оператор A коррекетн. Спецификация представлены тройками: {PA(x)} A {QA(x, z)}, Определим правила, гарантирующие корректность оператора суперпозиции (2.12). Правило RS17.P(x) PA(x) z (QA(x, z) y LS(B)(z, y)). Правило RS18.P(x) & z (QA(x, z) & LS(B)(z, y)) Q(x, y). Лемма 2.5. Пусть предусловие P(x) истинно. Допустим, оператор A корректен. Если правила RS1 и RS2 истинны, то оператор суперпозиции (2.12) является корректным.

34 Задачи верификации и синтеза на примере оператора суперпозиции A(x: y) pre P(x) { B(x: z); C(z: y) } post Q(x, y) (3) Операторы B(x: z) и C(z: y) корректны относительно своих спецификаций [P B (x), Q B (x, z)] и [P C (z), Q C (z, y)]. Спецификация [P(x), Q(x, y)] тотальна. Корректность предиката A гарантируется в случае истинности правил: Правило LS1. P(x) P B (x) Правило LS2. P(x) & Q(x, y) & Q B (x, z) P C (z) & Q C (z, y) Задача дедуктивной верификации Задача программного синтеза: требуется построить программу предиката A, представленного тотальной спецификацией [P(x), Q(x, y)]. Пусть для некоторых предикатов P B (x), Q B (x, z), P C (z) и Q C (z, y) доказана истинность правил LS1 и LS2. Тогда синтезируем программу (3). Корректность оператора S(x: y) относительно однозначной и тотальной спецификации [P(x), Q(x, y)]: P(x) & Q(x, y) LS(S(x: y)) (2)

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

36 P(x) [ LS(S)(x, y) Q(x, y) ] & y. LS(S)(x, y) (4.1) P(x) & Q(x, y) LS(S)(x, y)(4.6) Система правил доказательства корректности оператора суперпозиции, параллельного оператора и условного оператора Исчисление вычислимых предикатов множество вычислимых формул языка исчисления предикатов язык CCP (Calculus of Computable Predicates) минимальный полный базис языка предикатного программирования Язык предикатного программирования P (Predicate programming language). Расширяющаяся последовательность языков: CCP = P0, P1, P2, P3, P4 = P.

37 Язык P1: подстановка определения предиката на место вызова Подстановка определения предиката A(x: y) K(x: y) на место вызова A(t: z) блок { K(t: z) }, где x, y, t, z наборы переменных. Происходит замена вхождений переменных и переименование локалов. LS({ K(t: z) }) LS(K(t: z)) (5.1) runBlock(s, { K(t: z) }): runStat(s, K(t: z)) (5.2) Программа П, получаемая из программы П подстановкой определения предиката на место вызова, эквивалентна программе П: исполнение любого предиката программы П на фиксированном наборе аргументов дает тот же результат, что и в программе П. Язык P1: многократное произвольное применение подстановок определений предикатов на место вызовов. Конструкция: вызов или блок как подоператор в трех базисных операторах

38 Язык P2: оператор суперпозиции и параллельный оператор общего вида Операторы { A(…); B(…) }; C(…) и A(…); { B(…); C(…) } являются эквивалентными Эквивалентны{ A(…) || B(…) } || C(…) и A(…) || { B(…) || C(…) } Язык P2: оператор суперпозиции и параллельный оператор общего вида: A 1 (…); A 2 (…); … ; A n (…) и A 1 (…) || A 2 (…) || … || A n (…) для n > 1. P(x){B 1 (x: z 1 ); B 2 (z 1 : z 2 );...; B j (z j-1 : z j );...; B n (z n-1 : y)}Q(x, y) (5.3) x, z 1, z 2, …, z n-1, y различные непересекающиеся наборы переменных, B 1, B 2, …, B n обозначают предикаты или блоки языка P1 со спецификациями (предусловиями и постусловиями) P B1 (x), Q B1 (x, z 1 ), P B2 (z 1 ), Q B2 (z 1, z 2 ), …, P Bn (z n-1 ), Q Bn (z n-1, y).

39 LS( B 1 (x: z 1 ); B 2 (z 1 : z 2 );...; B j (z j-1 : z j );...; B n (z n-1 : y) ) z 1, z 2, …, z n-1.LS( B 1 (x: z 1 ) ) & LS( B 2 (z 1 : z 2 ) ) &...& & LS( B j (z j-1 : z j ) ) &...& LS( B n (z n-1 : y) ) (5.4) runStat(s, B 1 (x: z 1 ); …; B n (z n-1 : y )) runCallBlock(s, B1(x: z 1 )); (5.5) runCallBlock(s, B2(z 1 : z 2 ));.....; runCallBlock(s, Bj(z j-1 : z j ));.....; runCallBlock(s, Bn(z n-1 : y))

40 Параллельный оператор общего вида P(x){B 1 (x: y 1 ) || B 2 (x: y 2 )||...||B j (x: y j )||...||B n (x: y n )}Q(x, y) (5.7) x, y = y 1,…,y n различные непересекающиеся наборы переменных, B 1, B 2, …, B n предикаты или блоки языка P1 со спецификациями P B1 (x), Q B1 (x, y 1 ), P B2 (x), Q B2 (x, y 2 ),…,P Bn (x), Q Bn (x, y n ). LS(B 1 (x: y 1 ) || B 2 (x: y 2 ) ||...|| B j (x: y j ) ||...|| B n (x: y n )) LS(B 1 (x: y 1 )) & LS(B 2 (x: y 2 )) &... & & LS(B j (x: y j )) &... & LS(B n (x: y n )) (5.8) runStat(s, B 1 (…) || B 2 (…) || … || B n (…)) runCallBlock(s, B 1 (x: y 1 )) || (5.9) runCallBlock(s, B 2 (x: y 2 )) ||... || runCallBlock(s, B j (x: y j )) ||... || runCallBlock(s, B n (x: y n ))

41 Правило опускания скобок: {A(…); B(…)} || C(…) A(…); B(…) || C(…). A(x: y); {B(z: t) || C(u: v)} Набор y пересекается с набором z и не пересекается с набором u. Тогда A(x: y); {B(z: t) || C(u: v)} {A(x: y); B(z: t)} || C(u: v) A(x: y); B(z: t) || C(u: v). {A(x: y) || B(z: t)}; C(u: v) A(x: y) || B(z: t); C(u: v), если наборы y и u не пересекаются.

42 Язык P2: другое обобщение оператора суперпозиции B(x: z); C(x, z: y) обобщение оператора суперпозиции. P(x) {B 1 (x: z 1 ); B 2 (x, z 1 : z 2 );...; B j (x, z j-1 : z j );...; B n (x, z n-1 : y)} Q(x, y) (5.10) Частный случай: B(x: z); C(u, z: y), набор u часть набора x Наиболее общая форма суперпозиции: A(x: t, y) P(x) {B(x: z, t); C(x, z: y)} Q(x, t, y) (5.11) наборы x и t могут быть пустыми Спецификации: P B (x), Q B (x, z, t), P C (x, z), Q C (x, z, y).

43 B1(x: x1, z, t1) P B (x) {B(x: z, t1) || x1 = x} Q B (x, z, t1) & x1 = x C1(x1,z,t1: y, t) P C (x1, z) {C(x1, z: y) || t = t1} Q C (x1,z,y) & t = t1 Поскольку B1(x: x1, z, t1); C1(x1, z, t1: t, y) B(x: z, t); C(x, z: y), то справедливо другое определение предиката A: A(x: t, y) P(x) {B1(x: x1, z, t1); C1(x1, z, t1: t, y)} Q(x, t, y) (5.12) LS(B(x: z, t); C(x, z: y)) z. (LS(B(x: z, t)) & LS(C(z, y))) (5.13) runCallBlock(s, B(x: z, t)); (5.14) runCallBlock (s, C(x, z: y)) Правило RS1. P(x) P B (x) x1, z, t1 ((Q B (x, z, t1) & x1 = x) P C (x1, z)) Правило RS2. P(x) & x1,z,t1 (Q B (x1, z, t1) & x1 = x & Q C (x1, z, y) & t = t1) Q(x, t, y) A(x: t, y) P(x) {B(x: z, t); C(x, z: y)} Q(x, t, y) (5.11)

44 Правило RS5. P(x) P B (x) z, t (Q B (x, z, t) P C (x, z)) Правило RS6. P(x) & z (Q B (x, z, t) & (Q C (x, z, y)) Q(x, t, y) Лемма 5.5. Пусть предусловие P(x) истинно. Допустим, операторы B и C корректны. Если правила RS5 и RS6 истинны, то оператор суперпозиции (5.11) является корректным. Правило LS1. P(x) P B (x) Правило LS2. P(x) & Q(x, t, y) & Q B (x, z, t1) & x1=x P C (x1, z) & Q C (x1, z, y) & t = t1 Правило LS6.P(x) P B (x) Правило LS7.P(x) & Q(x, t, y) & Q B (x, z, t1) P C (x, z) & Q C (x, z, y) & t = t1 Лемма 5.6. Допустим, спецификация оператора суперпозиции (5.11) реализуема, операторы B и C однозначны в области предусловий и корректны, а их спецификации однозначны. Если правила LS6 и LS7 истинны, то оператор суперпозиции (5.11) является корректным.

45 Язык P3: выражения Функциональная форма. Предикат A(t: z). z = A(t) A(t: z) |z| = A(t), если z набор Инфиксная и постфиксная нотация как разновидность функциональной формы +(x, y: z), -(x, y: z), -(x: y),

46 D(x, z: u) P(x, z) {C(A(x), B(z): u)} Q(x, z, u) (5.15) E(x, z: y, t) P A (x) & P B (z){A(x: y) || B(z: t)}Q A (x, y) & Q B (z, t) D(x, z: u) P(x, z) { E(x, z: y, t); C(y, t: u)} Q(x, z, u) (5.16) Правило RS1. P(x, z) P A (x) & P B (z) y,t ( Q A (x, y) & Q B (z, t) P C (y, t)) Правило RS2. P(x, z) & y,t. ( Q A (x, y) & Q B (z, t) & Q C (y, t, u)) Q(x, z, u)

47 Правило RS7. P(x, z) P A (x) P B (z) P C (A(x), B(z)) Правило RS8. P(x, z) & Q C (A(x), B(z), u) Q(x, z, u). Лемма 5.7. Пусть предусловие P(x, z) истинно. Допустим, операторы A, B и C корректны, операторы A и B, а также их спецификации P A (x), Q A (x, y), P B (z), Q B (z, t) однозначны.. Если правила RS7 и RS8 истинны, то оператор (5.15) со спецификацией P(x, z) и Q(x, z, u) является корректным. Для получения правил серии L применим правила LS1 и LS2 для оператора в правой части (5.16). Правило LS1.P(x, z) P A (x) & P B (z). Правило LS2. P(x, z) & Q(x, z, u) & Q A (x, y) & Q B (z, t) P C (y, t) & Q C (y, t, u).

48 Правило LS8. P(x, z) P A (x) & P B (z). Правило LS9. P(x, z) & Q(x, z, u) P C (A(x), B(z)) & Q C (A(x), B(z), u). Лемма 5.8. Допустим, спецификация P(x, z) и Q(x, z, u) оператора (5.15) реализуема, операторы A, B и C однозначны в области предусловий и корректны, а их спецификации однозначны. Если правила LS8 и LS9 истинны, то оператор (5.15) является корректным. Понятие выражения. z = a b; y = z + c y = (a b) + c y = a b + c Правила приоритетов операций Переменные, изображения констант, вызовы функций и их представление в виде операций являются частными случаями понятия выражения.

49 else C(x: b); if (b) A(x: y) else B(x: y) if (C(x)) A(x: y) else B(x: y) В позиции условия выражение