CORECTITUDINEA ALGORITMILOR

A program and its proof should be developed

hand-in-hand, with the proof usually leading the way.

Gries [Gri85]

5.1Notiunea de corectitudine

Un program este corect daca el satisface specificatiile problemei. Nu ne intereseaza cata memorie foloseste acest program, din cate instructiuni este compus, sau cat timp de executie necesita. Cu alte cuvinte, un program este corect daca pentru acele date de intrare care satisfac specificatiile problemei rezultatele obtinute in urma executiei sunt corecte.

Pentru orice program P deosebim trei tipuri de variabile, pe care le vom grupa in trei vectori X, Y si Z. Componentele vectorului X desemneaza variabilele de intrare, deci datele presupuse cunoscute in problema rezolvata prin programul P. Componentele vectorului Z sunt variabilele care reprezinta rezultatele cerute de problema. In sfarsit, componentele vectorului Y sunt variabilele de lucru, care noteaza diferitele rezultate intermediare necesare in program.

O problema nu are sens pentru orice date de intrare. Vom folosi predicatul φ(X) pentru a preciza datele pentru care problema are sens. φ(X) se numeste predicat de intrare sau preconditie. Pentru acele valori ale lui X pentru care predicatul este adevarat problema are sens, pentru celelalte nu are sens sa executam programul P.

Intre rezultatele Z ale problemei si datele initiale X (cunoscute in problema) exista anumite relatii. Vom reda aceste relatii prin predicatul de iesire ψ(X,Z), numit si postconditie. Acesta este corect pentru acele valori a si b ale vectorilor X si Z pentru care rezultatele problemei sunt b in cazul cand datele initiale sunt a si este fals in caz contrar. Deci, daca executand programul cu datele initiale a obtinem rezultatele b' si ψ(a,b') este fals, acest fapt este un indiciu ca rezultatele obtinute in program nu sunt corecte.

Definitia 5.1.1. Spunem ca cele doua predicate, predicatul de intrare φ(X) si predicatul de iesire ψ(X,Y), constituie specificatia problemei. Cele doua predicate se mai numesc preconditie, respectiv postconditie.

Se subintelege ca pentru a cunoaste aceasta specificatie trebuiesc cunoscuti si vectorii X si Z.

Astfel, daca in problema se cere sa se calculeze radicalul de ordinul 2 (notat prin r) dintr-un numar real pozitiv x, specificatia problemei este data prin predicatele:

φ(X): 'x>0' (preconditia)

ψ(X,Z):'r²=x' (postconditia)

Aceasta specificatie este corecta pentru un matematician, dar nu si pentru un programator. Numarul real r este in general transcendent si nu poate fi reprezentat in calculator decat aproximativ. Deci nu exista procedeu finit prin care putem calcula pe r. Putem construi insa un program care sa aproximeze oricat de bine pe r si va trebui sa adaugam acest lucru la enuntul problemei, care devine: se cere sa se calculeze r cu o eroare absoluta maxima ε data. In aceasta situatie vectorul de intrare este X=(x,ε) iar specificatia problemei va fi:

j(X):'x>0 si ε>0' ;

ψ(X,Z): ' r²-x <ε' .

Se observa mai bine si semnificatia “preciziei” ε. Am ales ca el sa majoreze diferenta dintre r² si x intrucat diferenta dintre r si valoarea exacta a radicalului e necunoscuta.

Nu putine sunt cazurile in care executia programului intra intr-un ciclu infinit, deci nu se mai termina. Este un caz nedorit, care trebuie evitat in programare.

Referitor la corectitudinea programelor dam urmatoarele definitii:

Definitia 5.1.2. Spunem ca programul P se termina in raport cu predicatul de intrare φ(X) daca pentru orice intrare a = (a₁,a₂,, a_n) a vectorului X pentru care predicatul φ este adevarat, executia lui P se termina.

Definitia 5.1.3. Spunem ca programul P este partial corect in raport cu specificatiile problemei daca pentru intrarea a pentru care φ(a) este adevarat si executia programului se termina cu rezultatele b=P(a) atunci ψ(a,b) este adevarat.

Definitia 5.1.5. Spunem ca un program P este total corect in raport cu specificatiile problemei daca programul P se termina si daca el este partial corect in raport cu aceste specificatii.

Exista mai multe metode de demonstrare a corectitudinii unui program. In continuare vom prezenta metoda asertiunilor inductive datorata lui Floyd [Floyd67], metoda care considera algoritmii reprezentati prin scheme logice. Subliniem ca e vorba de corectitudinea logica a programelor si nu de corectitudinea lor sintactica. De aceea nu conteaza forma sub care e dat algoritmul: fie scris intr-o schema logica, fie in Pseudocod, fie intr-un limbaj de programare. In acest capitol prin program ne referim la algoritmul corespunzator, indiferent de forma in care e scris.

Metoda cere alegerea unor puncte in schema logica, numite puncte de taietura. Se va alege cel putin un punct de taietura in fiecare bucla, un punct de taietura la inceputul schemei logice (dupa blocul de citire) si un punct de taietura la sfarsitul schemei logice (inaintea blocului de tiparire a rezultatelor) .

In fiecare punct de taietura se alege un predicat invariant. In punctul de taietura de intrare predicatul invariant este φ(X), iar in punctul de taietura de iesire predicatul invariant este ψ(X,Z).

Pentru o pereche (i,j) de puncte de taietura pot exista mai multe drumuri de la i la j. Fie α un astfel de drum cu proprietatea ca el nu contine un alt punct de taietura. Vom nota prin R_α(X,Y) predicatul care ne da conditia ca sa se parcurga acest drum si prin r_α(X,Y) functia care da transformarea variabilelor intermediare Y la traversarea drumului α. Schematic, putem reprezenta notatiile facute astfel:

P_i(X,Y) R_α(X,Y)                         P_j(X,Y)

o──────────────────────────────────→o

i α j

Acestui drum i se asociaza conditia de verificare:

X Y (P_i(X,Y) R_α(X,Y) P_j(X,r_α(X,Y)))

Subliniem ca intre doua puncte de taietura pot exista mai multe drumuri directe distincte.

Floyd [Floyd67] demonstreaza urmatoarea teorema:

Teorema 5.1.1. Daca toate conditiile de verificat sunt adevarate atunci programul P este partial corect in raport cu specificatiile φ(X) si ψ(X,Z).

Ca exemplu de demonstrare a corectitudinii unui program sa consideram urmatorul algoritm de calcul al celui mai mare divizor comun a doua numere date:

ALGORITMUL CMMDC1(n1,n2,d) ESTE:

DATE n1,n2;                                     

FIE d:=n1;

FIE i:=n2;

CATTIMP (d i) SI (i>0) EXECUTA           

DACA d>i ATUNCI d:=d-i

ALTFEL i:=i-d

SFDACA

SFCAT

REZULTATE d;

SFALGORITM

Variabilele folosite, grupate in cei trei vectori X, Y, Z sunt:

X = (n1, n2), Y = (d, i) siZ = (d).

Drumurile posibile in acest algoritm sunt: α1 = AB, α2 = BB si α3 = BC, iar conditiile de parcurgere a acestor drumuri sunt:

R_α1(X,Y) = (d i) ∧ (i>0) ;

R_α2(X,Y) = (d i) ∧ (i>0) ;

R_α3(X,Y) = not [(d i) ∧ (i>0)] <=> (d=i) ∨ (i=0) .

Transformarile pe aceste drumuri sunt date de:

r_α1 X,Y n1,n2

r_α2 X,Y = Daca d>i atunci (d-i,i) altfel (d,i-d);

r_α3(X,Y) = r_α2(X,Y).

Corespunzator acestor drumuri avem urmatoarele conditii de verificare:

C_α1 = (n1 n2) ∧ (0 n2) ( (n1,n2)=(n1,n2) ) ;

C_α2 = ((d,i)=(n1,n2)) ∧ (d i) ∧ (i 0)

((d>i) ∧ (d-i,i)=(n1,n2)) ∨ ((d<i) ∧ (d,i-d)=(n1,n2)) ;

C_α3 = ((d,i)=(n1,n2)) ∧ ((d=i) ∧ (i=0)) ( d=(n1,n2) ).

Se poate verifica usor ca toate aceste conditii sunt adevarate.

