Corectitudinea algoritmilor

Corectitudinea algoritmilor

Un algoritm α care rezolva problema P are trei clase de variabile, grupate in vectorii x, y, z. Componentele vectorului x reprezinta variabilele de intrare, care sunt date cunoscute ale problemei P. Componentele vectorului z reprezinta variabilele de iesire, care sunt variabile care au ca valori rezultatele problemei P. Componentele vectorului y reprezinta variabilele de lucru ale problemei P, care au ca valori rezultate intermediare ale problemei P. Fie v=(x,y,z) vectorul tuturor variabilelor algoritmului α. In timpul executiei algoritmului α fiecare variabila are o valoare curenta sau pana la timpul curent nu a primit valoare, caz in care se spune ca variabila nu este inca utilizata. Fie v=(v(1),,v(n)) vectorul variabilelor si w=(w(1),,w(n)) vectorul valorilor curente ale vectorului v.

Vectorul w reprezinta starea executiei algoritmului α la timpul curent. Daca variabila v(i) este neutilizata pana la acest moment atunci valoarea ei w(i) se noteaza prin litera greceasca θ. Executia unei instructiuni a algoritmului α poate schimba valoarea unor variabile si deci poate schimba starea executiei algoritmului. Fie w₀ starea initiala a executiei, care este starea cu toate variabilele neutilizate. Secventa de stari

w₀, w₁,,w_m-1,w_m(,)

formata cu toate starile executiei, unde w_m este starea finala obtinuta dupa executia ultimei instructiuni, daca executia se termina intr-un numar finit de pasi, reprezinta calculul executat de algoritm. Este posibil ca algoritmul sa intre intr-un ciclu infinit, caz in care executia nu se termina intr-un numar finit de pasi. Daca executia algoritmului α se termina intr-un numar finit de pasi atunci vectorul r=(r(1), , r(l)) obtinut din w_m=(w_m(1), , w_m(n)) selectand valorile corespunzatoare variabilelor de iesire ale vectorului z reprezinta rezultatul executiei.

Exemplul 2.12

Sa se determine numarul de divizori ai unui numar natural dat x.

PROGRAM NRDIV;

I0) BEGIN

I1) READ X;

I2) Y:=1;

I3) Z:=0;

I4) WHILE X≠Y DO

I5) Y Y+1;

I6) IF X MODULO Y = 0 THEN Z Z+1;

ENDWHILE;

I7) WRITE Z;

END.

Se executa algoritmul pentru x=6. Calculul executat de algoritm este urmatorul:

v=(x,y,z), w₀=( θ, θ, θ)

i1(w₀)=w₁=(6, θ, θ)

i2(w₁)=w₂=(6, 1, θ)

i3(w₂)=w₃=(6, 1, 0)

i5(w₃)=w₄=(6, 2, 0)

i6(w₄)=w₅=(6, 2, 1)

i5(w₅)=w₆=(6, 3, 1)

i6(w₆)=w₇=(6, 3, 2)

i5(w₇)=w₈=(6, 4, 2)

i6(w₈)=w₉=(6, 4, 2)

i5(w₉)=w₁₀=(6, 5, 2)

i6(w₁₀)=w₁₁=(6, 5, 2)

i5(w₁₁)=w₁₂=(6, 6, 2)

i6(w₁₂)=w₁₃=(6, 6, 3)

r=(3)

Un algoritm este corect daca satisface specificatiile problemei rezolvate. Aceasta inseamna ca rezultatele obtinute prin executia algoritmului pentru o intrare care satisface specificatiile problemei sunt corecte.

O problema poate fi rezolvata numai pentru unele valori ale datelor de intrare. Utilizam un predicat de intrare pentru a distinge care sunt aceste valori si pentru ce valori de intrare problema nu are solutie. Notam acest predicat de intrare prin φ(x). Pentru acele valori w_x ale vectorului de intrare x pentru care φ(w_x) este adevarata problema are solutie (poate fi rezolvata), altfel problema nu are solutie (este inutil a cauta rezultatele).

