4

4. НАЙПРОСТІШІ ВЛАСТИВОСТІ ПРОГРАМ

Склавши програму, ми, очевидно, розраховуємо отримувати з її допомогою правильні результати кожного разу, коли її початкові дані правильні. Цю властивість природно назвати правильністю програми.

Для того щоб дослідити правильність програми, розглянемо властивості виконання. Можливі три випадки:

1) виконання програми завершується отриманням деякого результату (нормальне завершення);

2) виконання програми не завершується (нескінченне виконання);

3) на певному етапі виконання програми виявляється, що подальше її виконання неможливе (відмова).

Складаючи програму, слід би виключити нескінченне виконання. Для правильних вхідних даних повинно мати місце нормальне завершення з отриманням правильного результату, у разі неправильних початкових даних - відмова.

Приклад 4.1. Дані два натуральних числа n і m. Перевірити, чи ділиться n без остачі на m.

Розглянемо наступний фрагмент алгоритму

взяти (n, m);

якщо (m=0) V (n<m & n<>0) то

z <- -1

інакше

z <- n;

поки z>0 повт (А)

z <- z-m

кц

кр;

якщо z=0 то показати (n,' ділиться на ', m)

інакше показати (n,' не ділиться на ', m) кр.

Як пересвідчитися, що алгоритм (А) та відповідна йому програма П є правильними? Один підхід полягає в тому, щоб ввести програму, що реалізує цей алгоритм, в комп'ютер, скомпілювати її і перевірити для ряду даних. Такий метод ніколи не може дати абсолютної упевненості в правильності програми просто тому, що число можливих контрольних варіантів нескінченне. Набагато краще, довести, якщо це можливо, правильність програми. Існують різні способи доведення. Один з них - доведення від противного.

У нашому алгоритмі, очевидно, в якості твердження, що доводиться треба взяти висловлювання (z=0 = n ділиться на m). Припустимо, що це твердження невірне. Воно еквівалентно кон’юнкції висловлювань (z=0 É n ділиться на m) & (n ділиться на m É z=0). За припущенням, кон’юнкція хибна. Значить, хибний принаймні один з її членів. Допустимо, (z=0 É n ділиться на m) хибне, тобто z=0 істинне, але n на m не ділиться. Відповідно до алгоритму z=0 або коли n=0, або коли в процесі віднімання при деякому k (n-m-...-m) (k разів) виходить 0. В першій ситуації з n=0 слідує (n ділиться на m) в суперечності з пнрипущенням. У другій в силу еквівалентності висловлювання ( $ k Î N: 0=(n-m-..-m) (k разів) ) = ( $ k Î N: k*m=n) = (n ділиться на m) виявляється істинним твердження (n ділиться на m), що знову суперечить припущенню. Таким чином, z=0 спричиняє (n ділиться на m).

Припустимо тепер, що n ділиться на m, але z<>0. Нерівність z<>0 може мати місце або при (m=0) V (n<m & n<>0), або після завершення циклу, або в ході його виконання. Присвоєння z <- n при n<>0 призводить до входження в цикл, оскільки з n<>0 слідує n>0 і z>0. Так що ніяких інших можливостей для z<>0, крім відмічених трьох, не існує. Розберемо ці три можливості почергово.

Абсолютно очевидно, що (m=0) V (n<m & n<>0) спричиняє не тільки z<>0, але і (n не ділиться на m). Залишається розглянути цикл. Нехай z<>0 і цикл завершений. Тоді z<0. Знову використовуємо еквівалентність (n ділиться на m) = ( $ k Î N: 0=(n-m-..-m) (k разів) ). Оскільки процес віднімання в циклі призвів до негативного z, потрібного k не існує. Звідси n не ділиться на m. Залишається третя і остання можливість: z<>0 в ході виконання циклу. Але в цьому випадку ми і не вимагаємо, щоб була дана відповідь на питання про подільність n на m. Ми розраховуємо його отримати після виконання програми, а не в ході виконання. Але щойно було доведено, якщо цикл завершиться з z<>0, n на m не ділиться. Тим самим ми довели, що якщо алгоритм А закінчить роботу, задача на подільність буде вирішена, причому вирішена правильно.

Іншим способом доведення правильності програм є метод математичної індукції (ММІ). Ми їм вже неодноразово користувалися. Наприклад, ММІ застосовувався при доведенні правильності програми для визначення у = аⁿ.

Сформулюємо тепер поняття правильної програми. Нехай П - програма, F - твердження, що відноситься до вхідних даних, яке повинне бути істинне перед виконанням програми П, і G - твердження, яке повинне бути істинне після виконання програми П. F називається передумовою, а G - післяумовою програми П.

Розрізняють два вигляди правильності: часткову і повну. Програма П називається частково правильної по відношенню до F і G, якщо кожний раз, коли F істинна перед виконанням П і П закінчує роботу, післяуиова G також буде істинна. У цьому випадку будемо писати {F} П {G}. Програма П називається повно правильною по відношенню до F і G, якщо вона частково правильна по відношенню до F і G і обов'язково завершує свою роботу, якщо F істинне. У цьому випадку пишемо {F} П+ {G}.

