Invariant (informatika): Porovnání verzí
Smazaný obsah Přidaný obsah
Řádek 41:
Příklad invariantu cyklu na tomto algoritmu:
<pre>
z = x
j = 0
while j <
do z = z - 1
j = j + 1
</pre>
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"<br />▼
:Z" = X"
:Z" = X" −
(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 [[rovnice|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"
:Z
:Z + N = X" −(J-N)
▲A po n iteracích dostáváme:<br />
:Z + N = X"
:Z
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.
| |||