loop invariant

Angol

Főnév

loop invariant (tsz. loop invariants)

(informatika) A loop invariant (magyarul: ciklusinvariáns) egy olyan állítás vagy logikai feltétel, amely:

igaz a ciklus minden egyes iterációjának elején (és gyakran végén is),
nem változik a ciklus végrehajtása során – azaz invariáns.

Ez a fogalom kulcsfontosságú a programhelyesség formális bizonyításában (pl. Hoare-logika), és szintén szerepet játszik optimalizálásban, például a loop invariant code motion során.

🧪 Hétköznapi példa

Vegyünk egy egyszerű ciklust:

int sum = 0;
for (int i = 1; i <= n; i++) {
    sum += i;
}

Loop invariant példa:

A ciklus minden lépésénél a sum értéke megegyezik az 1 + 2 + ... + (i - 1) összeggel.

Ez igaz az elején, megmarad minden iteráción, és a ciklus végén segít bizonyítani, hogy a sum == 1 + 2 + ... + n.

🎯 Miért hasznos a ciklusinvariáns?

1. Programhelyesség-bizonyítás

Segítségével formálisan igazolható, hogy a ciklus azt teszi, amit elvárunk tőle.

2. Fordítóoptimalizálás

Ha egy kifejezés nem függ a ciklusváltozótól, akkor a fordító kiemelheti a cikluson kívülre, csökkentve a futásidőt (loop-invariant code motion).

3. Ciklusok újraformálása

Elemző eszközök felismerhetik, ha egy ciklus felesleges számításokat végez, vagy állandó értékeket újraszámol.

📐 Formális definíció (Hoare-logika)

A ciklus invariáns I egy állítás, amely:

igaz az előfeltételből indulva, még mielőtt a ciklus elkezdődne: {P} while (cond) { C } {Q}
megmarad minden cikluslépés után: {I ∧ cond} C {I}
és ha a ciklus feltétele már nem igaz, akkor az invariáns + ¬cond ⇒ utófeltétel: I ∧ ¬cond ⇒ Q

📌 Klasszikus példák

1. Szorzás összeadásként

int a = 0;
for (int i = 0; i < n; i++) {
    a += x;
}

Invariáns:

a == i * x

Ez megmarad minden iteráción: a növekszik x-szel, i nő 1-gyel → szorzás.

2. Faktor számítása

int fact = 1;
for (int i = 1; i <= n; i++) {
    fact *= i;
}

Invariáns:

fact == i! / n! * n! Vagy egyszerűbben: fact == 1 * 2 * ... * (i - 1)

🧮 Hogyan találjunk invariánst?

Figyeld meg, mi változik és mi marad állandó a ciklusban.
Próbálj rekurzív vagy kumulatív viszonyt keresni a változók között.
Teszteld az elején, közepén, végén – igaz-e minden lépésnél?

🔍 Loop-Invariant Code Motion (LICM)

A fordítóoptimalizálás során azokat a kifejezéseket, amelyek nem függenek a ciklusváltozótól, áthelyezhetjük a ciklus elé.

Példa:

for (int i = 0; i < n; i++) {
    y = x * z;  // nincs szükség újraszámolásra
    A[i] = y + i;
}

Optimalizált:

y = x * z;
for (int i = 0; i < n; i++) {
    A[i] = y + i;
}

🧠 Ciklusinvariáns + Verifikáció: Teljes helyesség

Ha egy ciklusinvariánst jól választunk, akkor a ciklus:

nem fut végtelenül (terminál),
mindig megőrzi a helyes állapotot,
garantálja, hogy a specifikáció teljesül.

Ez az algoritmusok formális bizonyításának egyik legfontosabb eszköze.

🔬 Nehézségek

Túl bonyolult állapotterek esetén nehéz megfogalmazni.
Ciklusok, amelyek nem lineárisak vagy rejtett függőségek vannak → invariáns nehezen található.
Bizonyos állítások csak összetett matematikai logikával fogalmazhatók meg.

TL;DR

A loop invariant egy olyan logikai állítás, amely igaz a ciklus minden iterációja előtt és után, és segít bizonyítani, hogy a ciklus helyesen működik. Kulcsfontosságú a programhelyesség formális ellenőrzéséhez, valamint a fordítóoptimalizálásokhoz is. Ha a ciklusinvariáns jól meghatározott, akkor segít bizonyítani, hogy a program pontosan azt teszi, amit elvárunk tőle – és hatékonyan is teszi.

További információk

loop invariant - Szótár.net (en-hu)
loop invariant - Sztaki (en-hu)
loop invariant - Merriam–Webster
loop invariant - Cambridge
loop invariant - WordNet
loop invariant - Яндекс (en-ru)
loop invariant - Google (en-hu)
loop invariant - Wikidata
loop invariant - Wikipédia (angol)