A programozás során a ciklus olyan utasítás, amely lehetővé teszi a program egy részének végrehajtásának megismétlését . A hurokinvariáns olyan tulajdonság, amely minden ismétlés előtt és után igaz. Ez egy logikai tulajdonság, amely lehetővé teszi egy program vagy algoritmus tanulmányozását .
A formális ellenőrzés során, különösen a Hoare logikában , a hurkok invariánsai logikai predikátumok , amelyek az őket használó algoritmusok , különösen ezen algoritmusok helyességének igazolására szolgálnak .
A hurokinvariánsnak igaznak kell lennie a hurok indítása előtt, és ezután garantáltan helyes marad a ciklus minden iterációja után. Különösen az invariáns mindig igaz lesz a hurok végén. Mivel a ciklusok és a rekurzió alapvetően hasonlóak, nincs sok különbség a hurok invariánsának bizonyítása és az indukciós érvelés segítségével a program helyes igazolása között . A gyakorlatban a hurokinvariáns gyakran az indukciós tulajdonság - az indukciós hipotézis -, amellyel azt mutatják be, hogy a rekurzív program ekvivalens egy hurokkal.
A C program max()az argumentuma legnagyobb elemének, a tömbnek az értékét adja vissza a[], ha mérete nlegalább 1.
A program 3., 6., 9., 11. és 13. sorában egy megjegyzés tulajdonságot ad a kód végrehajtásának ebben a szakaszában. A 6 és 11 vonalak tulajdonságai szó szerint megegyeznek, tehát az 5. és 12. vonal közötti hurok invariánsának számít. A 13. vonal elérésekor az invariáns továbbra is érvényes, és tudjuk, hogy az i!=n5. vonal folytatási feltétele hamis; ez a két tulajdonság azt jelenti, hogy mmegegyezik a maximális in értékkel a[0...n-1], azzal az értékkel , amelyet a függvénynek kell kiszámítania, hogy a helyes érték visszatérjen a 14. sorba.
int max(int n, const int a[]) { int m = a[0]; // m est égal à la valeur maximale de a[0...0] int i = 1; while (i != n) { // m est égal à la valeur maximale de a[0...i-1] if (m < a[i]) m = a[i]; // m est égal à la valeur maximale de a[0...i] ++i; // m est égal à la valeur maximale de a[0...i-1] } // m est égal à la valeur maximale de a[0...i-1], et i==n return m; }Ha a védekező programozási paradigma követték, a hurok állapotát i!=n5. sor kellene i<n, hogy legyen annak érdekében, hogy elkerüljék a végtelen hurkot negatív, elméletileg tilos, értékeit n. Még akkor is, ha intuitív módon nem kellene különbséget tennie, a bizonyítás kissé bonyolultabbá válik, mivel csak a i>=n13. sor biztos. Ennek i<=na feltételnek a megszerzéséhez hozzá kell adni a ciklus invariánsát. Egyszerű látni, hogy i<=nez is hurokinvariáns, mivel a i<n6-os vonal megszerezhető az 5-ös vonal (módosított) hurokfeltételéből, és így a i<=n11-es vonalat megtartja, miután a 10-es vonal inövekszik. formálisan az ellenőrző programok számára, olyan nyilvánvaló tulajdonságokat, i<=namelyeket gyakran figyelmen kívül hagytak.
Az Eiffel nyelv natív módon támogatást nyújt a hurok invariánsainak. A hurok invariánsokat az osztály invariánsainak hasonló szintaxissal fejezzük ki . Az alábbi példában a ciklus invariáns kifejezésnek x <= 10igaznak kell lennie az inicializálás után, majd a hurok minden végrehajtása után, és ezt futás közben ellenőrzik.
from x := 0 invariant x <= 10 until x >= 10 loop x := x + 1 end