Naredna: Dokaz parcijalne korektnosti programa Gore: Selection sort Prethodna: Testiranje programa   Sadržaj

Invarijanta petlje

Analizom programa može se zaključiti da nakon svakog prolaska kroz unutrašnju for petlju važi da je i-ti element niza, pri čemu je i brojač u spoljašnjoj petlji, manji ili jednak od svih elemenata počev od i+1-og pa do j-tog, pri čemu je j brojač u unutrašnjoj petlji. To se može formalno zapisati sledećom nejednakošću: 
X[i] ≤ {X[i+1], X[i+2], ..., X[j]}

Takođe, nakon svakog prolaska kroz spoljašnju for petlju, može se zaključiti da važi da je podniz, počev od 0-tog pa do i-tog elementa uređen neopadajuće i da su svi ti elementi manji ili jednaki od svih preostalih elemenata u nizu:

X[0] ≤ X[1] ≤ ... ≤ X[i], {X[0],X[1],...,X[i]} ≤ {X[i+1],X[i+2],...,X[n-1]}

Ovi uslovi bi mogli biti i korisne invarijante petlji.

Istaknimo potencijalne invarijante u pseudokodu programa: 

{X je niz dimenzije n, n ≥ 0}
for i = 0 to n - 2 do
begin 
	for j = i + 1 to n - 1 do
		begin 
			if (X[i] > X[j]) 
			begin 
				pom = X[i]; 
				X[i] = X[j]; 
				X[j] = pom ;
			end
		{X[i] ≤ {X[i+1],X[i+2],...,X[j]}}
		end
{X[0] ≤ X[1] ≤ ... ≤ X[i], {X[0],X[1],...,X[i]}≤{X[i+1],X[i+2],...,X[n-1]}}
end
{X[0] ≤ X[1] ≤ ... ≤ X[n-1]}


Pratite izvršavanje programa i vrednosti invarijante za različite ulazne vrednosti

Program: Vrednosti promenljivih: 

{X je niz dimenzije n, n ≥ 0}
 for i = 0 to n - 2 do
 begin 
  for j = i + 1 to n - 1 do
    begin 
     if (X[i] > X[j]) 
      begin 
	 pom = X[i]; 
	 X[i] = X[j]; 
	 X[j] = pom ;
      end
    X[i] ≤ {X[i+1],X[i+2],...,X[j]}}
    end
 {X[0] ≤ X[1] ≤ ... ≤ X[i], 
 {X[0],...,X[i]}≤{X[i+1],...,X[n-1]}}
 end
 {X[0] ≤ X[1] ≤ ... ≤ X[n-1]}



Naredna: Dokaz parcijalne korektnosti programa Gore: Selection sort Prethodna: Testiranje programa   Sadržaj