Invariant (informatika)

Z Wikipedie, otevřené encyklopedie
Skočit na: Navigace, Hledání

Invariant je podmínka v algoritmu, která musí být splněna po celou dobu běhu programu.

Invariant cyklu je mezilehlá podmínka v algoritmu, která musí být splněna před vykonáním a po vykonání každého průchodu cyklem. [1]

Jednoduchý příklad invariantu[editovat | editovat zdroj]

Nejprve malý příklad pro ukázání, co to invariant vlastně je −vezměme si tento jednoduchý cyklus:[2]

int i = 0;
while( i < 10 ){
  i++;
}
// i = 10

Podmínkou, která platí na začátku i na konci každého průchodu cyklem, zde zřejmě bude: 0 ≤ i ≤ 10

Definice[editovat | editovat zdroj]

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ůběh : Pokud platí před 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[editovat | editovat zdroj]

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.

Příklad invariantu cyklu na tomto algoritmu:

z=x
j=0

while j<z 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 tyto rovnice tak dostaneme Z" = Z + 1 a J" = J −1
Nyní, když začneme s rovnicí Z" = X" −J"
o které 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

Tento invariant je užitečným tím, ž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 cyklu ven. 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.

Reference[editovat | editovat zdroj]

  1. MCCLOSKEY, Robert. [cit. 2013-05-08]. Dostupné online. (anglicky) 
  2. WISMAN, Raymond. [cit. 2013-05-08]. Dostupné online. (anglicky)