TP, КНУ імені Тараса Шевченка, ПРОГРАМНІ ЛОГИКИ ФЛОЙДА-ХОАРА. Коректність та повнота.

TP, КНУ імені Тараса Шевченка, Мета лекції Сформулювати семантичні підстави логік верифікації програм Визначити логіку Флойда-Хоара для простої мови програмування Довести коректність та (відносну) повноту програмної логіки Флойда-Хоара

TP, КНУ імені Тараса Шевченка, Основні питання лекції Проста мова програмування та її семантика Анотації програм Аксіоматичне числення Флойда-Хоара Коректність числення Відносна повнота числення Узагальнення логік Флойда-Хоара Висновки

TP, КНУ імені Тараса Шевченка, Проста мова програмування SIPL Основні композиції мови є композиціями структурного програмування. Також додаються суперпозиції та реномінації. Основні типи функцій (State=Var Int): - номінативні FA=State Int - предикати FB=State Bool - біномінативні FS=State State Семантична основа – багатосортна алгебра номінативних функцій.

TP, КНУ імені Тараса Шевченка, Багатосортна алгебра номінативних функцій A (з релевантними композиціями)

TP, КНУ імені Тараса Шевченка, Семантика композицій мови SIPL КомпозиціяФормула обчислення Суперпозиції (S n (f, g 1,…, g n ))(st)=f(g 1 (st),…, g n (st)) (S [х] (fa, g))(st)=fa(st [x g(st)]) (S [х] (fb, g))(st)=fb(st [x g(st)]) Присвоєння AS x (fa)(st)=st [x fa(st)] Послідовність fs 1 fs 2 (st)=fs 2 (fs 1 (st)) Умовний оператор IF(fb, fs1, fs2)(st)= fs1(st), якщо fb(st)=true, IF(fb, fs1, fs2)(st)= fs2(st), якщо fb(st)=false. Цикл WH(fb,fs)(st)=st n, де st 0 =st, st 1 =fs(st 0 ), st 2 =fs(st 1 ), …, st n =fs(st n-1 ), причому fb(st 0 )=true, fb(st 1 )=true,…, fb(st n-1 )=true, fb(st n )=false. Розіменування x (st)=st(x) Тотожна ф-ія id(st)=st

TP, КНУ імені Тараса Шевченка, Приклад програми мови SIPL (підсолоджений семантичний терм) Найбільший спільний дільник: GCD = begin while M N do if M>N then M:=M–N else N:=N–M end Підсолоджений семантичний терм: sem_P(GCD)= WH(M N, IF(M>N, AS M (M–N), AS N (N–M)))

TP, КНУ імені Тараса Шевченка, Анотації програм. Формули Флойда-Хоара Формула, яка задає предикат типу State Bool називається анотацією. Анотації є корисними для доведення властивостей програм. Нехай LP – мова певної логіки предикатів. Формули Флойда-Хоара: {P}fs{Q}, де P – формула мови LP – передумова Q – формула мови LP – післяумова fs – терм програмної мови PL Є інші позначення: Хоара - P{fs}Q, повна коректність - [P]fs[Q].

TP, КНУ імені Тараса Шевченка, Семантика формул Флойда-Хоара Нехай A – програмна алгебра. Інтерпретацію формул та програм задамо відносно A. Формула Флойда-Хоара {P1} fs {P2} частково істинна (частково коректна, неспростовна) відносно A, позначаємо A |={P1}fs{P2}, якщо для довільного стану st, з того, що P1 A (st) =true, fs A (st) =st, та P2 A (st ) випливає, що P2 A (st ) = true. У подальшому індекс A будемо опускати.

TP, КНУ імені Тараса Шевченка, Приклади формул Флойда-Хоара Ми дотримуємось семантико-синтаксичного підходу, згідно якого основну роль грає семантика, а синтаксис їй підпорядкований. Тому у прикладах використовуються (підсолоджені) терми семантичної алгебри. {M>0 N>0} AS M (M–N) {M=N} {M>0 N>0} WH(M N, IF(M>N, AS M (M–N), AS N (N–M))) {M=N}

TP, КНУ імені Тараса Шевченка, Числення часткової коректності

TP, КНУ імені Тараса Шевченка, Приклад: доведення коректності програми GCD (1) Значення змінних M та N в заключному стані st є найбільшим спільним дільником значень цих змінних в початковому стані st. Тобто, gcd(X(st),Y(st))=gcd(M(st ),N(st )), де gcd(m,n) – найбільший спільник дільник чисел m та n. Але смисл формул такий, що предикати (перед- та післяумови) обчислюються лише на одному поточному стані, тобто або на st, або на st. Тому вводимо так звані логічні змінні X та Y, їх початкові значення програмою не змінюються, тобто стани мають вигляд [X x, Y y, M m, N n], де x, y, m, n – цілі числа. У початковому стані x=m, y=n. Коректність – твердження gcd(X,Y)=gcd(M,N).

