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

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла

Математические методыверификации схем и программСеминар 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(см.

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

Характеристики

Тип файла PDF

PDF-формат наиболее широко используется для просмотра любого типа файлов на любом устройстве. В него можно сохранить документ, таблицы, презентацию, текст, чертежи, вычисления, графики и всё остальное, что можно показать на экране любого устройства. Именно его лучше всего использовать для печати.

Например, если Вам нужно распечатать чертёж из автокада, Вы сохраните чертёж на флешку, но будет ли автокад в пункте печати? А если будет, то нужная версия с нужными библиотеками? Именно для этого и нужен формат PDF - в нём точно будет показано верно вне зависимости от того, в какой программе создали PDF-файл и есть ли нужная программа для его просмотра.

Список файлов семинаров