інваріант циклу

Програмісти часто складають цикли, як правило, щоб досягти якоїсь конкретної мети: знайти елемент із заданими властивостями, виконати сортування і т. П. Але як переконатися в тому, що мета буде досягнута, не виконуючи цикл безпосередньо? У цьому нам допоможе інваріант циклу.

Інваріант циклу - це твердження, що відноситься до змінних програми, яке залишається істинним на початку і в кінці виконання кожної ітерації циклу.

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

Нехай є масив a. що складається з n елементів. Введемо змінну TemporarySmallest (індекс елемента, в даний момент є найменшим) і покладемо її рівною 0 перед початком перевірки. Далі, будемо порівнювати a [TemporarySmallest] послідовно з a [1], a [2]. a [n-1]. Якщо виявиться, що a [TemporarySmallest] більше будь-якого з a [k]. то відновимо значення TemporarySmallest. Позначимо зміною nextToCheck індекс елемента, що підлягає перевірці.

Інваріант циклу буде виглядати так:

  1. TemporarySmallest знаходиться всередині [0, nextToCheck),
  2. і для всіх k з [0, nextToCheck) виконується A [k]> = A [TemporarySmallest].

[A, b) означає: всі цілі числа, що знаходяться на проміжку від a до b. включаючи a. але не включаючи b.

Іншими словами: найменший елемент масиву з відомим індексом TemporarySmallest знаходиться всередині дослідженого проміжку [0, nextToCheck). Це твердження має залишатися істинним на початку і в кінці кожної ітерації.

Ініціалізіруем змінні, що входять до інваріант, так, щоб він був справжнім до початку виконання циклу:

-- індекс найменшого елемента дорівнює 0. і це єдиний елемент в дослідженому проміжку [0,1). Поки інваріант зберігається.

На кожному кроці циклу значення nextToCheck збільшується на 1. і, при необхідності, змінюється TemporarySmallest:

-- так, щоб інваріант циклу залишався справжнім в кінці кожної ітерації. Отже, і після закінчення циклу інваріант збережеться - найменший елемент масиву з відомим індексом TemporarySmallest буде знаходитися всередині дослідженого проміжку [0, nextToCheck).

Умовою закінчення циклу є відсутність в масиві a елементів, які слід перевірити: nextToCheck == n. Таким чином, збереження інваріанта циклу гарантує нам, що після закінчення циклу (вичерпання елементів, які слід перевірити) буде знайдений індекс найменшого елемента TemporarySmallest - досягнута мета циклу. Це можна записати як

інваріант циклу Условіе_окончанія_цікла => Мета циклу

Замість умови закінчення можна використовувати умова виконання циклу. У нашому випадку це: nextToCheck

інваріант циклу ! (Условіе_виполненія_цікла) => Мета циклу

Таким чином, підібравши інваріант циклу і забезпечивши його збереження, ми можемо гарантувати досягнення мети, не виконуючи сам цикл.

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

Питання для самоперевірки при складанні циклів:

  • Чи є інваріант циклу істинним до початку циклу (ініціалізовані чи належним чином nextToCheck і TemporarySmallest)?
  • Для довільної ітерації: чи є інваріант циклу істинним на вході в тіло циклу, і після виходу з нього?
  • Чи відбувається рух у напрямку до закінчення виконання циклу (инкрементируется чи індекс nextToCheck в тілі циклу)?
  • Чи приводить збереження інваріанта циклу і умови закінчення циклу до досягнення мети?

При складанні циклів може виявитися зручним поняття області невизначеності. що використовується в обчислювальних методах математики. Область зміни параметрів задачі (в нашому прикладі: [0, n)) можна розділити на дві частини: досліджену область (для якої знайдено TemporarySmallest. [0, nextToCheck)) і область невизначеності ([nextToCheck, n)). Необхідно складати цикл так, щоб на кожній ітерації область невизначеності скорочувалася.

Повернемося до нашого прикладу. На початку першої ітерації досліджена область представляла собою єдину точку 0. а область невизначеності становила [1, n). На другому кроці область невизначеності скоротилася до [2, n). на третьому - до [3, n) і т. д. поки, нарешті, не перетворилася на порожній безліч, що не містить точок.

Розглянемо ще один приклад - сортування вибором по спадаючій. Нехай, потрібно впорядкувати масив a з n цілих чисел. Знайдемо найменший елемент і помістимо його в кінець масиву, на позицію n-1. Потім серед решти елементів знову виберемо найменший і помістимо його на позицію n-2 і т. Д. На i -й ітерації відсортовані елементи будуть займати позиції від i до n-1. а що залишилися невибраними - від 0 to i-1.

Для пошуку найменшого елемента використовуємо функцію FindMin (int a [], int n). повертає індекс найменшого елемента і написану на основі розглянутого вище прикладу. Введемо змінну numSorted. позначає кількість відсортованих елементів масиву.

Інваріант циклу буде таким:

  1. numSorted найменших елементів масиву відсортовані в порядку спадання на проміжку [n-numSorted, n),
  2. залишилися елементи масиву знаходяться на проміжку [0, n-numSorted).

Безпосередньо перед циклом инициализируем значення numSorted:

що робить інваріант циклу істинним.

На кожній ітерації кількість numSorted збільшується на одиницю. Щоб цього досягти, вибирається найменший серед перших [0, n-numSorted) невідсортованих елементів, і змінюється місцями (за допомогою функції swap ()) c елементом n-numSorted

Таким чином, відсортоване "хвіст" масиву щоразу подовжується на один елемент, а не відсортованого "голова" зменшується.

Цикл закінчується після досягнення numSorted == n.

що почитати

Схожі статті