Інваріант і функція обмеження циклу

Основна ідея методу проектування циклу за допомогою інваріанту - вираження взаємозв'язку між змінними в тілі циклу об'єктами у вигляді незмінної умови. Користь інваріанта полягає в тому, що такий опис взаємозв'язку легко зрозумілий і дозволяє, знаючи, як змінюються одні об'єкти, виводити, як мають змінюватимуться інші. Тим самим інваріант допомагає сконструювати команди S0 і S.

Визначення 9.6. Інваріант циклу — предикат, який правдивий перед виконанням циклу і після кожної його ітерації.

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

Для побудови коректної умови продовження циклу e використовується обмежуюча функція h. На кожному кроці циклу значення має зменшуватися принаймні на одиницю і залишатися додатнім до кінця циклу. Функція обмеження дозволяє гарантувати завершення циклу.

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

Схема проектування циклу за допомогою інваріанту.

• На першому етапі виконуються прості присвоювання S0, що роблять інваріант I істинним, а в якості умови продовження циклу береться предикат .
• На другому етапі конструюється тіло циклу S, що реалізує перетворення T: спочатку забезпечується зменшення обмежує функції h, а потім - збереження інваріанту I.

Геометрична інтерпретація даної схеми наведена на рисунку 9.2, де через позначено множину, що виходить з за допомогою сукупності присвоювання S0.

 

 

 

Рис. 9.2. Проектування циклу за допомогою інваріанта   Розглянемо застосування цієї схеми для вирішення наступного завдання.

ЗАВДАННЯ 9.24. Напишіть програму, яка знаходить добуток двох цілих чисел, одне з яких невід'ємне, без використання операції множення. Точні перед- і постумови необхідної програми, часова складність якої не повинна перевершувати такі: , . При написанні програми величини і змінювати не дозволяється, слід використовувати інваріант і обмежуючу функція .

 

Рішення. Для написання програми треба сконструювати S0 (сукупність присвоєнь, здійснюють початкову ініціалізацію), умову продовження e і тіло циклу S.

Початкові присвоювання повинні легко знаходитися та зробити істинним інваріант (у разі істинності передумови) і при цьому залишатися максимально простими. У нашому випадку досить швидко можна виявити, що гарним кандидатом на роль S0 є наступна сукупність присвоювання "x = a; y = b; z = 0;".

Умова продовження циклу e нам вже по-суті дана, бо чергова ітерація циклу повинна відбуватися тільки за h > 0. З цієї причини логічно припустити, що наша програма повинна містити оператор "while (y> 0) S;", тіло якого S поки невідомо.

Ми зобов'язані забезпечити завершення циклу, отже величина y повинна зменшуватися на кожній його ітерації. Зменшення y щоразу на одиницю свідомо не дозволить одержати досить ефективну програму. З цієї причини необхідно зменшувати величину y більш швидко. Гарною думкою є спроба ділити величину y навпіл тоді, коли це можна (при парних y). Легко оцінити, що якщо б поділ навпіл відбувалося на кожному кроці циклу, то кількість його ітерацій приблизно дорівнювала б log b. Це цілком узгоджується з тим, що потрібно для умови задачі по складності.

Враховуючи те, що після ітерації циклу інваріант повинен залишитися істинним, і вже знаючи як змінюється y, обчислюємо, як слід змінювати (бо за умовою задачі ми не можемо змінюват a і b). У результаті знаходимо (або в думках, або формально обчислюючи wp), що при парних y величину x слід подвоювати, а при непарних - необхідно збільшувати значення змінної z на x.

Програма написана!

Текст програми: