Naredna: Dokaz parcijalne korektnosti programa Gore: Celobrojno deljenje Prethodna: Testiranje programa   Sadržaj

Invarijanta petlje

Ono što se može uočiti iz prethodnog test primera jeste da pre svakog ulaska u petlju važi x=qy+r, r≥0. To nagoveštava da bi korisna invarijanta petlje mogla biti baš taj uslov.

Program u kojem je istaknuta potencijalna invarijanta može se zapisati na sledeći način:

{x ≥ 0, y > 0}
    q = 0;
    r = x;
   {x = q * y + r, r≥0}
   while (r ≥ y) do
      begin
        q = q + 1;
        r = r - y;
       {x = q * y + r, r≥0}  
      end
{x = q * y + r, 0≤r<y}

Pokažimo najpre da dati uslov važi nakon svake iteracije u pomenutom test primeru :

 
x
y
q
r
x=qy+r, r≥0
pre ulaska u petlju
100
15
0
100
100=0*15+100,100≥0
posle 1. iteracije
100
15
1
85
100=1*15+85,85≥0
posle 2. iteracije
100
15
2
70
100=2*15+70,70≥0
posle 3. iteracije
100
15
3
55
100=3*15+55,55≥0
posle 4. iteracije
100
15
4
40
100=4*15+40,40≥0
posle 5. iteracije
100
15
5
25
100=5*15+25,25≥0
posle 6. iteracije
100
15
6
10
100=6*15+10,10≥0


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

Program: Vrednosti promenljivih: 

 {x ≥ 0, y > 0} 
    q = 0;
    r = x;
       {x = q * y + r, r ≥ 0} 
    while (r ≥ y) do
      begin
        q = q + 1;
        r = r - y;
         {x = q * y + r, r ≥ 0} 
      end  
{x = q * y + r, 0 ≤ r < y}


Primer 1. Izmenimo prethodni program i razmotrimo šta se dešava sa datim uslovom koji je potencijalna invarijanta petlje originalnog programa.

{x ≥ 0, y > 0}
    q = 0;
    r = x;
   {x = q * y + r, r ≥0}
   while (r ≥ y) do
      begin
        q = q - 1;
        r = r - y;
       {x = q * y + r, r≥0}  
      end
{x = q * y + r, 0 ≤ r < y}
 
x
y
q
r
x=qy+r,r≥0
pre ulaska u petlju
100
15
0
100
100=0*15+100=100,100≥0
posle 1. iteracije
100
15
-1
85
100≠-1*15+85=70,85≥0
posle 2. iteracije
100
15
-2
70
100≠-2*15+70=40,70≥0
posle 3. iteracije
100
15
-3
55
100≠-3*15+55=10,55≥0
posle 4. iteracije
100
15
-4
40
100≠-4*15+40=-20,40≥0
posle 5. iteracije
100
15
-5
25
100≠-5*15+25=-50,25≥0
posle 6. iteracije
100
15
-6
10
100≠-6*15+10=-80,10≥0

Može se primetiti da već nakon prve iteracije odgovarajući uslov nije ispunjen, što znači da on nije invarijanta petlje ovog programa. Pritom, ovaj program ne zadovoljava datu specifikaciju.

Primer 2. Pogledajmo šta se dešava u sledećem, na drugi način izmenjenom programu: 

{x ≥ 0, y > 0}
    q = 0;
    r = x;
   {x = q * y + r, r ≥0}
   while (r > y) do
      begin
        q = q + 1;
        r = r - y;
       {x = q * y + r, r>0}  
      end
{x = q * y + r, 0 ≤ r < y}
 
x
y
q
r
x=qy+r,r≥0
pre ulaska u petlju
100
20
0
100
100=0*20+100=100,100≥0
posle 1. iteracije
100
20
1
80
100=1*20+80=100,80≥0
posle 2. iteracije
100
20
2
60
100=2*20+60=100,60≥0
posle 3. iteracije
100
20
3
40
100=3*20+40=100,40≥0
posle 4. iteracije
100
20
4
20
100=4*20+20=100,20≥0

Može se primetiti da nakon četvrte iteracije, kako nije ispunjeno da je r > y, odnosno nije 20 > 20, uslov ulaska u petlju nije zadovoljen i izlazi se iz programa.

Proverimo da li važi pauslov programa {x = q * y + r, 0 ≤ r < y}:
Važi da je 100=4*20+20 ali ne važi 0 ≤ r < y, odnosno ne važi 0 ≤ 20 < 20, pa pauslov programa nije zadovoljen, što znači da program nije parcijalno korektan.



Naredna: Dokaz parcijalne korektnosti programa Gore: Celobrojno deljenje Prethodna: Testiranje programa   Sadržaj