Підкреслимо, що поняття правильності програми П сформульоване відносно відповідних тверджень F і G. Тому з істинності твердження {F} П {G} (або {F} П+ {G} відповідно) не обов'язково випливає істинність твердження про правильність при інших умовах. Аналогічним чином, заміна в {F} П {G} (або {F} П+ {G} ) програми П на програму Г, взагалі кажучи, не зберігає істинного значення твердження про правильність.

З означень слідує, що будь-яка повно правильна програма є частково правильною при тих же перед- та післяумовах. Зворотнє, звичайно, не вірно.

У прикладі 4.1 ми довели повну правильність програми П { n Î N & m Î N } П+ { z=0 = n ділиться на m }.

Розглянемо деякі методи проектування програм, що гарантують їх правильність.

Джерелом нескінченного виконання програм є, очевидно, цикли за умовою. Ми розглядали три цикли за умовою: цикл з умовою повторення, цикл з умовою закінчення і цикл з виходом. Причому два останніх цикли визначали через цикл з умовою повторення. Тому надалі в цьому пункті будемо розглядати тільки цикл з умовою повторення.

Проаналізуємо властивості циклу з умовою повторення з метою виявлення тих з них, які можна було б покласти в основу проектування циклів.

Спочатку займемося аналізом числа виконань циклу. Нехай х - дійсна змінна, G(х) - умова. Розглянемо, наприклад, цикл

поки G(х) повт

х <- f(х) (S)

кц,

де функція f задана у вигляді деякого арифметичного виразу.

Цикл (S) називається скінченним при початковому значенні х, рівному C, якщо його виконання, почате при х = C, закінчується через скінченне число повторень. Наприклад, цикл

{ х = C }

поки х>0 повт

х <- х+1

кц

скінченний при будь-якому значенні C <= 0 і нескінченний при C > 0.

Зрозуміло, складаючи цикл, необхідно потурбуватися про дотримання необхідної умови скінченності циклу, а саме: змінні, що використовуються в умові G(х), повинні змінюватися в тілі циклу. Якщо жодна змінна з умови G(х) в тілі циклу не змінюється, то ніколи не зміниться значення самої умови. Отже, одного разу почавши виконуватись, такий цикл ніколи не закінчиться.

Нехай В(х) - функція, що приймає цілі значення. Назвемо її обмежувальною функцією циклу (S), якщо

G(х) = Іст спричиняє В(х) > 0, (B1)

B(х) > В(f(х)), (B2)

тобто кожне виконання тіла х <- f(х) циклу (S) зменшує значення В(х).

Обмежувальна функція грає важливу роль при аналізі cкінченності циклів.

Теорема 4.1. (про скінченність циклу). Якщо цикл (S) має обмежувальну функцію В(х), то він скінченний при будь-якому початковому значенні C змінної х.

Доведення. Розглянемо послідовність

а = C, (4.1)

а = f(а ), k=1,2,...

k k-1

значень змінної х, що отримується при виконанні циклу (S).

Визначимо далі цілу послідовність

b = В(а ), k=0,1,2,...

k k

Згідно з властивістю (B2) послідовність b_k монотонно спадає

b > b >. .. > b > ...

0 1 m

Отже, знайдеться такий номер n >= 0, що b_n <= 0, тобто B(а_n) <= 0 і згідно з властивістю (B1) G(а_n) = Хиб. Виконання циклу (S) таким чином закінчується при значенні х, рівному а_n, через n кроків після початку.¦

Приклад 4.2. Дослідити скінченність циклу

поки х > 0 повт

х <- х-1

кц.

Необхідна умова скінченності циклу очевидно виконується. Розглянемо функцію В(х) = [х]+1. Оскільки [х] >= 0 при х>0, то х>0 спричиняє В(х) > 0. Оскільки [х-1]=[х]-1, то В(х) = [х]+1 > [х] = [х-1]+1 = В(х-1). Отже В(х) - обмежувальна функція і, згідно з теоремою 4.1, цикл скінченний.

Наслідок 4.1. Яким би не було початкове значення C змінної х, якщо виконання циклу (S) закінчується, то заключне значення змінної х задовольняє умові, протилежній G(х), тобто

поки G(х) повт

х <- f(х)

кц

{ ¬ G(х) }.¦

Повертаючись до взаємодії циклічних програм помітимо, що всі Ас-програми містяться в класі Aw-програм. Зворотнє, взагалі кажучи, невірно. Для з'ясування цього досить помітити, що будь-який цикл вигляду (Lc) має обмежувальну функцію В(k) = (c-k)*b.

Тому будь-яка Ас-програма кінцева. У той же час, наприклад, Aw-програма

k <- 1;

поки k>0 повт Нічого кц (4.2)

є нескінченною. Отже, ніяка Ас-програма не може бути реалізацією (4.2).