Intre rezultatele z ale problemei si datele de intrare x exista o relatie. Aceasta relatie este data printr-un predicat de iesire notat ψ(x,z).. Acest predicat este adevarat pentru acele valori w_x si w_z ale vectorilor x si z pentru care rezultatele problemei sunt w_z cand valorile de intrare sunt w_x si predicatul este fals altfel. Cu alte cuvinte, daca executia algoritmului pentru valorile de intrare w_x se obtin rezultatele w_z' si ψ(w_x, w_z') este fals, atunci inseamna ca rezultatele w_z' sunt incorecte.

Definitia 2.19

Perechea (φ(x), ψ(x,z)), unde φ(x) este predicatul de intrare si ψ(x,z) este predicatul de iesire se numeste specificatia problemei P sau specificatia algoritmului α.

Observatia 2.9

Predicatul de intrare se mai numeste si preconditie si predicatul de iesire se mai numeste si postconditie. Evident ca cele doua predicate sunt cunoscute (specificatia este cunoscuta) numai cand vectorul de intrare x si vectorul de iesire z sunt cunoscuti.

Exemplul 2.17

Calculul radacinii patrate a unui numar real. Fie w numarul real dat si r rezultatul (radacina patrata a lui w). Atunci specificatia este data prin predicatele:

φ(x): "w>0"    (preconditia)

ψ(x,z): "r²=w"    (postconditia)

Aceasta specificatie este corecta pentru un matematician, dar nu este admisibila pentru un informatician. Un numar real este reprezentat in memoria unui calculator cu un numar finit de biti si uzual valoarea exacta a radacinii patrate r este aproximata astfel incat |w-r²|<ε, cu ε>0. Precizia ε trebuie data, astfel vectorul de intrare este x=(w, ε) si specificatia devine:

φ(x): "w>0 si ε>0" (preconditia)

ψ(x,z): "|w-r²|<ε"    (postconditia)

Referitor la corectitudinea unui algoritm α prezentam urmatoarele definitii.

Definitia 2.20

Se spune ca algoritmul α se termina in raport cu predicatul de intrare φ(x) daca si numai daca pentru oricare intrare w_x a vectorului de intrare x pentru care predicatul de intrare φ este adevarat, executia lui α se termina.

Definitia 2.21

Se spune ca algoritmul α este partial corect in raport cu specificatia (φ, ψ) daca si numai daca pentru orice intrare w_x a vectorului de intrare x pentru care predicatul de intrare φ este adevarat si executia algoritmului α se termina cu rezultatul w_z= α(w_x) atunci ψ(w_x, w_z) este adevarata.

Definitia 2.22

Se spune ca algoritmul α este total corect in raport cu specificatia (φ, ψ) daca si numai daca α se termina si este partial corect referitor la aceasta specificatie.

In continuare se prezinta metoda Floyd pentru demonstrarea corectitudinii partiale a unui algoritm α. Algoritmul poate fi exprimat fie printr-un program sub forma de schema logica, fie in pseudocod sau intr-un limbaj de programare. Reamintim ca un program sub forma de schema logica este un graf orientat in care orice arc este etichetat conform instructiunii pe care o reprezinta si apartine cel putin unui drum de la instructiunea START la instructiunea STOP. Nodurile sunt puncte care delimiteaza arcele. O multime de puncte astfel incat fiecare circuit contine cel putin un punct al multimii si de asemenea contine punctul terminal al instructiunii START si punctul initial al instructiunii STOP se numeste multime de puncte taietura. Analog se poate defini o multime de puncte taietura pentru un subprogram. La fiecare punct taietura i se asociaza un predicat τ_i(x,y). Aceste predicat este adevarat invariant pentru valorile curente ale lui x si y in acest punct si se numeste predicat invariant. Pentru punctul terminal al instructiunii START predicatul invariant este φ(x) si pentru punctul initial al instructiunii STOP predicatul invariant este ψ(x,z). Fie D_ij un drum de la punctul taietura i la punctul taietura j care nu contine puncte taietura intermediare (pot exista mai multe astfel de drumuri). La acest drum se asociaza un predicat δ_ij(x,y) care ofera conditia ca drumul sa fie traversat si o functie f_ij(x,y) astfel incat daca y sunt valorile intermediare in punctul taietura i atunci, cand drumul este traversat, y'=f_ij(x,y) sunt valorile in punctul de taietura j cu τ_j(x,y') predicatul invariant. Conditia de verificare asociata drumului D_ij este

