Dokažimo sada da svojstvo x=qy+r,r≥0 jeste invarijanta petlje polaznog programa za proizvoljan ulaz. Kao i u prethodnim primerima, ono što treba da dokažemo je da svaki put kada se ulazi u petlju važi dato svojstvo.
Dokaz se sprovodi u tri koraka:
1. Uspostavljanje invarijante - Najpre treba da dokažemo da prvi put kada naiđemo na ulazak u petlju važi uslov x=qy+r, r≥0. To je ispunjeno, jer pre prvog ulaska u petlju postoje dve naredbe dodele (q dobija vrednost 0 i r dobija vrednost x), pa kako važi da je x=0*y+x, x≥0 to znači da je x=qy+r, r≥0.
2. Održavanje invarijante - Dalje treba da dokažemo da ako uslov x=qy+r,r≥0 važi pre ulaska u petlju, onda važi i nakon (jednog) izvršavanja tela petlje. Označimo sa q' vrednost promenljive q nakon izvršavanja odgovarajuće iteracije, a sa r' vrednost promenljive r nakon izvršavanja te iste iteracije. Tada tvđenje važi na osnovu sledećih jednakosti:
x = q * y + r = q * y + r + y - y = (q + 1) * y + (r - y) = q' * y + r'
Pri tome, za prvu jednakost korišćena je pretpostavka da je uslov invarijante ispunjen pre iteracije.
Dokažimo još da važi i drugi deo uslova invarijante, tj. da je r≥0. Pre iteracije važi r≥0, a kako je uslov za ulazak u petlju ispunjen, to je r≥y pa je r-y≥0, odnosno r'≥0.
Ovim smo dokazali da svaki put kada se izračunava vrednost uslova ulaska u petlju, važi da je uslov x=qy+r,r≥0 ispunjen.
3. Ostvarivanje željenog pauslova - Ako se izvršavanje petlje okonča, odnosno ako je vrednost uslova ulaska u petlju netačna, tada je r<y i program se zaustavlja i važi da je x=qy+r,0≤r<y.
To dokazuje da program zadovoljava uslove specifikacije i time je dokazana parcijalna korektnost programa.
Naredna: Dokaz zaustavljanja programa Gore: Celobrojno deljenje Prethodna: Invarijanta petlje Sadržaj