Семинар 1. Логика Хоара. Корректность программ

Математические методыверификации схем и программСеминар 1Логика Хоара,Корректность программУпражнение 1Построить вычисление императивной программы на заданнойоценке переменныхx ⇐ z;while x < y doi f x % 2 thenx ⇐ 3 ∗ x + 1elsex ⇐ x / 2fiodОценка переменных:1. {x/15, y/4, z/1}2. {x/3, y/1, z/0}Упражнение 2Является ли программаI частично корректнойI тотально корректнойотносительно заданных триплетом предусловия и постусловия?truetruefalsefalsetruex = 50falsey = 50{x{x{x{x{x{x{x{x⇐⇐⇐⇐⇐⇐⇐⇐100}100}100}100}100}100}100}100}truefalsefalsetruex = 100x = 50x = 50y = 50Упражнение 2Является ли программаI частично корректнойI тотально корректнойотносительно заданных триплетом предусловия и постусловия?truetruefalsefalsex > 3x < 3x < 3x < −3x < −3{ while{ while{ while{ while{ while{ while{ while{ while{ whilexxxxxxxxx>>>>>>>>>000000000dododododododododoxxxxxxxxx⇐⇐⇐⇐⇐⇐⇐⇐⇐xxxxxxxxx−−−−−−−−−111111111od}od}od}od}od}od}od}od}od}truefalsefalsetruex = 0x = 0x = 1x = 0x = −7Упражнение 2Является ли программаI частично корректнойI тотально корректнойотносительно заданных триплетом предусловия и постусловия?true { x ⇐ E} x = E(E — произвольное выражение)Упражнение 3Записать в виде предусловия и постусловия требованиекорректности программы, записанное на естественном языке1.

программа записывает в переменную prod произведениезначений x и y2. программа записывает в переменные quo, rem частное иостаток от деления положительного значения x наположительное значение y3. программа меняет местами значения переменных x, y4. программа записывает в переменную N наибольший общийделитель значений x, y5. программа записывает в переменную m максимальныйэлемент непустого массива s[0 : n − 1]6. программа разворачивает непустой массив s[0 : n − 1]задом наперёдУпражнение 4Вычислить слабейшее предусловие для заданных программы ипостусловия{x ⇐{x ⇐{x ⇐{x ⇐{x ⇐{if xx +x +x +x +x += y10} x = 710} true10} f a l s e10} x = x + 1010; y ⇐ x + y} x = A & y = Bthen x ⇐ 7 e l s e x ⇐ x + y + 2}x = A & y = B & z = C{a [ 1 ] = x} ∀ i (0 ≤ i ≤ n → a [ i ] < 7){a [ y ] = x} a [ 3 ] = 7Упражнение 5Используя логику Хоара, доказать частичную корректность ипроверить тотальную корректность программы относительнозаданных требованийx ⇐ x + 1;y ⇐ y + 1Требование: если значения переменных x, y совпадали до выполнения программы, то будут совпадать после выполненияУпражнение 5Используя логику Хоара, доказать частичную корректность ипроверить тотальную корректность программы относительнозаданных требованийz ⇐ x;x ⇐ y;y ⇐ zТребование: значения переменных x, y меняются местамиУпражнение 5Используя логику Хоара, доказать частичную корректность ипроверить тотальную корректность программы относительнозаданных требованийx ⇐ 1;a [1] ⇐ 2;a[x] ⇐ xТребование: в первый элемент массива a записывается единицаУпражнение 5Используя логику Хоара, доказать частичную корректность ипроверить тотальную корректность программы относительнозаданных требованийx ⇐ 0;while a [ x ] 6= 0 dox ⇐ x + 1odТребование: если на вход подаётся массив a[0 : 1] = [1, 0], тозначения нолевого и первого элементов не изменяются, а значение a[x] после выполнения — нольРазбираем подробно{ a [ 0 ] = 1 & a [ 1 ] = 0}x ⇐ 0;while a [ x ] 6= 0 dox ⇐ x + 1od{ a [ 0 ] = 1 & a [ 1 ] = 0 & a [ x ] = 0}Разбираем подробно{ a [ 0 ] = 1 & a [ 1 ] = 0}x ⇐ 0;{ a [ 0 ] = 1 & a [ 1 ] = 0 & x = 0} // = ϕ ;while a [ x ] 6= 0 do // условие − Bx ⇐ x + 1od{ a [ 0 ] = 1 & a [ 1 ] = 0 & a [ x ] = 0} // = ψА как искать инвариант цикла?Это свойство inv цикла, которое “показывает, что всё хорошо”:ϕ → inv ,inv & B{.

