Анотація: Розглядається схема побудови циклу "поки" за допомогою інваріанта, тобто затвердження, яке зберігається при кожному виконанні тіла циклу. Застосування цієї схеми дає можливість свідомо будувати алгоритм і доводити правильність його роботи по тексту, не вдаючись до тестування. Застосування схеми ілюструється на прикладах: алгоритм Евкліда обчислення найбільшого загального дільника, алгоритм швидкого зведення в ступінь, розширений алгоритм Евкліда, наближене обчислення логарифма без використання розкладання в ряд.
Правильне використання конструкції циклу завжди представляє деяку складність. Застосування елементарної теорії допомагає уникнути помилок і полегшує написання складних програм.
Основна ідея полягає в наступному. В процесі виконання циклу змінюються значення набору змінних. Треба знайти співвідношення між мінливими змінними, яке залишається постійним. Це співвідношення називається інваріантом циклу. Свідоме побудова циклу "поки" завжди пов'язане з явною формулюванням і використанням інваріанта циклу.
Явна формулювання інваріанта допомагає виписати ініціалізацію змінних, виконувану до початку циклу. і тіло циклу. Ініціалізація повинна забезпечити виконання інваріанта до початку роботи циклу. Тіло циклу має бути сконструйоване таким чином, щоб забезпечити збереження інваріанта. (Більш точно, з того, що інваріант виконується до початку виконання тіла циклу. Має слідувати виконання інваріанта після закінчення тіла циклу. В процесі виконання тіла циклу інваріант може порушуватися.)
Завершення циклу. як правило, пов'язано з обмеженою величиною. яка монотонно зростає або монотонно убуває при кожному виконанні тіла циклу. Цикл "поки" завершується, коли умова після слова "поки" в заголовку циклу стає хибним. Отже, ця умова має прямо або побічно залежати від величини, монотонно спадної або зростаючій в процесі виконання циклу. По досягненню її певного значення умова має ставати помилковим. Умовою завершення циклу називають заперечення умови, що стоїть після слова "поки" в заголовку циклу.
Виконання інваріанта циклу і одночасно умови завершення повинно забезпечувати рішення необхідної задачі.
Загальна схема
Позначимо через X безліч всіляких наборів значень всіх змінних, що міняються в ході виконання циклу. Безліч X іноді називають фазовим, або конфігураційним, простором завдання. Інваріант - це деяка умова I (x). залежне від точки x з множини X і приймає значення "істина" або "брехня". (Математики називають такі умови предикатами.) В процесі ініціалізації точці x присвоюється таке значення x0. що умова I (x0) істинно.
Позначимо умова завершення циклу через Q (x). Умови I (x) і Q (x) повинні бути підібрані таким чином, щоб одночасна істинність I (x) і Q (x) забезпечувала рішення необхідної задачі: знаходження точки x з необхідними властивостями.
Тіло циклу можна трактувати як відображення точки x в нову точку T (x) з того ж безлічі X:
Умова I (x) є інваріантом для відображення T. якщо I (x) істинно, то I (T (x)) також істинно.
Загальна схема побудови циклу з допомогою інваріанта виглядає наступним чином:
Звичайно, ця схема не має ніякої цінності без уміння застосовувати її на практиці. Розглянемо кілька важливих прикладів її використання.