Invariant (informatika)

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.

Jednoduchý příklad invariantu

Nejprve malý příklad pro ukázání, co to invariant vlastně je - vezměme si tento jednoduchý cyklus: int i = 0; while( i 0 ≤ i ≤ 10.

Definice

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í. +more *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é. +more 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 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

Reference

Kategorie:Informatika