Kako se u svakoj iteraciji promenljive z1 i z2 množe sa dva, može se pokazati da pre svake iteracije prve petlje važi:
z1(n) = z1(0) * 2n = y * 2n
z2(n) = z2(0) * 2n = 2n
pri čemu je z1(n) vrednost promenljive z1 nakon n-te iteracije prve petlje a z1(0) njena vrednost pre prvog ulaska u prvu petlju. Na taj način se izvodi sledeća jednakost koja važi u tački N:
(1) z1 = y * 2n i z2 = 2n
Ove veze mogu biti kombinovane u sledeću jednakost:
(2) {z1 = y * z2}
koja važi u tački N.
Dokažimo da je to ujedno i invarijanta prve petlje:
Kako inicijalno z1 dobija vrednost y a z2 dobija vrednost 1 to je jednakost (2)(trivijalno) ispunjena pre prvog ulaska u petlju. Dokažimo da ukoliko je jednakost (2) ispunjena pre nekog ulaska u petlju, onda je ona ispunjena i nakon (jednog) izvršenja tela petlje:
Označimo sa z1' vrednost promenljive z1 nakon izvršavanja odgovarajuće iteracije a sa z2' vrednost promenljive z2 nakon izvršavanja te iste iteracije. Tada tvrđenje važi na osnovu sledećih jednakosti:
z1' = 2 * z1 = 2 * y * z2 = y * 2 * z2 = y * z2'
čime je dokazano da je jednakost (2)ujedno i invarijanta prve petlje.
Dodatne jednakosti koje (trivijalno) važe u tački N su:
(3) r = x i q = 0.
Izvođenje invarijante druge petlje:
Pre prvog ulaska u drugu petlju i nakon svake njene iteracije važe sledeće relacije:
z1(m) = z1(0) / 2m
z2(m) = z2(0) / 2m
pri čemu je z1(m) vrednost promenljive z1 nakon m-te iteracije druge petlje, a z1(0) njena vrednost pre prvog ulaska u drugu petlju. Iz jednakosti (1) dobijamo vrednosti za z1(0) i z2(0):
z1(0) = y * 2n i z2(0) = 2n
odakle dobijamo sledeću jednakost koja važi u tački M:
(4) z1 = y * 2n/2m i z2 = 2n/2m i z1 = y * z2
Korišćenjem iste tehnike za r i q, dobijamo rekurzivnu relaciju
r(m) = r(m-1) + [if (z1(m-1) ≤ r(m-1)) then -z1(m-1) else 0 ]
q(m) = q(m-1) + [if (z1(m-1) ≤ r(m-1)) then z2(m-1) else 0 ]
Ako se ove jednakosti razviju u izraze korišćenjem suma, ako zamenimo -z1(m-1) sa -y*z2(m-1) (na osnovu (4)) i ako izdvojimo zajednički faktor -y ispred zagrade, dobijamo:
r(m) = r(0) - y * ∑ [if (z1(i-1) ≤ r(i-1)) then z2(i-1) else 0 ] za i = 1 do m
q(m) = q(0)+ ∑ [if (z1(i-1) ≤ r(i-1)) then z2(i-1) else 0 ] za i = 1 do m
Uprošćavanjem dobijamo sledeću jednakost u tački M:
r(m) - r(0) = - y * (q(m) - q(0))
Vrednosti za r(0) i q(0) u tački M mogu se izvesti razmatranjem dve moguće putanje u tačku M iz if naredbe koja joj prethodi:
Ako se dobijene vrednosti za r(0) i q(0) uvrste u gornju jednakost, u oba slučaja se dobija r(m) - x = -y * q(m).
Dakle, u tački M važi sledeća jednakost, kako pre prvog ulaska u drugu petlju tako i nakon svake iteracije druge petlje:
(5) x = q * y + r.
Nakon izlaska iz prve petlje važiće uslov r ≤ z1. Ukoliko je r = z1, r će biti umanjeno za z1 što znači da će u tački M, pre prvog ulaska u drugu petlju važiti r < z1.
Dokažimo da će uslov
(6) r < z1
ukoliko važi pre nekog ulaska u petlju, važiti i nakon (jednog) izvršavanja tela petlje:
Neka je r' vrednost promenljive r nakon određene iteracije, a z1' vrednost promenljive z1 nakon iste iteracije. Tada važi sledeće:
z1' = z1 / 2 .
Razlikujemo dve moguće putanje koje slede iz if naredbe u petlji:
Dakle, uslov (6) će važiti nakon svake iteracije druge petlje.
Takođe, kako se inicijalno r postavlja na x koje je veće od ili jednako 0, i kako se pre ulaska prvi put u drugu petlju r umanjuje za z1 samo ako je z1 ≤ r, važiće da je r ≥ 0. Takođe, kako se u svakoj iteraciji druge petlje r umanjuje za z1 samo ako je z1 ≤ r, to će nakon svake iteracije važiti r ≥ 0.
Tako se dobija sledeća relacija koja važi u tački M:
(7) {x = q * y + r, 0 ≤ r < z1}
za koju smo pokazali da važi pre prvog ulaska u drugu petlju i da važi nakon svakog prolaska kroz drugu petlju, pa je ona ujedno i invarijanta druge petlje.
Dokaz parcijalne korektnosti programa:
Dokažimo sada da su to korisne invarijante, odnosno dokažimo parcijalnu korektnost programa. Potrebno je dokazati da će za proizvoljne ulazne vrednosti promenljivih x i y koje ispunjavaju preduslov, pod pretpostavkom da se program zaustavi, biti ispunjen pauslov programa.
Ukoliko promenljiva y ne ispunjavaja preduslov programa, odnosno ako je y ≤ 0 onda će prva petlja biti beskonačna pa se program neće zaustaviti. Ukoliko promenljiva x ne ispunjavaja preduslov programa, odnosno ako je x < 0, tada neće biti ispunjen uslov r ≥ 0 jer se inicijalno r postavlja na x, pa relacija (7) neće biti invarijanta petlje.
U slučaju da promenljive x i y ispunjavaju preduslov, navedene relacije (2) i (7) su njihove invarijante. U trenutku kada je uslov izlaska iz druge petlje ispunjen, a to je za z2 = 1 , tada važi z1 = y (na osnovu (4)) pa invarijanta u tački M vodi u pauslov, odnosno važi:
{x = q * y + r, 0 ≤ r < y}
što znači da je program parcijalno korektan.
Naredna: Pseudokod programa Gore: Hardverdsko celobrojno deljenje Prethodna: Invarijanta petlje (izvođenje iz brojača) Sadržaj