Scrigroup - Documente si articole

Username / Parola inexistente      

Home Documente Upload Resurse Alte limbi doc  
AccessAdobe photoshopAlgoritmiAutocadBaze de dateCC sharp
CalculatoareCorel drawDot netExcelFox proFrontpageHardware
HtmlInternetJavaLinuxMatlabMs dosPascal
PhpPower pointRetele calculatoareSqlTutorialsWebdesignWindows
WordXml


Corectitudinea algoritmilor

c



+ Font mai mare | - Font mai mic



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 w0 starea initiala a executiei, care este starea cu toate variabilele neutilizate. Secventa de stari

w0, w1,,wm-1,wm(,)

formata cu toate starile executiei, unde wm 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 wm=(wm(1), , wm(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), w0=( θ, θ, θ)

i1(w0)=w1=(6, θ, θ)

i2(w1)=w2=(6, 1, θ)

i3(w2)=w3=(6, 1, 0)

i5(w3)=w4=(6, 2, 0)

i6(w4)=w5=(6, 2, 1)

i5(w5)=w6=(6, 3, 1)

i6(w6)=w7=(6, 3, 2)

i5(w7)=w8=(6, 4, 2)

i6(w8)=w9=(6, 4, 2)

i5(w9)=w10=(6, 5, 2)

i6(w10)=w11=(6, 5, 2)

i5(w11)=w12=(6, 6, 2)

i6(w12)=w13=(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 wx ale vectorului de intrare x pentru care φ(wx) 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 wx si wz ale vectorilor x si z pentru care rezultatele problemei sunt wz cand valorile de intrare sunt wx si predicatul este fals altfel. Cu alte cuvinte, daca executia algoritmului pentru valorile de intrare wx se obtin rezultatele wz' si ψ(wx, wz') este fals, atunci inseamna ca rezultatele wz' 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): "r2=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-r2|<ε, cu ε>0. Precizia ε trebuie data, astfel vectorul de intrare este x=(w, ε) si specificatia devine:

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

ψ(x,z): "|w-r2|<ε"    (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 wx 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 wx a vectorului de intrare x pentru care predicatul de intrare φ este adevarat si executia algoritmului α se termina cu rezultatul wz= α(wx) atunci ψ(wx, wz) 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 Dij 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 fij(x,y) astfel incat daca y sunt valorile intermediare in punctul taietura i atunci, cand drumul este traversat, y'=fij(x,y) sunt valorile in punctul de taietura j cu τj(x,y') predicatul invariant. Conditia de verificare asociata drumului Dij este

τj(x,y) δij(x,y) τj(x,y') pentru x, y, Dij.

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 τ1(x): mN, nN, τ2(x, y): (d,i)=(m,n), τ3(x,z): d=(m,n). Drumurile Dij posibile in acest program sunt: D12=(1, 2), D22=(2, 2), D23=(2, 3). Conditiile de parcurgere a acestor drumuri sunt

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

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

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

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

f12(x,y): (m,n);

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

f23(x,y)=f22(x,y).

Corespunzator drumurilor Dij avem urmatoarele conditii de verificare:

C12: (m≠n) si (0≠n) ((m, n) = (m, n));

C22: (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));

C23: (CMMDC(d, i)=CMMDC(m, n)) si ((d=i) sau (i=0))

(d=CMMDC(m, n)).

Prima conditie C12 este imediata: intotdeauna un numar este egal cu el insusi. A doua conditie C22 contine doua cazuri: d>i si d<i, corespunzatoare circuitului D22 (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 C23 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: gi:MxxMx M. Pentru fiecare drum Dij 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 Dij 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:

g1(x,y): 2m+2n;

g2(x,y): d+i;

g3(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 D22 (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 D22 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.





Politica de confidentialitate | Termeni si conditii de utilizare



DISTRIBUIE DOCUMENTUL

Comentarii


Vizualizari: 1055
Importanta: rank

Comenteaza documentul:

Te rugam sa te autentifici sau sa iti faci cont pentru a putea comenta

Creaza cont nou

Termeni si conditii de utilizare | Contact
© SCRIGROUP 2024 . All rights reserved