Naredna: Dokaz zaustavljanja programa Gore: NZD Prethodna: Invarijanta petlje   Sadržaj

Dokaz parcijalne korektnosti programa

Dokažimo da uslov NZD(p,q)=NZD(x,y) jeste invarijanta petlje polaznog programa za proizvoljan ulaz. Ono što treba da dokažemo je da svaki put kada se ulazi u petlju važi navedeni uslov.

1. Uspostavljanje invarijante. Najpre treba da dokažemo da prvi put kada naiđemo na ulazak u petlju važi uslov NZD(p,q)=NZD(x,y). To je ispunjeno, jer pre prvog ulaska u petlju postoje dve naredbe dodele (p dobija veću vrednost od x i y, a q manju), i kako važi da je NZD(x,y)=NZD(y,x) za proizvoljne brojeve x i y, to onda važi i odgovarajući uslov, odnosno NZD(p,q)=NZD(x,y).

2. Održavanje invarijante. Dalje treba da dokažemo sledeće: ako uslov NZD(p,q)=NZD(x,y) važi pre nekog ulaska u petlju, onda važi i nakon (jednog) izvršavanja tela petlje.
U tom cilju dokažimo sledeću lemu:

Lema: Za proizvoljne prirodne brojeve prvi i drugi važi sledeća jednakost:

NZD(prvi,drugi) = NZD(drugi,ostatak), pri čemu je prvi = k * drugi + ostatak

za neki prirodan broj k.

Dokaz:

Pretpostavimo da je NZD(prvi,drugi)=q.
Tada važi da q|prvi i q|drugi pa odatle važi i da q|drugi i q|ostatak zato što je ostatak=prvi-k*drugi.
Dokažimo sada da je q=NZD(drugi,ostatak). Pretpostavimo suprotno, tj. pretpostavimo da postoji veći zajednički delilac p za drugi i ostatak (p>q). Tada p|drugi i p|ostatak pa p|prvi zato što je prvi=k*drugi+ostatak. Dakle, p je zajednički delilac i za prvi i za drugi pa q nije NZD(prvi,drugi) zato što postoji p koji je veći od q i zajednički je delilac za prvi i drugi, a to je suprotno od pretpostavke da je NZD(prvi,drugi)=q. Dakle, polazna pretpostavka nije tačna, odnosno q=NZD(drugi,ostatak).

Time je dokazana lema. Dokažimo sada tvrđenje ako uslov NZD(p,q)=NZD(x,y) važi pre nekog ulaska u petlju, onda važi i nakon (jednog) izvršavanja tela petlje.

Označimo sa p' vrednost promenljive p nakon izvršavanja odgovarajuće iteracije, a sa q' vrednost promenljive q nakon izvršavanja te iste iteracije.

Tada tvđenje važi na osnovu sledećih jednakosti:

NZD(x,y) = NZD(p,q) = NZD(q,p mod q) = NZD(p',q')

Pri tome, za prvu jednakost korišćena je pretpostavka da uslov važi pre ulaska u petlju, a za drugu je korišćena gore dokazana lema.

3. Ostvarivanje željenog pauslova - Ako se izvršavanje petlje okonča, odnosno ako uslov ulaska u petlju nije ispunjen, tada je q=0 i program se zaustavlja i važi da je NZD(x,y)=NZD(p,0)=p. Nakon dodele z=p važi z=NZD(x,y).

To dokazuje da program zadovoljava uslove specifikacije i time je dokazana parcijalna korektnost programa.

Naredna: Dokaz zaustavljanja programa Gore: NZD Prethodna: Invarijanta petlje   Sadržaj