Dokaz parcijalne korektnosti programa

Dokažimo sada da pomenuti uslovi zaista jesu korisne invarijante petlji. Ono što treba da dokažemo je da nakon svakog prolaska kroz odgovarajuću petlju važi dati uslov, kao i da nas ovi uslovi vode ka ostvarivanju željenog pauslova.

Dokaz invarijante unutrašnje petlje

Dokažimo najpre da je uslov

{X[i] ≤ {X[i+1],X[i+2],...,X[j]}}	(*)

invarijanta unutrašnje for petlje za proizvoljnu vrednost i, 0 ≤ i ≤ n-2, pri čemu je i brojač u spoljašnjoj for petlji a j brojač u unutrašnjoj for petlji.

Za j = i + 1, pošto je 0 ≤ i ≤ n-2 ispunjen je uslov ulaska u petlju tj. važi j ≤ n-1. Ako nije X[i] > X[j], onda važi X[i] ≤ X[j], a ako je X[i] > X[j] tada će biti izvršena razmena vrednosti i-tog i j-tog elementa niza. Dakle, nakon prvog prolaska kroz petlju važi da je

{X[i] ≤ {X[j]}}

{X[i] ≤ {X[i+1],X[i+2],...,X[j+1]}}

Ukoliko je ispunjen uslov ulaska u petlju j' ≤ n-1 onda se ispituje da li važi X[i] > X[j'].

• Ako je uslov X[i] > X[j'] ispunjen, tada na osnovu tranzitivnosti relacije ≤ i pretpostavke (*) važi da je X[j'] ≤ {X[i+1],X[i+2],...,X[j]}. Kako X[i] i X[j'] u ovom slučaju razmenjuju mesta, važi {X[i] ≤ {X[i+1],X[i+2],...,X[j']}}.
• Ako uslov X[i] > X[j'] nije ispunjen, tada je uslov {X[i] ≤ {X[i+1],X[i+2],...,X[j']}} direktno ispunjen.

Ovim smo dokazali da za proizvoljnu vrednost i, 0 ≤ i ≤ n-2, nakon svakog prolaska kroz unutrašnju petlju važi uslov (*) tj. da je on invarijanta unutrašnje petlje.

Dokaz invarijante spoljašnje petlje

Dokažimo sada da je uslov

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

invarijanta spoljašnje for petlje.Dokažimo ujedno i parcijalnu korektnost programa.

Dokaz se sastoji iz tri koraka:

1. Uspostavljanje invarijante
2. Održavanje invarijante
3. Ostvarivanje željenog pauslova

1. Uspostavljanje invarijante: Iz preduslova važi da je n ≥ 0. U slučaju da je n = 0 ili n = 1, to znači da je u pitanju prazan niz ili niz od jednog elementa pa je takav niz već sortiran i pauslov je ispunjen. U slučaju da je n ≥ 2, odnosno da se niz sastoji od bar dva elementa, važi:

Nakon prvog prolaska kroz spoljašnju petlju, za i = 0, kako nakon svakog prolaska kroz unutrašnju petlju važi prethodno dokazana invarijanta unutrašnje petlje

{X[i] ≤ {X[i+1],X[i+2],...,X[j]}}

to ona važi i nakon posledjeg prolaska kroz unutrašnju petlju kada je j = n - 1

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

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

nakon prvog prolaska kroz spoljašnju petlju tj. za i = 0.

2. Održavanje invarijante: Pretpostavimo da navedena relacija važi za proizvoljnu vrednost i, 0 ≤ i ≤ n-2 i dokažimo da važi za i' pri čemu je i' = i + 1.

Za i' ≤ n-2, nakon poslednjeg prolaska kroz unutrašnju petlju važiće njena invarijanta za j = n-1, tj. važiće uslov:

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

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

to jest

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

i kako je

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

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

Takođe, kako je

X[0] ≤ X[1] ≤ ... ≤ X[i]

i

važi

X[0] ≤ X[1] ≤ ... ≤ X[i] ≤ X[i']

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

3. Ostvarivanje željenog pauslova: Nakon izlaska iz spoljašnje for petlje za i = n - 2, izlazi se iz programa i važi

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

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

što je pauslov programa, čime smo dokazali parcijalnu korektnost programa.

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