Invariant (informatika)

Definice

Invariant cyklu je mezilehlá podmínka v algoritmu, která je v daném bodě výpočtu splněna v každém průchodu cyklem.

Invariant cyklu se používá abychom pochopili proč je algoritmus korektní.O invariantu cyklu musíme říct tři věci:

Inicializace : Platí před první iterací cyklu.
Průbeh : Pokud platí pred iterací cyklu, zůstane platit i před další iterací.
Zakončení: Když cyklus skončí, invariant nám dá užitečnou vlastnost k dokázání korektnosti algoritmu.

Pokud platí první dvě části, invariant cyklu platí během každé iterace cyklu. Třetí vlastnost je možná nejdůležitější, protože jí používáme k dokázání korektnosti algoritmu.

Příklad

Takovým příkladem invariantu by mohlo být prakticky cokoli i např. Slunce je žluté. Je to podmínka která platí pořád. Při určování invariantu cyklu však musíme dbát o to, aby se námi zvolený invariant vztahoval k danému algoritmu.
Ukažme si teď příklad invariantu cyklu na tomhle jednoduchém algoritmu:

z=x
j=o

while j<y do
z=z-1
j=j+1

Invariant tohoto cyklu je z=x-j , teď si po jednotlivých krocích vysvětlíme proč tomu tak je.
1. Před první iterací máme:
Z" = X"
Z" = X" - 0
Z" = X" - J"

(Pro počáteční hodnotu proměnných x,z,j používám ")

2. Po první iteraci cyklu:
Z = Z" + 1 a J = J" + 1
Když si přeuspořádáme tyhle rovnice tak dostaneme Z" = Z - 1 a J" = J + 1
Teď, když začneme s rovnicí Z" = X" - J"
o které už víme, že je vždy pravdivá, můžeme nahradit Z - 1 za Z" a J" = J + 1 a dostáváme:

Z - 1 = X" - (J+1)
Z - 1 = X" - J - 1
Z = X" - J

A po n iteracích dostáváme:
Z - N = X" - (J+N)
Z - N = X" - J - N
Z = X" - J

A co dělá tenhle invariant užitečným je to,že po poslední iteraci cyklu J = Y" . Podmínka zněla,že cyklus pokračuje pokud J<Y" a J se zvyšuje o 1 každým průchodem cyklu takže když J=Y"
dostáváme se z cykle von.Takže proto můžeme J nahradit Y"-em a dostáváme:
Z = X" - J = X" - Y" což je přesně to co jsme chtěli dokázat.
--Puchly jozef 22. 4. 2010, 13:15 (UTC)