TP, КНУ імені Тараса Шевченка, Приклад: доведення коректності програми GCD (2) Позначимо P = def gcd(X,Y)=gcd(M,N). Побудова виводу для формул з AS M (M–N). Згідно схеми аксіом Ax_AS можна вивести таку формулу {S [M] (P, M–N)} AS M (M–N){P}, тобто |– {S [M] (P, M–N)} AS M (M–N){P}. Оскільки оператор виконується при умові (M>N), то можна посилити передумову і за схемою Ax_CONS вивести формулу {(M>N) S [M] (P, M–N)} AS M (M–N){P}. Тут імплікація (M>N) S [M] (P, M–N) S [M] (P, M–N) є очевидною. Отже, можна написати |– {(M>N) S [M] (P, M–N)} AS M (M–N){P}.

TP, КНУ імені Тараса Шевченка, Приклад: доведення коректності програми GCD (3) Наступним кроком буде посилення передумови до (M>N) P. Щоб це зробити, треба довести імплікацію (M>N) P (M>N) {S [M] (P, M–N)}. Для (семантичного) доведення цієї імплікації розглянемо довільний стан st виду [X x, Y y, M m, N n], на якому предикат (M>N) P є істинним. Це означає, що ((M>N) P)(st)=true. Це означає, що m>n та gcd(x,y)=gcd(m,n). Обчислення значення (M>N) (S [M] (P, M–N)) (st) призводить до виразів m>n та gcd(x,y)=gcd(m–n, n). З теорії чисел відомо, що коли m>n, то gcd(m,n)= gcd(m–n, n). Тому імплікація істинна. Таким чином, за правилом Ax_CONS маємо |– {(M>N) P} AS M (M–N){P}.

TP, КНУ імені Тараса Шевченка, Приклад: доведення коректності програми GCD (4) Доведення (для операторів присвоєння):

TP, КНУ імені Тараса Шевченка, Приклад: доведення коректності програми GCD (5) Тепер виводимо: |– {P} IF(M>N, AS M (M–N), AS N (N–M)) {P} Передумову можна посилити, дописавши до неї предикат (M N): |– {(M N) P} IF(M>N, AS M (M–N), AS N (N–M)) {P} Тепер, за схемою Ax_WH отримуємо |–{P} WH(M N, IF(M>N, AS M (M–N), AS N (N–M))) {P (M N)}. Нарешті, посилимо передумову до (X=M Y=N). (Тут імплікація (X=M Y=N) P очевидна.) Також послабимо післяумову з урахуванням, що (M N)= (M=N). Тому |– P (M N) (M=N) gcd(X,Y)=M. Отримали, що |–{(X=M Y=N)} WH(M N, IF(M>N, AS M (M–N), AS N (N–M))) {(M=N) gcd(X,Y)=M}.

TP, КНУ імені Тараса Шевченка, Приклад: доведення коректності програми GCD (6) Остання формула стверджує часткову коректність програми GCD в композиційній семантиці: якщо X=M Y= N в початковому стані, та якщо програма завершується, то M=N та значення M є найбільшим спільним дільником початкових значень M та N.

TP, КНУ імені Тараса Шевченка, Коректність логіки Флойда-Хоара (1)

TP, КНУ імені Тараса Шевченка, Коректність логіки Флойда-Хоара (2)

TP, КНУ імені Тараса Шевченка, Коректність логіки Флойда-Хоара (3)

TP, КНУ імені Тараса Шевченка, Коректність логіки Флойда-Хоара (4)

TP, КНУ імені Тараса Шевченка, Коректність логіки Флойда-Хоара (5)

TP, КНУ імені Тараса Шевченка, Повнота логіки Флойда-Хоара (1)

TP, КНУ імені Тараса Шевченка, Повнота логіки Флойда-Хоара (2)

TP, КНУ імені Тараса Шевченка, Повнота логіки Флойда-Хоара (3)

TP, КНУ імені Тараса Шевченка, Повнота логіки Флойда-Хоара (4)

TP, КНУ імені Тараса Шевченка, Повнота логіки Флойда-Хоара (5)

TP, КНУ імені Тараса Шевченка, Повнота логіки Флойда-Хоара (6)

TP, КНУ імені Тараса Шевченка, Синтаксично-орієнтоване числення

TP, КНУ імені Тараса Шевченка, Узагальнення логіки Флойда-Хоара 1. Узагальнення на складні структури даних 2. Узагальнення на взаємодіючі процеси 3. Узагальнення для нових композицій 4. Повна коректність та завершуваність програм

TP, КНУ імені Тараса Шевченка, Висновки Фундаментальність (класичність) логіки Флойда-Хоара Широка сфера застосувань Програмні засоби підтримки