Розглянемо ще одну властивість циклів на прикладі.

Приклад 4.3. Алгоритм множення двох натуральних чисел n і m за допомогою повторного додавання:

а <- n; b <- m; c <- 0;

поки b <> 0 повт

b <- b-1; c <- c+а

кц.

Зміст цього алгоритму очевидний: до c, спочатку рівному 0, b разів додається a, що прямо відповідає визначенню множення. Включимо в алгоритм деяке висловлювання, яке повинне бути справедливими (якщо алгоритм вірний) незалежно від того, по якому шляху обчислення прийшло в дану точку. У цьому випадку висловлювання є "інваріантом циклу", тобто реченням, яке справедливе, скільки б разів даний цикл не виконувався. Яке ж висловлювання про величини, що входять в задачу, залишається справедливим протягом всього виконання алгоритму? Оскільки а і b на самому початку задані рівними n і m, то на початковому етапі а*b повинно бути рівним n*m. Аналогічно, коли обчислення завершене, як добуток береться c, яке повинно також дорівнювати n*m. На проміжних етапах між початком і кінцем цієї процедури при кожному збільшенні c на а відбувається зменшення b на 1. Із цього випливає, що рівність а*b+c = n*m має силу протягом всього розрахунку. Дане висловлювання є, отже, основним інваріантом цього циклу поки; разом з умовою завершення (b=0) воно встановлює необхідний результат (c=n*m).

У цьому прикладі справедливість висловлювання, використаного для підтвердження правильності програми, носить навряд чи більш очевидний характер, ніж правильність самих операторів алгоритму. Однак цей алгоритм простий. Вся сила висловлювання, як засобу верифікації програм, виявляється, коли алгоритм вдосконалюють з метою підвищити його ефективність. Адже як би програма ні ускладнювалася, висловлювання, сформульоване в найпростішому випадку, залишається справедливим.

У алгоритмі множення методом повторного додавання цикл повинен виконатися m разів. Існують набагато більш швидкі методи. Наприклад, алгоритм заснований на тому ж самому принципі, але тільки b зменшують більш великими кроками. Замість того щоб зменшити значення b на 1, його ділять на 10, що в десятковій системі виконати особливо легко.

Щоб застосувати цей ефективний метод, модифікуємо алгоритм, виходячи з вимоги зберегти інваріантом висловлювання а*b+c=n*m. Оператор присвоєння b<-b-1 в початковому алгоритмі потрібно замінити на b<-b div 10. Збереження інваріанта вимагає, щоб а було помножене на 10. Якщо b не кратне 10, залишок (b mod 10) віднімається від b, тому, щоб зберегти інваріант, до c додають а*(b mod 10). Остаточно отримуємо алгоритм

а <- n; b <- m; c <- 0;

поки b <> 0 повт

c <- c+а*(b mod 10);

а <- а*10; b <- b div 10

кц.

Розглянемо більш детально поняття інваріанта для циклу

поки F повт Р кц, (4.3)

де F - умова, Р - інструкція.

Умова Q називається інваріантом циклу (4.3), якщо його істинність не порушується дією Р, тобто з істинності умови Q до виконання дії Р у разі справедливості F випливає істинність умови Q після виконання Р.

З визначення інваріанта циклу і наслідку 4.1 випливає справедливість

Властивість 4.1. Якщо:

1) умова Q(х) є інваріантом циклу (S);

2) цикл (S) завершується нормально;

3) умова Q(х) істинна до виконання циклу,

то після виконання циклу (S) буде істинною кон’юнкція умов Q(х) & ¬ G(х).

Властивість 4.1 використовується в методі проектування циклів, що отримав назву методу ітерацій.

Для проектування циклу методом ітерацій необхідно:

1) виявити умови, які будуть справедливими до початку циклу;

2) визначити умови, які повинні бути справедливими після його завершення;

3) виділити ті з них, які залишаються незмінними в процесі розв’язку задачі;

4) визначити тіло циклу так, щоб останні умови стали його інваріантом.

Розглянемо два цикли

поки G(k, х) повт

k <- k+1; х <- f(х) (4.4)

кц

та

поки G(k, х) повт

х <- f(х); k <- k+1 (4.5)

кц

в яких змінна k грає роль лічильника числа повторень тіла циклу.

Наслідок 4.2. Нехай послідовність { а_k } задана співвідношеннями (4.1). Тоді умова х=а_k є інваріантом циклів (4.4) і (4.5), тобто

{ k=0 & х=а } { k=0 & х=а }

0 0

поки G(k, х) повт поки G(k, х) повт

k <- k+1; х <- f(х) х <- f(х); k <- k+1

{ х=а } { х=а }

k k

кц кц

Приклад 4.4. Степінь з натуральним показником.

k <- 0; у <- 1;

{ у=х^k }

поки k<>n повт

k <- k+1; у <- у*х

{ у=х^k }

кц

{ k=n, у=х^k }.

[ЗМІСТ] [Далі] [Назад]