. . }inv ,inv & ¬B → ψИ что же хорошего в этом цикле?Разбираем подробно{ a [ 0 ] = 1 & a [ 1 ] = 0}x ⇐ 0;{ a [ 0 ] = 1 & a [ 1 ] = 0 & x = 0}{ inv : 0 ≤ x ≤ 1 & a [0] = 1 &while a [ x ] 6= 0 do // условие −x ⇐ x + 1od{a [ 0 ] = 1 & a [ 1 ] = 0 & a [ x ] =// = ϕa [ 1 ] = 0}B0} // = ψЦикл совершает всего один виток, просматривает всего два элемента, и эти элементы остаются неизменными0 ≤ x ≤ 1 & a[0] = 1 & a[1] = 0Разбираем подробно{ a [ 0 ] = 1 & a [ 1 ] = 0}x ⇐ 0;{ a [ 0 ] = 1 & a [ 1 ] = 0 & x = 0}{ inv : 0 ≤ x ≤ 1 & a [0] = 1 &while a [ x ] 6= 0 do // условие −x ⇐ x + 1od{a [ 0 ] = 1 & a [ 1 ] = 0 & a [ x ] =// = ϕa [ 1 ] = 0}B0} // = ψϕ → inv :a[0] = 1 & a[1] = 0 & x = 0→0 ≤ x ≤ 1 & a[0] = 1 & a[1] = 0,Разбираем подробно{ a [ 0 ] = 1 & a [ 1 ] = 0}x ⇐ 0;{ a [ 0 ] = 1 & a [ 1 ] = 0 & x = 0}{ inv : 0 ≤ x ≤ 1 & a [0] = 1 &while a [ x ] 6= 0 do // условие −x ⇐ x + 1od{a [ 0 ] = 1 & a [ 1 ] = 0 & a [ x ] =// = ϕa [ 1 ] = 0}B0} // = ψinv & B{.

. . }inv :a[0] = 1 & a[1] = 0 & 0 ≤ x ≤ 1 & a[x] 6= 0{x ⇐ x + 1}a[0] = 1 & a[1] = 0 & 0 ≤ x ≤ 1Разбираем подробно{ a [ 0 ] = 1 & a [ 1 ] = 0}x ⇐ 0;{ a [ 0 ] = 1 & a [ 1 ] = 0 & x = 0}{ inv : 0 ≤ x ≤ 1 & a [0] = 1 &while a [ x ] 6= 0 do // условие −x ⇐ x + 1od{a [ 0 ] = 1 & a [ 1 ] = 0 & a [ x ] =// = ϕa [ 1 ] = 0}B0} // = ψinv & ¬B → ψa[0] = 1 & a[1] = 0 & 0 ≤ x ≤ 1 & a[x] = 0→a[0] = 1 & a[1] = 0 & a[x] = 0Разбираем подробно{ a [ 0 ] = 1 & a [ 1 ] = 0}x ⇐ 0;{ a [ 0 ] = 1 & a [ 1 ] = 0 & x = 0}{ inv : 0 ≤ x ≤ 1 & a [0] = 1 &while a [ x ] 6= 0 do // условие −x ⇐ x + 1od{a [ 0 ] = 1 & a [ 1 ] = 0 & a [ x ] =// = ϕa [ 1 ] = 0}B0} // = ψОказывается, если заменить “0 ≤ x ≤ 1” на “x ≥ 0” или вообще вычеркнуть из inv , это всё равно останется инвариантом;но в следующих примерах такие “простые” свойства не позволятдоказать корректностьРазбираем подробно{ a [ 0 ] = 1 & a [ 1 ] = 0}x ⇐ 0;{ a [ 0 ] = 1 & a [ 1 ] = 0 & x = 0}{ inv : 0 ≤ x ≤ 1 & a [0] = 1 &while a [ x ] 6= 0 do // условие −x ⇐ x + 1od{a [ 0 ] = 1 & a [ 1 ] = 0 & a [ x ] =// = ϕa [ 1 ] = 0}B0} // = ψА как быть с тотальной корректностью?Чтобы доказать, что цикл всегда завершает работу, достаточнопредоставить выражение E над целыми числами (ограничивающую функцию), которое уменьшается с каждым витком цикла ипри этом ограничено снизуНапример, выражение (1−x) постоянно уменьшается и ограничено снизу значением 0, а значит, программа тотально корректнаУпражнение 5Используя логику Хоара, доказать частичную корректность ипроверить тотальную корректность программы относительнозаданных требованийx ⇐ 2;while a [ x ] 6= 0 dox ⇐ x + 1odТребование: если на вход подаётся массив a[0 : 1] = [1, 0], тозначения нолевого и первого элементов не изменяются, а значение a[x] после выполнения — нольУпражнение 5Используя логику Хоара, доказать частичную корректность ипроверить тотальную корректность программы относительнозаданных требованийquo ⇐ 0 ; rem ⇐ x ;while rem ≥ y dorem ⇐ rem − y ;quo ⇐ quo + 1odТребование: в переменную quo записывается частное, а в переменную rem — остаток от деления неотрицательного значения xна неотрицательное значение yОтвет{ x ≥ 0 & y ≥ 0}quo ⇐ 0 ; rem ⇐ x ;{ x ≥ 0 & y ≥ 0 & quo = 0 & rem = x }{ i n v : x = quo ∗ y + rem & rem ≥ 0}while rem ≥ y dorem ⇐ rem − y ;quo ⇐ quo + 1od{ x = quo ∗ y + rem & 0 ≤ rem < y }Программа не является тотально корректной: если y = 0,то цикл не завершит работуА если y > 0, то ограничивающая функция — remУпражнение 5Используя логику Хоара, доказать частичную корректность ипроверить тотальную корректность программы относительнозаданных требованийquo ⇐ 0 ; rem ⇐ x ;while rem ≥ y dorem ⇐ rem − y ;quo ⇐ quo + 1odТребование: в переменную quo записывается частное, а в переменную rem — остаток от деления неотрицательного значения xна положительное значение yУпражнение 5Используя логику Хоара, доказать частичную корректность ипроверить тотальную корректность программы относительнозаданных требованийp r ⇐ 0 ; cou ⇐ y ;while cou > 0 dopr ⇐ pr + x ;cou ⇐ cou − 1odТребование: в переменную pr записывается произведение неотрицательных значений x, yУпражнение 5Используя логику Хоара, доказать частичную корректность ипроверить тотальную корректность программы относительнозаданных требованийx ⇐ 0 ; y ⇐ 1 ; cou ⇐ n ;while cou > 0 doh ⇐ y;y ⇐ x + y;x ⇐ h;cou ⇐ cou − 1 ;odТребование: в переменную x записывается n-е число ФибоначчиНичто не запрещает ввести функцию fib(n), если мы работаем сней “логично”: ∀n(n ≥ 0 → fib(n + 2) = fib(n + 1) + fib(n))Упражнение 5Используя логику Хоара, доказать частичную корректность ипроверить тотальную корректность программы относительнозаданных требованийi ⇐ 1; m ⇐ s [ 0 ] ;while i < n doi f s [ i ] < m thenm ⇐ s[i]fi ;i ⇐ i + 1odТребование: в переменную m записывается максимальный элемент непустого массива s[0 : n − 1]Упражнение 5Используя логику Хоара, доказать частичную корректность ипроверить тотальную корректность программы относительнозаданных требованийsum ⇐ 0 ; i ⇐ 0 ;while i < n dosum ⇐ sum + s [ i ]odТребование: в переменную sum записывается сумма элементовнепустого массива s[0 : n − 1]Упражнение 5Используя логику Хоара, доказать частичную корректность ипроверить тотальную корректность программы относительнозаданных требованийi ⇐ 0;while 2 ∗ i < n − 1 doy ⇐ s[ i ];s [ i ] ⇐ s [ n−i − 1 ] ;s [ n−i −1] ⇐ y ;i ⇐ i + 1;odТребование: в результате работы программы массив s[0 : n − 1]разворачивается задом наперёдДомашнее заданиеИспользуя логику Хоара, доказать тотальную корректностьпрограммы, сортирующей непустой массив целых чиселs[0 : n − 1] по неубываниюi ⇐ n − 1;while i > 0 dok ⇐ i ; j ⇐ i − 1;while j ≥ 0 doi f s [ j ] > s [ k ] thenk ⇐ jfi ;j ⇐ j − 1od ;y ⇐ s[k]; s[k] ⇐ s[ i ]; s[ i ] ⇐ y;i ⇐ i − 1;od(см.

подсказку про новые символы для чисел Фибоначчи).