Pentru a demonstra terminarea programelor vom folosi notiunea de multime convenabila.

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

Exemple de multimi convenabile sunt multimea numerelor naturale N cu relatia '<' si multimea NxN cu ordinea lexicografica:

(m1,n1)<(m2,n2) daca (m1<m2) ∨ (m1=m2) ∧ (n1<n2).

Pentru a demonstra terminarea algoritmului va trebui sa demonstram ca anumite conditii de terminare au loc. Aceste conditii spun ca la trecerea prin schema logica (algoritm) de la un punct de taietura la altul valorile unor functii in multimea convenabila aleasa scad. Intrucat nu putem construi un sir (infinit) descrescator rezulta ca nu vom trece de la un punct de taietura la alt punct de taietura de o infinitate de ori, deci executia este finita; cu alte cuvinte algoritmul se termina. Prin urmare, in punctul de taietura i se alege o functie u_i : D_X x D_Y M, iar conditia de terminare pentru drumul α este:

X Y (φ(X) R_α(X,Y) (u_i(X,Y)>u_j(X,r_α(X,Y) )

In cazul in care s-a demonstrat partial corectitudinea si P_i(X,Y) a fost predicatul invariant in punctul i, conditia de terminare pentru drumul α care duce de la punctul i la punctul j se poate lua:

Document online: Accizele armonizate Document online: Elementele dobanzii simple si Plati esalonate anticipate - formule contabile

X Y (P_i(X,Y) R_α(X,Y) (u_i(X,Y) > u_j(X,r_α(X,Y)) )

Pentru algoritmul CMMDC1 avem trei puncte de taietura, pentru care alegem:

u₁(X,Y) = 2*n1 + 2*n2;

u₂(X,Y) = d + i;

u₃(X,Y) = 0,

iar conditiile de terminare corespunzatoare acestor drumuri sunt:

T_α1 = (n1 n2) (n2>0) (2*n1+2*n2 >n1+n2) ;

T_α2 = (P_B (d>i) (i>0) d+i>d) sau (P_B (d<i) (i>0) d+i>i) ;

T_α3 = True .

Se poate verifica ca toate cele trei conditii sunt adevarate pentru n1>0, dar T_α2 este falsa daca n1=0, intrucat d ia valoarea 0 si inegalitatea i>i este falsa. In acest caz drumul α2 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 α2 daca d=0. Obtinem urmatorul algoritm total corect:

ALGORITMUL CMMDC2(n1,n2,d) ESTE:

DATE n1,n2;                             

DACA n1=0 ATUNCI FIE d:=n2; i:=0

ALTFEL FIE d:=n1; i:=n2;

SFDACA

CATTIMP (d i) SI (i>0) EXECUTA                               

DACA d>i ATUNCI d:=d-i

ALTFEL i:=i-d

SFDACA

SFCAT

REZULTATE d;

SFALGORITM

Demonstrarea corectitudinii algoritmilor poate fi facuta dupa elaborarea lor, sau in timp ce sunt conceputi. Am vazut ca ea presupune scrierea unor predicate invariante corespunzatoare punctelor de taietura, deci ea impune proiectantului respectarea unei discipline in 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.

Gries [Gries89] spunea: Proiectarea programului si demonstrarea corectitudinii lui trebuie facute in paralel. Intr-o astfel de proiectare convingerea programatorului ca a conceput un algoritm corect creste, iar scrierea predicatelor invariante reduce numarul erorilor in programare. De asemenea, daca s-ar incerca demonstrarea corectitudinii algoritmilor descrisi, multe erori ar fi descoperite si eliminate in faza de proiectare.

Pornind de la aceasta afirmatie vom exemplifica in sectiunea urmatoare cum putem obtine algoritmi corecti prin rafinari succesive, pornind din specificatii. Rezulta din exemplele date ca in prim plan este demonstratia corectitudinii, propozitiile care compun algoritmul fiind o consecinta a acestei demonstratii.

5.2. Dezvoltarea algoritmilor din specificatii

In cele ce urmeaza vom prezenta mai multe reguli ce vor fi aplicate pentru a ajunge de la specificatii la algoritmul final corect. Este vorba despre o rafinare in pasi succesivi, in care unele parti din program sunt exprimate cu instructiuni din limbaj, altele, inca nefinisate, sunt doar specificate. La plecare, in versiunea initiala, avem doar specificatia, formata din cele doua predicate, de intrare si de iesire.

Regulile pe care le vom folosi in acest proces de rafinare se refera la propozitiile admise in descrierea algoritmilor si la reguli cunoscute din logica matematica. Propozitiile 'nestandard' folosite in acest proces de rafinare sunt specificatii care trebuie rafinate la un pas urmator. Astfel, prin propozitia nestandard

[φ1, ψ1]

vom nota acea parte de program care, pornind executia dintr-o stare in care preconditia φ1 este adevarata, ajunge intr-o stare in care postconditia ψ1 e adevarata.

Specificarea ne spune ce trebuie facut din punct de vedere al beneficiarului. Codul final, programul propriu-zis compus numai din instructiunile standard ale limbajului ales, spune calculatorului ce are de facut. Programatorul le intelege pe amandoua si actioneaza ca un translator. El transforma specificatiile, programul abstract, intr-un program executabil pe calculator. Procesul de realizare a acestui program final, adeseori dificil, va consta dintr-o succesiune de versiuni intermediare, compuse atat din specificatii (propozitii nestandard) cat si din propozitii standard (instructiunile limbajului).

In acest proces de rafinare o versiune Pnou va fi obtinuta din versiunea Pvechi prin rafinarea unor specificatii cu aplicarea regulilor care vor fi date putin mai jos. Spunem ca Pnou rafineaza pe Pvechi si scriem

Pvechi Pnou

Initial avem specificatia [φ, ψ], numita program abstract, notat cu P₀. Procesul de rafinare a specificatiilor va porni de la programul abstract P₀, va trece prin versiunile intermediare P₁ , P₂ , , P_n-1, pentru a ajunge la programul final P_n, aplicand regulile de rafinare permise, descrise in paginile care urmeaza. Redam acest proces sub forma:

P₀ P₁ P_n-1 P_n.

Regulile de rafinare sunt date in continuare. In cele ce urmeaza prin φ1(z|e) notam rezultatul substituirii in predicatul φ1(z) a variabilelor z prin expresiile e.

Regula atribuirii. Daca          pre T post[w|e]

atunci

[pre, post] w:=e

Urmatoarea regula se refera la compunerea secventiala

prog1 ; prog2

al carei efect consta in executia mai intai a partii de program prog1 urmata de executia lui prog2.

Regula compunerii secventiale. Oricare ar fi formula mijloc avem

[pre,post] [pre,mid] ; [mid,post]

Regula alternantei. Fie b₁ orice predicat si fie b₂ negatia lui b₁. Specificarea [pre,post] se poate rafina la

DACA b₁

ATUNCI [b₁ pre, post]

ALTFEL [b₂ pre, post]

SFDACA

Regula iteratiei. Pentru orice formula inv si e o expresie intreaga specificarea

[inv, inv not b₁

se poate rafina la

Cattimp b₁ executa

[inv b₁, inv (0<=e<e₀)]

sfcat

unde e₀ este valoarea expresiei e cu valori naturale inainte de executia propozitiei nestandard din interiorul lui Cattimp, deci paranteza din postconditie este conditia de terminare a ciclului.

In regula de mai sus formula inv joaca rolul de predicat invariant. El apare atat in preconditie cat si in postconditie. Pentru a nu-l scrie de doua ori introducem notatia

[pre, inv, post] :: = [pre inv, inv post]

Cu regulile prezentate mai sus putem da exemple de rafinari.

Exemplul 5.2.1. Inmultirea prin adunari repetate. Daca x si y sunt doua numere naturale arbitrare se cere sa se obtina produsul lor, efectuand doar adunari. Avem urmatoarea specificare:

φ : TRUE

ψ : z = x*y

deci programul abstract P₀ este

[TRUE; z = x*y ]

Aplicand regula compunerii secventiale cu predicatul

mijloc ::=z + u*v = x*y

ajungem la versiunea

P₁:

[ TRUE ; z + u*v = x*y] ;

[z + u*v = x*y ; z = x*y ]

intrucat postconditia din primul rand este adevarata pentru substitutia (z,u,v) | (0,x,y)

aplicand regula atribuirii ajungem la versiunea

P₂:

(z,u,v):=(0,x,y);

[z + u*v = x*y ; z = x*y ]

Pentru a continua vom scrie postconditia din randul doi intr-o forma echivalenta, astfel ca obtinem versiunea

P₃:

(z,u,v):=(1,x,y);

[z + u*v = x*y ; (z u*v = x*y) (v=0) ]

Observand ca prima paranteza este predicat invariant, vom aplica regula iteratiei, ajungand la versiunea

P₄:

(z,u,v):=(0,x,y);

Catimp v > 0 executa

[v>0, (z + u*v = x*y), v<v₀]

sfcat

Prima posibilitate de a-l micsora pe v este v:=v-1. Pentru ca predicatul invariant sa ramana adevarat este necesara substituirea lui z cu z+u, intrucat

z + u*v = (z+u) + u*(v-1)

deci ajungem la versiunea

P₅:

(z,u,v):=(1,x,y);

Cattimp v > 0 executa

(z,v):=(z+u,v-1)

sfcat

In versiunea P₄ , in cazul in care v este par, o alta posibilitate de a-l micsora pe v este a-l injumatati prin atribuirea v:=v div 2, pastrand predicatul invariant adevarat. Intrucat

(v e par) ∨ (v e impar) = TRUE

aplicand regula alternantei ajungem la urmatoarea versiune:

P₆: (z,u,v):=(0,x,y);

Cattimp v > 0 executa

Daca v e par

atunci[v e par,z + u*v = x*y ; (v = v₀/2)]

altfel[v impar ; (z + u*v = x*y),v=v₀-1]

sfdaca

sfcat

Pentru a pastra invariant predicatul z + u*v = x*y dupa atribuirea v := v / 2 este necesara atribuirea u := u+u intrucat

z + u*v =z + (u+u)*(v/2)

In cazul v impar stim din exemplul anterior ca ultima propozitie nestandard se rafineaza la atribuirea (v,z) := (v-1, z+u), astfel ca cele doua propozitii nestandard se rafineaza prin atribuiri si se ajunge la versiunea finala:

P₇: (z,u,v):=(0,x,y);

Cattimp v > 0 executa

Daca v e par

atunci (u,v) : = (u*u, v div 2)

altfel(v,z) : = (v-1,z+u)

sfdaca

sfcat

In versiunea P₄ , in cazul in care v este par si-l impartim la doi el poate ramane par. Aplicand de mai multe ori aceeasi micsorare (injumatatire) asupra lui v, acesta va deveni impar, caz in care se va micsora cu 1. Aplicand aceste transformari variantei P₄ de mai sus ajungem la urmatoarea versiune:

P₈: (z,u,v):=(0,x,y);

Cattimp v > 0 executa

Cattimp v e par executa

[v e par,z + u*v = x*y ; (v = v₀/2)]

sfcat

[v impar ; (z + u*v = x*y),v=v₀-1]

sfcat

Pentru a pastra invariant predicatul z + u*v = x*y dupa atribuirea v := v / 2 este necesara atribuirea u := u+u intrucat

z + u*v = z + (u+u)*(v/2)

Dupa aceasta rafinare se ajunge la varianta

Deja stim cum se rafineaza cele doua propozitii nestandard, astfel ca in doi pasi ajungem la versiunea:

P₉:

(z,u,v):=(0,x,y);

Cattimp v > 0 executa

Cattimp v e par executa

(u,v) : = (u*u, v div 2)

sfcat

(v,z) : = (v-1,z+u)

sfcat

Exemplul 5.2.2 Descompunerea unui numar in factori primi

Pentru a simplifica scrierea vom face urmatoarele notatii:

P=(p₁,p₂,, p_n); E=(e₁,e₂,, e_n)

PUTERE(p,e) = p^e;

PRODUS(k,P,E) ::= PUTERE(p₁,e₁)*PUTERE(p₂,e₂)**PUTERE(p_k,e_k)

PRIME(k,P,E) ::= ('p_i este prim si e_i>0', pentru i=1,k)

Cu aceste notatii specificarea problemei noastre este:

Preconditia:nIN; n 2;

Postconditia: (n = PRODUS(k,P,E) ) PRIME(k,P,E)

De asemenea, vom nota prin inv urmatorul predicat:

n = m*PRODUCT(k,P,E) PRIME(k,P,E)

care va avea rolul de predicat invariant. Pornind de la programul abstract

P₀:                     [n>2; (n = PRODUS(k,P,E) ) PRIME(k,P,E)]

si folosind regula compunerii secventiale obtinem versiunea:

P₁:         [n>2; inv] ;

[inv ; ( n = PRODUS(k,P,E) ) PRIME(k,P,E)] ;

intrucat inv devine TRUE pentru k=0 si m=n, prima propozitie nestandard se rafineaza la o atribuire. Ajungem la versiunea:

P₂:

(k,m):= (0,n) ;

[inv ; (n = PRODUS(k,P,E) ) PRIME(k,P,E)] ;

Postconditia se obtine din (m=1) inv astfel ca P₂ se poate rafina la

P₃:

(k,m):= (0,n) ;

[inv; inv (m=1)]

si folosind regula iteratiei ajungem la

P₄:

(k,m):= (0,n) ;

Cattimp m 1 executa

[m>1 ; inv; conditie de terminare]

sfcat

Conditia de terminare ar putea fi m<m₀ sau e<e₀ pentru o anumita expresie e. Pentru a-l micsora pe m pastrand inv adevarat e nevoie sa “mutam” un factor din m in vectorul P. Avem nevoie de o variabila candidat a fi factor prim al lui m pe care o vom nota cu f. Primul candidat este numarul prim 2, astfel ca initial f trebuie sa primeasca valoarea 2, iar propozitia nestandard o vom rafina prin regula alternantei la:

P₅:

(k,m):= (0,n) ; f:=2;

Cattimp m 1 executa

Daca m mod f = 0

atunci

[m mod f =0; inv ; f nu este factor al lui m]

altfel f:=f+1

sfdaca

sfcat

In propozitia nestandard inv este predicat invariant iar “f nu mai este factor al lui m” este o conditie de terminare, deci rafinarea se face cu regula iteratiei. Ajungem la versiunea

P₆: (k,m):= (0,n) ; f:=2;

Cattimp m 1 executa

Daca m mod f = 0

atunci

(k,P_k+1,e_k+1,m) :=(k+1,f,1,m/f);

Cattimp m mod f =0 executa

[m mod f = 0; inv ; (m=m₀/f)]

sfcat

altfel f:=f+1

sfdaca

sfcat

Pentru ca inv sa ramana adevarat dupa atribuirea m:=m/f este necesar ca e_k sa creasca cu 1, intrucat P_k=f. Ajungem la versiunea

P₇:         (k,m):= (0,n) ; f:=2;

Cattimp m 1 executa

Daca m mod f = 0

atunci

(k,P_k+1,e_k+1,m) :=(k+1,f,1,m/f);

Cattimp m mod f =0 executa

(m,e_k)=(m/f,e_k+1)

sfcat

altfel f:=f+1

sfdaca

sfcat

intrucat pe ramura atunci m se modifica astfel incat m nu se mai divide cu f, care este chiar conditia de pe ramura altfel, atribuirea f:=f+1 se poate muta in afara propozitiei Daca astfel ca obtinem varianta finala

P₈:         (k,m,f):= (0,n,2) ;

Cattimp m 1 executa

Daca m mod f = 0 atunci

(k,P_k+1,e_k+1,m) :=(k+1,f,1,m/f);

Cattimp m mod f =0 executa

(m,e_k)=(m/f,e_k+1)

sfcat

sfdaca

f:=f+1

sfcat

5.3 Probleme propuse

I. Folosind metoda lui Floyd, demonstrati corectitudinea algoritmilor precizati la fiecare caz.

1. Demonstrati partial-corectitudinea subalgoritmului CAT(m,n,q,r) in raport cu specificatia:

Preconditia: m≥0, n≥0

Postconditia: (m=n*q+r) ∧ (0≤r<n) .

1.

Subalgoritmul CAT(m,n,q,r) este:

Fie (q,r):=(0,m)

Cattimp r x executa

(r,d,q1):=(r-n,n,1);

Cattimp r d+d executa

(r,d,q₁) := (r-d-d,d+d,q₁+q₁+1)

sfcat

q:= q+q₁

sfcat

2. Demonstrati terminarea subalgoritmului CAT(m,n,q,r) in raport cu specificatia:

Preconditia: m≥0, n>0

Postconditia: : (m=n*q+r) si (0≤r<n) .

3. Demonstrati partial-corectitudinea subalgoritmului RADICAL(n,r) in raport cu specificatia:

Preconditia: n≥0

Postconditia: r² <= n < (r+1)² .

Subalgoritmul RADICAL(n,r) este:

r:=0; q:=s;

Cattimp r+1 q executa

p:= (r+q)/2;

Daca s<p²

atunci q:= p;

altfel r:=p

sfdaca

sfcat

4. Demonstrati terminarea subalgoritmului RADICAL(n,r) in raport cu specificatia:

Preconditia: n≥0

Postconditia: r² <= n < (r+1)² .

5. Demonstrati terminarea subalgoritmului CMMDC2(n1,n2,d) in raport cu specificatia:

Preconditia: n1≥0, n2≥0

Postconditia: d=cmmdc(n1,n2) .

Subalgoritmul CMMDC2(n1,n2,d) este:

Daca n1=0 atunci Fie d:=n2; i:=0

altfel Fie d:=n1; i:=n2;

sfdaca

Cattimp (d i) si (i>0) executa 

Daca d>i atunci d:=d-i

altfel i:=i-d

sfdaca

sfcat

SFCMMCD2

6. Demonstrati terminarea subalgoritmului FERMAT(n,x,y) in raport cu specificatia:

Preconditia: nIN

Postconditia: n=x*y

Subalgoritmul FERMAT(n, x,y) este:

(r,u,v):=(0,1,1);

Cattimp r n executa

Daca r<n

atunci (r,u):=(r+u,u+2)

altfel (r,v):=(r-v,v+2)

sfdaca

sfcat

sf-FERMAT

7. Demonstrati partial corectitudinea subalgoritmului FERMAT(n,x,y) in raport cu specificatia:

Preconditia: nIN

Postconditia: n=x*y

8. Demonstrati total corectitudinea urmatorului subalgoritm:

Algoritmul DIVINT(x,y,q,r) este:

(r, q) (x, 0)

Cattimp y r executa

r:= r-y;

q:=q+1;

sfcat

sf-DIVINT

II. Dezvoltati algoritmi corecti pentru urmatoarele probleme

1. Aflarea celui mai mare divizor comun a doua numere:

Preconditia: x,y I N;

Postconditia: d=cmmdc(x,y)

2. Aflati catul si restul unei impartiri intregi:

Preconditia: (x 0) (y>0)

Postconditia: (x=q*y+r) (0 r<y)

3. Radicalul intreg dintr-un numar natural:

Preconditia: sIN

Postconditia: r = partea intreaga din radical din s, adica r²≤s<(r+1)²

4. Ridicare la putere prin inmultiri repetate:

Preconditia: (x>0) (y 0)

Postconditia:: z = x^y

5.5. Suma componentelor unui vector:

Preconditia: n≥1

Postconditia:: s = a₁ + a₂ + + a_n

6. Cautare secventiala: gasiti pozitia pe care se afla un numar intr-un sir:

Preconditia: (0<j n, a_jIR) (xIR);

Postconditia: ( j, 0<j i, x a_j) (i=n conditional x=a_i+1) (0 i n)

7. Cautare binara

Preconditia: i, 1 i<n, a_i a_i+1) (a₁ x a_n)

Postconditia: (1 r<N, a_r x a_r+1)

8. Sortare: Se da vectorul A cu n componente. Sa se ordoneze crescator.

Preconditia: True

Postconditia: ORD(n,A) si (A=Perm(A₀))

unde

ORD(n,A) ::= ( i,j: 1 i,j n, i j T a_i a_j)

iar Perm(A₀) este o permutare a vectorului A₀, prin A₀ notandu-se valoarea initiala a vectorului A

9. Descompunerea unui numar in produs de doi factori specificatia:

Preconditia: nIN

Postconditia: n=x*y