loop invariant

loop invariant (tsz. loop invariants)

1. (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.

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.

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

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).

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

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

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.

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)

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

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é.

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

Optimalizált:

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

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.

• 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.

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.

• 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)