Pre formalnog izvođenja korektnosti programa, testirajmo program na nekoliko primera. Primeri su odabrani tako da se prilikom izvršavanja testiraju sve grane programa.
Testirajmo najpre ispravnost programa za x=100 i y=15.
Promenljive x i y u toku izvršavanja programa neće menjati svoju vrednost,
pa je dovoljno pratiti promene vrednosti promenljivih q i r nakon svake iteracije:
x |
y |
q |
r |
|
| pre ulaska u petlju | 100 |
15 |
0 |
100 |
| posle 1. iteracije | 100 |
15 |
1 |
85 |
| posle 2. iteracije | 100 |
15 |
2 |
70 |
| posle 3. iteracije | 100 |
15 |
3 |
55 |
| posle 4. iteracije | 100 |
15 |
4 |
40 |
| posle 5. iteracije | 100 |
15 |
5 |
25 |
| posle 6. iteracije | 100 |
15 |
6 |
10 |
Kako za r=10 uslov za ulazak u petlju r=y nije zadovoljen, program se zaustavlja a promenljive q i r sadrže željene vrednosti: 100 = 6*15 + 10 i 0≤10<15.
Testirajmo sada ispravnost programa za x=15 i y=20.
x |
y |
q |
r |
|
| pre ulaska u petlju | 15 |
20 |
0 |
15 |
Kako uslov ulaska u petlju nije zadovoljen, to se telo petlje neće izvršavati. Vrednosti promenljivih q i r sadrže željene vrednosti: 15 = 0*20 + 15 i 0≤15<20
Ovi test primeri su nas do izvesne mere uverili u ispravnost programa, međutim, to još uvek ne znači da program zaista jeste ispravan za sve moguće vrednosti na ulazu koje zadovoljavaju preduslov. Da bi se to dokazalo, potrebno je izvesti formalni dokaz korišćenjem sredstava matematičke logike.
Naredna: Invarijanta petlje Gore: Celobrojno deljenje Prethodna: Pseudokod programa Sadržaj