В інформатиці інваріант циклу — властивість циклу в програмі, яка є істинною до (і після) кожної ітерації. Це , яке в програмному коді іноді перевіряють за допомогою інструкції перевірки тверджень. Знання інваріанта(ів) важливе для розуміння того, як виконується цикл.
У формальній верифікації програм, зокрема в підході Флойда — Гоара, інваріанти циклів виражають формальною логікою предикатів і використовують для доведення властивостей циклів, а також алгоритмами розширення, що використовують цикли (зазвичай властивості ). Інваріанти циклів будуть істинними при вході в цикл і після кожної ітерації, так що при виході з циклу можна гарантувати як інваріанти циклу, так і умову завершення циклу.
З погляду методології програмування, інваріант циклу можна розглядати як більш абстрактну специфікацію циклу, яка характеризує глибше призначення циклу, що виходить за рамки деталей цієї реалізації. Оглядова стаття охоплює фундаментальні алгоритми з багатьох галузей інформатики (пошук, сортування, оптимізація, арифметика тощо), характеризуючи кожен з них з точки зору його інваріанта.
Через схожість циклів та рекурсивних програм, доведення часткової правильності циклів з інваріантами дуже схоже на доведення правильності рекурсивних програм за допомогою індукції. Фактично, інваріант циклу часто збігається з індуктивною гіпотезою, яку потрібно довести для рекурсивної програми, еквівалентної даному циклу.
Неформальний приклад Наведена підпрограма мовою C max() повертає максимальне значення в масиві аргументів a[], за умови, що його довжина n не менша від 1. В рядках 3, 6, 9, 11 та 13 є коментарі. Кожен коментар містить твердження про значення однієї або кількох змінних на цьому етапі функції. На початку та в кінці циклу (рядки 6 та 11) виділено однакові твердження. Отже, вони описують інваріантну властивість циклу. Коли досягнуто рядка 13, цей інваріант все ще виконується, і відомо, що умова циклу i! =n з рядка 5 стала хибною. Обидві властивості разом означають, що m дорівнює максимальному значенню в a[0...n-1], тобто, що правильне значення повертається з рядка 14.int max(int n, const int a[]) { int m = a; // m equals the maximum value in a[0...0] int i = 1; while (i != n) { // m equals the maximum value in a[0...i-1] if (m < a[i]) m = a[i]; // m equals the maximum value in a[0...i] ++i; // m equals the maximum value in a[0...i-1]
// m equals the maximum value in a[0...i-1], and i==n return m; }Дотримуючись парадигми безпечного програмування, умову циклу i! =n у рядку 5 краще змінити на i<n, щоб уникнути нескінченного циклу для некоректних від'ємних значень n. Попри те, що інтуїтивно ця зміна в програмі не мала б нічого змінити, міркування, що ведуть до її правильності, дещо ускладнюються, оскільки тоді в рядку 13 відомо лише i>=n. Щоб можна було стверджувати, що виконується нерівність i<=n, її необхідно додати до інваріанта циклу. Легко побачити, що i<=n також є інваріантом циклу, оскільки i<n у рядку 6 можна отримати зі (зміненої) умови циклу в рядку 5, і тому i<=n виконується в рядку 11 після інкременту i в рядку 10. Однак, коли для формальної перевірки програми інваріанти циклу доводиться надавати вручну, такими інтуїтивно очевидними властивостями, як i<=n, часто нехтують.
Логіка Флойда — Гоара У логіці Флойда — Гоара циклу з передумовою визначається таким правилом висновування:
Це означає:
Якщо деяка властивість зберігається під час виконання коду — точніше, якщо залишається істинною після виконання щоразу, коли і , і були істинними до цього — (верхній рядок), то та гарантовано будуть відповідно хибним та істинним після виконання всього циклу , за умови, що було істинним до початку циклу (нижній рядок).
Іншими словами: наведене вище правило є дедуктивним кроком, передумовою якого є трійка Гоара Ця трійка насправді є на станах машини. Вона має місце щоразу, коли, починаючи зі стану, в якому булівський вираз є істинним, успішно виконується певний код під назвою , після чого машина переходить у стан, у якому є істинним. Якщо це співвідношення можна довести, то правило дає нам змогу зробити висновок, що успішне виконання програми призведе від стану, в якому істинне, до стану, в якому істинне . Булева формула в цьому правилі називається інваріантом циклу.
З деякими варіаціями у позначеннях та з передумовою, що цикл зупиняється, це правило також відоме як теорема про інваріантне відношення. Один підручник 1970-х років так представляє його в доступний для студентів-програмістів спосіб:
Нехай позначення P { seq } Q означає, що якщо P істинне до виконання послідовності операторів seq, то Q істинне після нього. Тоді теорема про інваріантне відношення стверджує, що
P & c { seq } P означає, що P { DO WHILE (c); seq END; } P & ¬c
Приклад Наведемо приклад, що ілюструє, як працює це правило. Розгляньмо програму: поки (x < 10) x := x+1; Тоді можна довести таку трійку Гоара:
Умова C циклу while така: . Корисний інваріант циклу потрібно вгадати; доречним виявляється . За цих припущень можна довести таку трійку Гоара:
Хоча цю трійку можна формально вивести з правил логіки Флойда — Гоара, що регулюють присвоєння, вона також інтуїтивно виправдана: обчислення починається у стані, коли істинне, що просто означає, що є істинним. Обчислення додає 1 до , що означає, що все ще є істинним (для цілого x).
Згідно з цією передумовою, правило для циклів while дає змогу зробити такий висновок:
Однак, післяумова ( менше або дорівнює 10, але не менше 10) логічно еквівалентна , що ми й хотіли показати.
Властивість також є інваріантом циклу з прикладу, а тривіальна властивість — ще одним. Застосування наведеного вище правила виведення до першого інваріанта дає Застосовуючи це до інваріанта дає трохи виразніше.
Підтримка в мовах програмування
Eiffel Мова програмування Eiffel має вбудовану підтримку інваріантів циклів. Інваріант циклу виражається тим самим синтаксисом, що й . У наведеному нижче прикладі інваріант циклу x <= 10 має бути істинним після ініціалізації циклу та після кожного виконання тіла циклу; це перевіряється під час виконання. from x := 0 invariant x <= 10 until x > 10 loop x := x + 1 end
Whiley Мова програмування також забезпечує вбудовану підтримку інваріантів циклів. Їх виражають за допомогою одного або кількох речень where, як показано нижче:function max(int[] items) -> (int r) // Requires at least one element to compute max requires |items| > 0 // (1) Result is not smaller than any element ensures all { i in 0..|items| | items[i] <= r } // (2) Result matches at least one element ensures some { i in 0..|items| | items[i] == r }: // nat i = 1 int m = items // while i < |items| // (1) No item seen so far is larger than m where all { k in 0..i | items[k] <= m } // (2) One or more items seen so far matches m where some { k in 0..i | items[k] == m }: if items[i] > m: m = items[i] i = i + 1 // return mФункція max() визначає найбільший елемент у цілочисельному масиві. Щоб він був визначеним, масив повинен містити принаймні один елемент. Післяумови max() вимагають, щоб повернене значення було: (1) не меншим за будь-який елемент; та (2) щоб воно дорівнювало принаймні одному елементу. Інваріант циклу визначається індуктивно через два оператори where, кожен з яких відповідає оператору в післяумові. Фундаментальна відмінність полягає в тому, що кожен оператор інваріанта циклу визначає результат як правильний до поточного елемента i, тоді як післяумови визначають результат як правильний для всіх елементів.
Використання інваріантів циклів Інваріант циклу може слугувати одній з таких цілей:
суто для документування; для перевірки в коді, наприклад, за допомогою виклику припущення; для перевірки на основі підходу Флойда — Гоара
Для випадку 1 достатньо коментаря природною мовою (наприклад, // m дорівнює найбільшому з a[0...i-1] у наведеному вище прикладі).
Для випадку 2 потрібна підтримка в мовах програмування, як-от бібліотека assert.h у C або показана вище вказівка invariant у Eiffel. Часто перевірку під час виконання можна вмикати (для налагоджувальних запусків) та вимикати (для робочих запусків) як параметр компілятора або середовища виконання.
Для випадку 3 існують деякі інструменти для підтримки математичних доведень, зазвичай заснованих на згаданому вище правилі Флойда — Гоара, що заданий код циклу справді задовольняє заданий (набір) інваріант(ів) циклу.
Для автоматичного виявлення інваріантів циклу заданого коду можна використати техніку . Однак цей підхід обмежений дуже простими інваріантами (як-от 0<=i && i<=n && i%2==0).
Відмінність від коду, інваріантного до циклу
Код, інваріантний до циклу, включає команди або інструкції, які можна перемістити за межі тіла циклу, не вплинувши на семантику програми. Такі перетворення, які називаються , виконують для оптимізації програм деякі компілятори. Приклад коду, інваріантного до циклу (мовою програмування C):for (int i=0; i<n; ++i) { x = y+z; a[i] = 6*i + x*x; }де обчислення x = y+z та x*x можна виконати перед циклом, що дасть еквівалентну, але швидшу програму:x = y+z; t1 = x*x; for (int i=0; i<n; ++i) { a[i] = 6*i + t1; }На противагу цьому, наприклад, властивість 0<=i && i<=n є інваріантом циклу як для початкової, так і для оптимізованої програми, але не є частиною коду, тому немає сенсу говорити про «переміщення її з циклу».
Код, інваріантний до циклу, може привести до появи відповідної властивості, інваріантної до циклу. Для наведеного вище прикладу найпростіший спосіб побачити це — розглянути програму, де код, інваріантний до циклу, обчислюється як до, так і всередині циклу:x1 = y+z; t1 = x1*x1; for (int i=0; i<n; ++i) { x2 = y+z; a[i] = 6*i + t1; }Властивість цього коду, інваріантна до циклу, має вигляд (x1==x2 && t1==x2*x2) || i==0, що вказує на те, що значення, обчислені перед циклом, збігаються зі значеннями, обчисленими всередині (за винятком випадків, коли значення обчислюються до першої ітерації).
Див. також Інваріант (математика)
Примітки
Література Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest, and Clifford Stein. Introduction to Algorithms, Second Edition. MIT Press and McGraw-Hill, 2001. ISBN 0-262-03293-7. Pages 17–19, section 2.1: Insertion sort. David Gries. «A note on a standard strategy for developing loop invariants and loops.» Science of Computer Programming, vol 2, pp. 207–214. 1984. Michael D. Ernst, Jake Cockrell, William G. Griswold, David Notkin. «Dynamically Discovering Likely Program Invariants to Support Program Evolution.» International Conference on Software Engineering, pp. 213–224. 1999. Robert Paige. «Programming with Invariants.» IEEE Software, 3(1):56–69. January 1986. Yanhong A. Liu, Scott D. Stoller, and Tim Teitelbaum. Strengthening Invariants for Efficient Computation. Science of Computer Programming, 41(2):139–172. October 2001. Michael Huth, Mark Ryan. «Logic in Computer Science.», Second Edition.