Potenssinkorotuksen oikeellisuus (yksityiskohtia)
Tarkastellaan ohjelman toimintaa annetulla syötteellä n. Huomataan, että ennen while-silmukan suoritusta muuttujien m ja i arvot toteuttavat ehdon P0 = {m = 1, i = n}, ja tavoitteena on osoittaa, että silmukan suorituksen jälkeen muuttujan m arvo toteuttaa ehdon P1 = {m = 2n}.
Tämä voidaan todeta osoittamalla, että jokainen silmukan suorituskerta pitää voimassa muuttujien suhdetta koskevan silmukkainvariantin I = {m*2i = 2n}.
Ehto I on nimittäin selvästi voimassa silmukan suorituksen alussa (P0 Þ I) ja yhdessä silmukan lopetusehdon {i = 0} kanssa se takaa halutun lopputuloksen (I & {i = 0} Þ P1).
Oletetaan siis, että muuttujien m ja i arvot toteuttavat ehdon I silmukan jonkin suorituskerran alussa. Silmukan rungossa muuttujille sijoitetaan uudet arvot m’ = 2*m ja i’ = i-1. Mutta tällöin myös nämä uudet arvot toteuttavat ehdon I:
m’*2i’ = (2*m)*2i-1 = m*2i = 2n.
Siten jokainen silmukan suorituskerta säilyttää invariantin I.