τ_j(x,y) δ_ij(x,y) τ_j(x,y') pentru x, y, D_ij.

Teorema 2.2

Daca toate conditiile de verificare sunt adevarate atunci programul P este partial corect in raport cu specificatiile φ(x), ψ(x,z).

Demonstratie

Cititorul interesat poate consulta bibliografia indicata in aceasta carte.

Exemplul 2.18

Sa se determine cel mai mare divizor comun (CMMDC) d a doua numere naturale m si n, d=(m,n).

Programul sub forma de schema logica si pseudocodul algoritmului de rezolvare a problemei sunt prezentate in continuare.

PROGRAM CMMDC;

BEGIN

READ M, N;

D:=M;

I:=N;

WHILE (D≠I) AND (I>0) DO

IF D>I

THEN D:=D-I

ELSE I:=I-D;

ENDIF;

ENDWHILE;

WRITE D;

END.

Varibilele folosite grupate in cei trei vectori sunt x=(m,n), y=(d,i), z=(d). Specificatiile problemei sunt:

φ(x): mN, nN,

ψ(x,z): d=(m,n).

Multimea de puncte taietura este T=. Predicatele invariante sunt τ₁(x): mN, nN, τ₂(x, y): (d,i)=(m,n), τ₃(x,z): d=(m,n). Drumurile D_ij posibile in acest program sunt: D₁₂=(1, 2), D₂₂=(2, 2), D₂₃=(2, 3). Conditiile de parcurgere a acestor drumuri sunt

δ₁₂(x,y): (d≠i) si (i>0);

δ₂₂(x,y): (d≠i) si (i>0);

δ₂₃(x,y): (d=i) si (i=0).

Transformarile f_ij(x,y) care modifica valorile vectorului y=(d,i) sunt:

f₁₂(x,y): (m,n);

f₂₂(x,y): daca d>i atunci (d-i, i) altfel (d, i-d);

f₂₃(x,y)=f₂₂(x,y).

Corespunzator drumurilor Dij avem urmatoarele conditii de verificare:

C₁₂: (m≠n) si (0≠n) ((m, n) = (m, n));

C₂₂: (CMMDC(d, i)=CMMDC(m, n)) si (d≠i) si (i>0)

((d>i) si CMMDC(d-i, i)=CMMDC(m, n)) sau

((d<i) si CMMDC(d, i-d)=CMMDC(m, n));

C₂₃: (CMMDC(d, i)=CMMDC(m, n)) si ((d=i) sau (i=0))

(d=CMMDC(m, n)).

Prima conditie C₁₂ este imediata: intotdeauna un numar este egal cu el insusi. A doua conditie C₂₂ contine doua cazuri: d>i si d<i, corespunzatoare circuitului D₂₂ (ramurile THEN si ELSE). In ambele cazuri conditia stabileste ca cel mai mare divizor comun a doua numere nu se schimba daca inlocuim numarul cel mai mare prin diferenta lor, care este o simpla lema din matematica. De asemenea, conditia C₂₃ contine doua cazuri: d=i sau i=0. Daca d=i atunci CMMDC(d, i)=d si conditia este verificata. Daca i=0 din nou CMMDC(d, i)=d.

Pentru a demonstra terminarea programului se va folosi notiunea de multime convenabila.

Definitia 2.23

O multime este o multime convenabila daca ea este partial ordonata si nu contine nici un sir descrescator infinit.

Exemplul 2.19

Multimea numerelor naturale N cu relatia "<" si multimea NxN cu ordinea lexicografica:

(m1, n1)<(m2, n2) daca (m1<m2) sau (m1=m2) si (n1<n2) sunt multimi convenabile.

Pentru a demonstra terminarea algoritmului va trebui sa demonstram ca anumite conditii de terminare au loc. Aceste conditii spun ca trecerea prin programul sub forma de schema logica sau pseudocod de la un punct de taietura la urmatorul valorile unor functii in multimea convenabila aleasa scad. Deoarece nu se poate construi un sir descrescator infinit rezulta ca nu se trece de la un punct taietura la urmatorul de o infinitate de ori. Deci executia algoritmului se termina.

Pentru fiecare punct taietura i se alege o functie: g_i:M_xxM_x M. Pentru fiecare drum D_ij conditia de terminare este de forma:

In cazul in care s-a demonstrat partial corectitudinea si τ_i(x, y) a fost predicatul invariant in punctul i, conditia de terminare pentru drumul D_ij de la punctul i la punctul j se poate lua:

Teorema 2.3

Daca toate conditiile de terminare sunt adevarate atunci algoritmul se termina in raport cu predicatul de intrare φ(x).

Demonstratie

Cititorul interesat poate consulta bibliografia indicata in aceasta carte.

Exemplul 2.20

Reluam problema CMMDC din exemplul anterior. Avem trei puncte taietura, pentru care alegem:

g₁(x,y): 2m+2n;

g₂(x,y): d+i;

g₃(x,y): 0,

iar conditiile de terminare corespunzatoare acestor drumuri sunt:

;

Se poate verifica ca toate trei conditiile sunt adevarate pentru m>0 , dar este falsa daca m=0, intrucat d ia valoarea 0 si inegalitatea i>i este falsa. In acest caz drumul D₂₂ (care este un circuit) este parcurs de o infinitate de ori, deoarece variabilele d si i nu-si modifica valorile la parcurgerea acestui drum. Pentru a obtine un algoritm total corect este necesara modificarea algoritmului CMMDC1 astfel incat sa nu se intre in drumul D₂₂ daca d=0. Obtinem urmatorul algoritm total corect:

PROGRAM CMMDC2;

BEGIN

READ M,N

IF M=0

THEN D:=N; I:=0

ELSE D:=M; I:=N

ENDIF;

WHILE (D≠I) AND (I>0) DO

IF D>I

THEN D:=D-I

ELSE I:=I-D

ENDIF;

ENDWHILE;

WRITE D;

END.

O buna parte din demonstrarea corectitudinii unui program poate fi automatizata. Astfel, scrierea conditiilor de verificat, in ipoteza ca sunt date predicatele invariante, poate fi automatizata. De asemenea, demonstrarea automata a conditiilor de verificat este posibila. Ceea ce nu se poate automatiza este descoperirea predicatelor invariante, care trebuie furnizate de proiectant. Aceasta ultima cerinta impune proiectantului respectarea unei discipline de programare. Foarte probabil ca aceste predicate invariante sunt sugerate de semnificatiile variabilelor. Deci este necesar ca fiecare variabila sa aiba semnificatia ei si sa nu fie folosita in scopuri diferite.

Ideile lui Floyd au fost dezvoltate de Hoare care introduce o metoda axiomatica pentru demonstrarea corectitudinii partiale a unui algoritm. Dijkstra introduce conceptul important de cea mai slaba preconditie. Aceasta idee a fost continuata de Gries si dezvoltata de Dromey si Morgan. Cititorii interesati de aceste idei pot consulta cartea [8]. Aceasta reprezinta lucrarea principala din care s-au preluat informatiile redactarii acestui paragraf.