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

Invarijanta petlje

Može se primetiti da je u svim test primerima nakon svake iteracije ispunjen uslov NZD(p,q)=NZD(x,y). To bi mogla da bude korisna invarijanta petlje.
Program u kome je istaknuta potencijalna invarijanta zapisuje se na sledeći način:

{x > 0, y > 0} 
    p = x;
    q = y; 
    if (p < q) then 
      begin 
        pom = p; 
        p = q; 
        q = pom; 
      end 
    {NZD(p,q) = NZD(x,y)} 
    while (q ≠ 0) do 
      begin
        pom = q; 
        q = p % q; 
        p = pom; 
      {NZD(p,q)=NZD(x,y)} 
      end  
    z = p; 
{z = NZD(x,y)} 

Pokažimo najpre da dati uslov važi nakon svake iteracije za vrednosti ulaznih promenljivih za koje smo izvršili testiranje programa:

Za x=14 i y=21:

	x	y	p	q	NZD(p,q)=NZD(x,y)
pre ulaska u petlju	14	21	21	14	7=7
posle 1. iteracije	14	21	14	7	7=7
posle 2. iteracije	14	21	7	0	7=7

Za x=7 i y=0:

	x	y	p	q	NZD(p,q)=NZD(x,y)
pre ulaska u petlju	7	0	7	0	7=7

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

{x ≥ 0, y ≥ 0} 
    p = x;
    q = y; 
    if (p < q) then 
      begin 
        pom = p; 
        p = q;			
        q = pom; 
      end 
    {NZD(p,q) = NZD(x,y)}
    while (q ≠ 0) do 
      begin
        pom = q; 
        q = p % q; 
        p = pom; 
      {NZD(p,q)=NZD(x,y)} 
      end  
    z = p; 
{z = NZD(x,y)} 

Primer 1. Razmotrimo datu vezu u nešto drugačijem programu:

{x > 0, y > 0} 
    p = x; 
    q = y; 
    if (p < q) then 
      begin 
        q = p; 
        p = q; 
      end 
    while (q ≠ 0) do 
      begin
        pom = q; 
        q = p % q; 
        p = pom; 
      end   
    z = p; 
{z = NZD(x,y)} 

Za x=21 i y=14:

	x	y	p	q	NZD(p,q)=NZD(x,y)
pre ulaska u petlju	21	14	21	14	7=7
posle 1. iteracije	21	14	14	7	7=7
posle 2. iteracije	21	14	7	0	7=7

Dakle, u ovom slučaju, program izračunava željenu vrednost NZD-a brojeva x i y.

Za x=14 i y=28:

	x	y	p	q	NZD(p,q)=NZD(x,y)
pre ulaska u petlju	14	28	14	14	14 = 14
posle 1. iteracije	14	28	14	0	14 = 14

I u ovom slučaju, program izračunava željenu vrednost NZD-a brojeva x i y.

Međutim, za x=14 i y=21:

	x	y	p	q	NZD(p,q)=NZD(x,y)
pre ulaska u petlju	14	21	14	14	14 ≠ 7
posle 1. iteracije	14	21	14	0	14 ≠ 7

Za ove ulazne vrednosti invarijanta nije uspostavljena pre ulaska u petlju što dovodi do netačnog rezultata, specifikacija nije zadovoljena pa ovaj program nije parcijalno korektan.

Primer 2. Promenimo sada preduslov programa:

{x ≥ 0, y ≥ 0} 
    p = x; 
    q = y; 
    if (p < q) then 
      begin 
        pom = p; 
        p = q; 
        q = pom; 
      end 
    while (q ≠ 0) do 
      begin
        pom = q; 
        q = p % q; 
        p = pom; 
      end   
    z = p; 
{z = NZD(x,y)} 

Za x=14 i y=21:

	x	y	p	q	NZD(p,q)=NZD(x,y)
pre ulaska u petlju	14	21	21	14	7=7
posle 1. iteracije	14	21	14	7	7=7
posle 2. iteracije	14	21	7	0	7=7

Međutim, testirajmo ovaj program za x=0 i y=0:

	x	y	p	q	NZD(p,q)=NZD(x,y)
pre prvog ulaska u petlju	0	0	0	0	NZD(0,0)=NZD(0,0)

Uslov ulaska u petlju q ≠ 0 nije ispunjen još na samom početku, vrednost promenljive z se postavlja na 0 i izlazi se iz programa. Kako ne važi 0 = NZD(0,0), jer NZD(0,0) nije definisan, pauslov programa nije ispunjen, pa program nije parcijalno korektan.

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