VERIFICARE FORMALIZATA A PROGRAMELOR

VERIFICARE FORMALIZATA A PROGRAMELOR

Din capitolul anterior reiese rolul deosebit al operatiei de testare in semnalarea unor eventuale erori; ea este utila si pentru a ne familiariza cu algoritmul si a capata incredere in functionarea sa. Dar prin teste, oricat de numeroase ar fi ele, nu se poate garanta functionarea corecta, mai ales daca programul este foarte complex.

Au existat programe de importanta deosebita, realizate de programatori profesionisti, a caror functionare necorespunzatoare nu a putut fi semnalata prin teste si a generat situatii critice (printre altele cazul unui program de pe calculatoarele unei nave Soiuz TM).

S-a simtit deci nevoia utilizarii altor metode de verificare a programelor. In continuare va fi prezentata o astfel de metodologie de esenta matematica, prin care se poate demonstra in mod riguros ca:

a) procesul de calcul se termina in timp finit pentru orice date de intrare din domeniul specificat in enuntul problemei;

b) dupa terminarea procesului de calcul, datele de iesire ofera solutia problemei pentru care algoritmul a fost creat.

Metodologia isi are originea in lucrarile informaticienilor R. W. Floyd, C.A.R. Hoare, E. W. Dijkstra, Z. Manna. Ea se bazeaza pe analiza, instructiune cu instructiune, a textului programului. In cazul de fata, ne vom referi la programe scrise in limbajul Pascal, alcatuite din instructiuni de atribuire, instructiuni de decizie (if) si instructiuni iterative (while, repeat, for).

In cele ce urmeaza, o secventa de instructiuni (algoritm) A va fi precedata totdeauna de un comentariu P care descrie proprietatile datelor de intrare si va fi urmata de un comentariu Q ce descrie proprietatile datelor de iesire. P va fi numita proprietate initiala sau preconditie iar Q proprietate finala sau postconditie. Constructia rezultata A mai este numita si formula de corectitudine totala.

Definitia 1. Un algoritm A se spune ca este corect in cazul in care:

daca datele de intrare satisfac proprietatea P,

atunci

1) executarea lui A se termina (intr-un interval finit de timp) si

2) datele de iesire satisfac proprietatea Q.

Algoritmul A nu este neaparat un program Pascal; el poate fi o secventa oarecare

de instructiuni Pascal. Se va spune deci, dupa caz, ca programul este corect sau instructiunile sunt corecte.

Exemple

1) Instrucsiunea x := x + 1 este corecta si exprima faptul evident ca daca x are valoarea zero inainte de executarea instructiunii x := x + 1, dup_ executare va avea valoarea 1.

2) Este de asemenea corecta instructiunea:

if x < 0 then x := -a

care exprima faptul ca prin aceasta instructiune se calculeaza valoarea absoluta a lui x.

3) Instructiunile:

if x >= y

then m := x

else m := y

sunt corecte _i calculeaz_ maximul dintre x _i y.

4) Instruc_iunea: x := x + 1 nu este corect_.

5) Instruc_iunea urm_toare:

while x <> y do

if x > y then x := x - y

else y := y - x

nu este corect_, deoarece dac_ x = 0 _i y = 1, executarea sa nu se termin_ (a se vedea _i exemplul 1..1.2.3).

Anumite rela_ii intre datele algoritmului sint adev_rate indiferent de valorile variabilelor ce apar in ele (de exemplu x = x, x ³ x - 1, 1 = 1 etc.); o astfel de rela_ie va fi desemnat_, in cele ce urmeaz_, prin constanta true. Altele sint false indiferent de valorile variabilelor (x <> x; 1 = 2 etc.) _i vor fi desemnate prin constanta false.

Observa_ie. Algoritmul A este corect, oricare ar fi A _i Q. Aceasta este o consecin__ a faptului c_ enun_ul 'datele de intrare satisfac proprietatea false' este fals.

Observa_ie. Algoritmul A este corect dac_ _i numai dac_ executarea lui A se termin_ atunci cind datele ini_iale satisfac proprietatea P. Intradev_r, punctul 2 al defini_iei 1..2 este in mod banal satisf_cut.

Exerci_iu. Da_i exemplu de propriet__i P, Q _i instruc_iune care se termin_ A, astfel incit A _i A s_ nu fie corecte.

R. P: n ³ 0

Q: n = 2

A: n := n + 1.

Corectitudinea instruc_iunilor foarte simple se stabile_te cu destul_ u_urin__. Algoritmii complec_i pot fi, la rindul lor descompu_i in elemente simple a c_ror corectitudine se analizeaz_. Este deci important s_ dispunem de reguli precise pe baza c_rora elementele constitutive corecte pot fi asamblate spre a ob_ine algoritmi corec_i. Aceste reguli vor fi prezentate in paragrafele urm_toare.

Observa_ia 1..2. Dac_ A _i A sint corecte, atunci A este corect_.

2.1 Regula compunerii secven_iale

S_ presupunem c_ se analizeaz_ corectitudinea algoritmului A unde A este de fapt alc_tuit din dou_ p_r_i, B _i C, astfel c_ mai intii se execut_ B, apoi C. Cu alte cuvinte, datele de ie_ire de la B sint date de intrare pentru C. In limbajul Pascal, o astfel de situa_ie apare cind A este B; C.

Vom enun_a urm_toarea regul_, numit_ regula compunerii secven_iale

COMP:

dac_ B _i C sint algoritmi corec_i,

atunci B ; C este algoritm corect.

Intr-adev_r, dac_ datele de intrare pentru A satisfac proprietatea P, atunci executarea primei p_r_i B a lui A se termin_ _i datele rezultate satisfac proprietatea R (c_ci B este corect). Dar acestea sint date de intrare pentru C, a doua parte a lui A; deoarece C este corect, executarea lui C se termin_ iar datele de ie_ire satisfac proprietatea Q; dar acest lucru inseamn_ c_ executarea lui A s-a terminat _i datele de ie_ire satisfac pe Q.

Dac_ se dore_te s_ se pun_ in eviden__ faptul c_ s-a aplicat regula compunerii secven_iale pentru 'asamblarea' algoritmilor corec_i  B  _i  C , se scrie algoritmul ob_inut in forma:

B;  C

(proprietatea intermediar_ R apare explicit).

Exemplu. Algoritmul

x := x + 1; x := 2 * x

este corect _i se ob_ine prin compunerea secven_ial_ a algoritmilor corec_i

x := x + 1

_i x := 2 * x .

Prin aplicarea succesiv_ a acestei reguli de dou_ ori, din algoritmi corec_i de forma

A₁ , A₂ , A₃

se ob_ine algoritmul corect

A₁ ; A₂ ; A₃ .

El poate fi scris _i in forma

 A₁;  A₂ ; A₃

punind in eviden__ elementele constitutive.

Exemplu. Instruc_iunile urm_toare sint corecte:

x := x + y

y := x - y

x := x - y

Aplicind de dou_ ori regula compunerii secven_iale se ob_ine algoritmul corect:

x := x + y ; y := x - y ; x := x - y

prin care se interschimb_ valorile lui x _i y.

Regula compunerii secven_iale poate fi de fapt aplicat_ in cazuri mai generale:

COMPG:

dac_ A₁ , A₂ , A_n

unde n ³ 2, sint algoritmi corec_i,

atunci A₁ ; A₂ ; A_n este algoritm corect.

2.2. Regula implica_iei

Sint situa_ii in care se _tie c_ A este corect, dar algoritmul A urmeaz_ s_ se aplice in condi_ii ini_iale 'mai tari' ca P, pentru a ob_ine rezultate ce indeplinesc condi_ii 'mai slabe' decit Q.

Reamintim c_ o proprietate P₁ este mai tare decit P dac_ din P₁ rezult_ P (P₁ implic_ P, notat P₁ Þ P). Se mai spune in acest caz c_ P este mai slab decit P₁.

Exemplu. Instruc_iunea x := x + 1 este corect_. S_ presupunem ins_ c_ instruc_iunea x := x + 1 se aplic_ in situa_ia x = 1 (care este mai tare decit x³0) pentru a ob_ine date de ie_ire care satisfac condi_ia x³-1 (care este mai slab_ decit x > 0, deoarece x > 0 Þ x ³ -1). Este u_or de v_zut c_ instruc_iunea  x := x + 1  este corect_.

In astfel de situa_ii se aplic_ urm_toarea regul_, numit_ regula implica_iei:

IMPL:

dac_ A este corect,

P₁ Þ P (P₁ mai tare ca P)

Q Þ Q₁ (Q₁ mai slab decit Q),

atunci A este corect.

2.3 Regula instruc_iunii de atribuire

Instruc_iunea de atribuire este elementul fundamental al limbajelor de programare procedurale. Pin_ acum, faptul c_ un algoritm de forma  x := y + 1  este corect a fost acceptat pe baze intuitive. In cazul in care propriet__ile datelor de intrare _i de ie_ire au descrieri mai complicate, ra_ionamentul intuitiv poate deveni greoi. Din acest motiv vom utiliza procedee mai formalizate, care se bazeaz_ pe descrierea datelor prin formule de genul celor utilizate in logica matematic_.

In mod frecvent, rela_iile dintre valorile variabilelor sint descrise in programe prin expresii booleane (condi_ii) in care se folosesc operatorii rela_ionali <, >, >=, <=, <>, = _i operatorii logici and, or, not ca in exemplele: x = y+1; x <> y; x > 1; (x = 1) or (x = 2). Ele sint evaluate de calculator _i pot fi adev_rate, false, sau nedefinite; de pild_, condi_ia not(1 div x = 1) este nedefinit_ dac_ x este 0. Pentru a exprima (in afara programelor) propriet__ile datelor se utilizeaz_ construc_ii mai generale decit condi_iile booleane, in care pot ap_rea conectorii logici: & (_i); (sau); (nega_ie); Þ (implica_ie); Û (echivalen__). Acestea vor fi numite formule logice _i ele pot fi satisf_cute sau nu de valorile variabilelor. Spre exemplu, (x = 1)  (x = 2) este o formul_ satisf_cut_ de valorile 1 _i 2 ale lui x; formula (x £ y) & (y £ z) Þ (x £ z) este satisf_cut_ de orice valori reale ale variabilelor x, y _i z. Formulele not(1 div x = 1) _i (1 div x = 1) nu sint satisf_cute de valoarea 0 a lui x dar pentru aceea_i valoare formula (1 div x = 1) este satisf_cut_.

Intr-o formul_ oarecare R o variabil_ x poate fi inlocuit_ (substituit_) printr-o alt_ expresie e, ob_inind o nou_ rela_ie, notat_ R^x_e. Spre exemplu, (x > y)_x+1^x este x + 1 > y; ((x £ y) & (y £ z) Þ (x £ z))₁^y este (x £ 1) & (1 £ z) Þ (x £ z); (sin x £ x)^x_cos x este sin cos x £ cos x etc.

Fie P o proprietate (formul_ logic_) in care, pe ling_ variabila x, mai apar _i alte variabile x₁, x_n _i fie v, v₁, v_n valori oarecare ale acestor variabile. Efectul substituirii variabilei x printr-o expresie e in P este urm_torul: valoarea formulei ob_inute P_e^x, calculat_ pentru valorile v, v₁ v_n ale variabilelor x, x₁, x_n, este identic_ cu valoarea formulei P, calculat_ in situa_ia in care valoarea lui x este e(v, v₁, v_n), iar valorile celorlalte variabile r_min neschimbate. Pe scurt,

P_e^x(v, v₁, v_n) = P(e(v, v₁,v_n), v₁, v_n).

Spre exemplu, dac_ P este x ³ y + z iar e este x + 1 atunci P_x+1^x este x + 1 ³ y + z. Se observ_ c_ e(v, v₁, v₂) = v + 1 _i c_ P_e^x(v, v₁, v₂) = (v + 1 ³ v₁ + v₂). Avem de asemenea P(v+1, v₁, v₂) = (v + 1 ³ v₁ + v₂).

Formule mai complicate se ob_in prin utilizarea cuantificatorului universal ' (oricare) _i a cuantificatorului existen_ial $ (exist_).

O formul_ 'x P este adev_rat_ dac_ oricare ar fi valoarea v a lui x rezult_ c_ P^x_v este adev_rat_ . Spre exemplu, dac_ x ia valori in mul_imea numerelor naturale, formula 'x(x ³ 0) este adev_rat_ c_ci oricare ar fi num_rul natural n, formula (x ³ 0)^x_n, adic_ n ³ 0 este adev_rat_.

O formul_ $x P este adev_rat_ dac_ exist_ o valoare v a lui x, astfel incit P^x_v s_ fie adev_rat_. Spre exemplu, dac_ x ia valori numere naturale, formula $x(x > 10) este adev_rat_ (se poate lua in rolul lui v valoarea 11 _i (x > 10)^x₁₁ este adev_rat_). Formula 'x $y(x ³ y) este adev_rat_, c_ci pentru orice valoare a lui x avem c_ ($y(x ³ y))^x_v (adic_ $y(v ³ y)) este adev_rat_; intr-adev_r, (v ³ y)^y₀ (adic_ v ³ 0) este adev_rat_.

Observa_ie. Dac_ formula P nu con_ine cuantificatorii ' sau $, substitu_ia se face inlocuind fiecare apari_ie a lui x cu expresia e, a_a cum s-a f_cut in exemplele anterioare. In cazul formulelor ce con_in cuantificatori, pentru ca substitu_ia s_ aib_ efectul prezentat mai inainte sint necesare anumite precau_ii.

In primul rind, nu pot fi substituite decit acele apari_ii ale lui x care nu sint legate de cuantificatori (aceste apari_ii se numesc libere). Spre exemplu, in (x ³ 0) & $x(x ³ 10) nu poate fi substituit_ decit prima apari_ie a lui x; astfel, (x ³ 0 & $x(x ³ 10))^x₉ este (9 ³ 0 & $x(x ³ 10). Efectul dorit prin opera_ia de substituire se p_streaz_, c_ci P(9) = P₉^x = true. Dac_ in mod incorect se substituie _i a treia apari_ie a lui x prin 9, ob_inem formula 9 ³ 0 & $x(9 ³ 10), care este fals_; deci P(9) ¹ P₉^x.

In al doilea rind, dac_ expresia e con_ine o variabil_ care, dup_ substituire, se poate lega de un cuantificator atunci substituirea nu se face direct. Spre exemplu, fie P formula 'y(1 ³ x), unde x _i y iau valori numere naturale.

Dac_ s-ar substitui direct x prin y + 1, atunci formula ob_inut_ P^x_e ar fi 'y(0 ³ y). Se observ_ cum variabila y este legat_ acum de cuantificatorul 'y. Efectul substitu_iei nu este in acest caz cel dorit. Intr-adev_r, s_ consider_m c_ x are valoarea 1 _i y valoarea 0. Se observ_ c_ P^x_e(1, 0) = 'y(0 ³ y) este fals_ dar P(e(1, 0), 0) = P(1, 0) = 'y(1 ³ 1) este adev_rat_.

Din acest motiv, dac_ expresia e con_ine o variabil_ y care dup_ substituire se leag_ de un cuantificator 'y sau $y din P, substitu_ia lui x prin e se face dup_ ce variabila y este inlocuit_ in P printr-o variabil_ nou_ z (care nu mai apare nici in P, nici in e _i este diferit_ de x). Astfel, in cazul anterior ['y(1 ³ x)]^x_y+1 = ['z(1 ³ x)]^x_y+1 = 'z(0 ³ y). Efectul opera_iei de substituire se p_streaz_;

de pild_ P^x_y+1(1,0) = 'z(0 ³ y)(1,0) = 'z(0 ³ 0)

iar P(0+1,0) = 'y(1 ³ x)(1,0) = 'y(1 ³ 1).

Ambele formule sint adev_rate.

O discu_ie mai ampl_ despre condi_ii _i formule logice se face in anexa A. Aceasta poate fi util_ cititorilor mai pu_in familiariza_i cu logica sistemelor de calcul _i cu logica matematic_.

2.3.1 Instruc_iuni de atribuire la variabile simple

Fie x := e o instruc_iune de atribuire, unde x este o variabil_ simpl_ (f_r_ indici). Este evident c_ pentru terminarea normal_ a acestei instruc_iuni este necesar ca valoarea expresiei e s_ fie bine definit_, adic_ variabilele care intervin in alc_tuirea ei s_ aib_ valori atribuite la un moment anterior iar in cursul evalu_rii s_ nu apar_ situa_ii anormale de tipul imp_r_ire la zero, dep__ire a domeniului etc.

Vom nota prin def(e) proprietatea satisf_cut_ doar de acele date ini_iale pentru care evaluarea expresiei e se desf__oar_ normal.

Exemple.

1) def(1/y +1) este proprietatea y ¹ 0;

2) Dac_ vectorul b este definit prin

var b : array [1..10] of integer;

atunci def(b[i]) este proprietatea 1 £ i £ 10.

Conven_ie. Exist_ expresii a c_ror bun_ definire nu pune probleme deosebite, fiind suficient ca variabilelor care apar in structura lor s_ li se fi atribuit valori mai inainte. De pild_, in programul

var x : integer;

begin x := x + 1 end.

expresia x + 1 nu este bine definit_. Pentru a simplifica expunerea in cele ce urmeaz_ se presupune c_ variabilelor dintr-o expresie le-au fost atribuite valori la un moment anterior. In consecin__, pentru o expresie e a c_rei bun_ definire depinde doar de acest lucru, vom conveni c_ def(e) = true _i vom spune c_ in acest caz condi_iile de definire nu sint critice.

Exemplu. def(x+1) = true; def(x*y) = true.

Efectul substitu_iei lui x prin e intr-o formul_ P ne permite s_ enun__m urm_toarea regul_ a instruc_iunii de atribuire:

ATR:

instruc_iunea

x := e

este corect_.

Exemplu. Deoarece (x > 0)^x_x+1 este x > -1 iar def(x > 0) = true (prin conven_ie), rezult_ conform regulii instruc_iunii de atribuire, c_ instruc_iunea

x := x + 1 este corect_. Din acela_i motiv sint corecte instruc_iunile urm_toare:

x := x * x

x := 2 * y + 3

x := x + y

x:=(x-y)*(x+y)

i := i + 1

i := i - 1

i := j

x := 1

x := y

Exemplu. Dac_ b este declarat prin

var b : array [1..10] of integer;

atunci

def(b[i]) = (1 £ i £ 10).

Deci urm_toarea instruc_iune

s := s + b[i]

este corect_.

Remarc_. Aplicarea regulii instruc_iunii de atribuire se face in mod frecvent inso_it_ de regula implica_iei. Astfel, dac_ se dore_te s_ se arate c_ instruc_iunea x := e este corect_, este suficient s_ se arate c_ P Þ Q^x_e & def(e) este adev_rat_, adic_ P este mai tare decit Q^x_e & def(e). Aceast_ implica_ie este demonstrat_ utilizind propriet__ile elementelor ce apar in P _i Q_e^x, adic_ variabile _i constante de diferite tipuri (numere intregi, numere reale, caractere, vectori etc.), func_ii cu propriet__i cunoscute (logaritm, exponen_ial_, func_ii trigonometrice, maxim, minim, cel mai mare divizor comun, div, mod etc.). In acest fel, ra_ionamentul este 'transferat' din domeniul program_rii in domeniul matematicii.

Exemplul 1..2.3.1. Instruc_iunea urm_toare:

y := y - x

este corect_. Semnifica_ia sa este c_ instruc_iunea de atribuire nu modific_ cel mai mare divizor comun pozitiv (x, y) dar mic_oreaz_ suma celor dou_ numere (a se vedea algoritmul CMMDC din exemplul 1..1.2.3). Conform remarcii anterioare, este suficient s_ se demonstreze c_ P Þ Q^y_y-x, adic_:

x ¹ y & x <= y & x > 0

& y > 0 & c = (x, y) & u = x + y

Þ

x > 0 & y > 0

& c = (x, y - x) & u > x + y - x

Utilizind faptul c_ (x, y) = (x, y - x) (Algebra, manual pentru clasa a X-a) _i propriet__ile rela_iei de ordine >, rezult_ c_ implica_ia este adev_rat_.

Remarc_. In cazul unui algoritm alc_tuit din mai multe instruc_iuni de atribuire succesive, se aplic_ regula instruc_iunii de atribuire pentru toate instruc_iunile, in ordinea de la dreapta la stinga. De pild_, in cazul

x := e; y := f;

avem c_ urm_toarele instruc_iuni sint corecte:

y := f

x := e

Aplicind regula compunerii secven_iale, rezult_ c_ instruc_iunile

x := e ; y := f

sint corecte. Dac_ P este mai tare decit (Q^y_f)^x_e & def(f^x_e) & def(e), atunci conform regulii implica_iei, rezult_ c_ algoritmul ini_ial este corect. Dac_ e _i f sint expresii cu proprietatea def(e) = def(f) = true (condi_iile de bun_ definire a expresiilor e _i f nu sint critice), atunci este suficient ca P s_ fie mai tare decit (Q^y_f)^x_e.

Exemplu. Algoritmul urm_tor:

t := x ; x := y ; y := t

este corect (aceast_ secven__ de trei instruc_iuni se utilizeaz_ pentru interschimbarea valorilor lui x _i y). Intr-adev_r, condi_iile de bun_ definire a expresiilor x, y _i t nu sint critice (def(x) = def(t) = def(y) = true). Aplicind de trei ori regula instruc_iunii de atribuire, de la dreapta la stinga, rezult_ c_ instruc_iunile urm_toare sint corecte:

y := t

deoarece (x = b & y = a)^y_t este x = b & t = a;

x := y ;

t := x ;

Se aplic_ apoi regula compunerii secven_iale.

Exemplu. Instruc_iunile urm_toare sint corecte, unde b este declarat prin

var b : array[1..10] of integer;

i := i-1; s := s + b[i]

In acest caz, avem def(s + b[i]) = 1 £ i £ 10. Conform regulii ATR, instruc_iunile:

s := s + b[i]

_i

i := i - 1

sint corecte. In cazul cind 2 £ i £ 11, avem

b[k] = b[i-1] + b[k].

Prin urmare

s = b[k] & 2 £ i £ 11 Þ s + b[i-1] = b[k]

_i se aplic_ regula implica_iei.

Exemplu. Instruc_iunile urm_toare:

n := n + 1 ; x := x * n ,

sint corecte, unde n _i x sint variabile ce iau valori numere naturale.

Intr-adev_r,

x := x * n

_i n := n + 1

sint corecte, conform regulii instruc_iunii de atribuire.

Dar x = n! Þ x * (n+1) = (n + 1)!; conform regulilor implica_iei _i compunerii secven_iale, rezult_ c_ algoritmul ini_ial este corect.

Exemplu. Urm_toarele instruc_iuni sint corecte.

a := a + 1 ; b := a

Intr-adev_r,

b := a

_i a := a + 1

sint corecte. In plus, a + 1 = a + 1 este totdeauna adev_rat_ (astfel de formule am convenit s_ le not_m prin true).

Exemplul 2..2.3.1. Instruc_iunile urm_toare:

q := a div b ; r := a mod b

sint corecte. Aceste instruc_iuni apar in algoritmul IMP_R_IRE (exemplul 2..1.2.3). Aici intervin condi_iile critice de bun_ definire

def(a div b) = def(a mod b) = (b ¹ 0)

Este suficient s_ ar_t_m c_ implica_ia:

b ¹ 0 Þ a = b * (a div b) + a mod b

& 0 £ ½ a mod b ½ < ½b½

este adev_rat_. Aceast_ implica_ie, de_i destul de simpl_, nu poate fi demonstrat_ f_r_ cunoa_terea propriet__ilor operatorilor div _i mod.

Reamintim c_ a div b, pentru a, b I Z, b ¹ 0 este un num_r intreg cu propriet__ile urm_toare:

i) dac_ a/b ³ 0 atunci a div b £ a/b < a div b + 1;

ii) dac_ a/b < 0 atunci a div b - 1 < a/b £ a div b.

Spre exemplu, -5 div 2 este -2 deoarece -2-1 < -2, 5 £ -2 iar -5 div -2 este 2.

Se _tie de asemenea c_ a mod b = a - (a div b) * b. S_ presupunem, spre exemplu, c_ a > 0 _i b < 0. In acest caz,

a div b - 1 < a/b £ a div b (proprietatea ii).

De aici (a div b) * b - b > a ³ (a div b) * b,

adic_ -b > a mod b ³ 0;

prin urmare, 0 £ a mod b < ½b½.

Celelalte cazuri sint analoge.

Exerci_ii. Demonstra_i c_ urm_toarele instruc_iuni sint corecte:

a) i := i + 1 ; j := j + 1

b) j = j + i ; i := i + 1

c) a := 0 ; n := 1

d)

s := s + b[i] ; i := i + 1

unde b este declarat prin

var b: array[0..n-1] of integer;

e)

a:= a div 2 ; b := 2 * b

Indica_ie: se va utiliza faptul c_

a num_r par Þ (a div 2) * 2 = a.

f)

i := 1 ; s := b[0]

unde b este definit prin

var b: array [0..n] of integer;

Observa_ia 1..2.3.1. Instruc_iunea

x := e

este corect_, conform regulii instruc_iunii de atribuire. Semnifica_ia sa este c_, prin atribuirea x:= e, valorilor altor variabile r_min neschimbate. Totu_i, in limbajul Pascal, evaluarea expresiei e poate provoca modificarea unor variabile, atunci cind func_iile ce apar in e provoac_ efecte laterale. Fie exemplul urm_tor:

var y : integer;

function e : integer;

begin

e := y;

y := 1

end;

var x : integer;

begin

y := 0;

x := e;

writeln ('y=', y)

end.

Din cauza efectelor laterale, asupra instruc_iunii x := e din exemplul de mai inainte nu se poate aplica regula instruc_iunii de atribuire. Intr-adev_r, in acest caz instruc_iunea  x := e  nu este corect_, deoarece evaluarea lui e modific_ valoarea lui y.

Aceea_i problem_ apare _i in cazul cind in e apar func_ii ce utilizeaz_ variabile globale, chiar dac_ nu le modific_. S_ consider_m programul Pascal urm_tor:

var x, y, a : integer;

function f : integer;

begin f := a end;

begin

a := 0; x := f ;

a := 1; y := f ;

writeln(x=y)

end.

Valorile lui x _i y sint diferite. _i totu_i, prin aplicarea regulii instruc_iunii de atribuire, avem c_:

a := 0

x := f

a := 1

y := f

sint corecte.

Prin aplicarea regulii de compunere secven_ial_, ar rezulta c_ datele finale satisfac x = y. Motivul acestei concluzii eronate este acela c_ variabila a nu apare explicit in membrul drept al instruc_iunii de atribuire _i deci opera_ia de substituire (x = f )^a₁ este inefectiv_.

Observa_ie. Regula instruc_iunii de atribuire se aplic_ numai in cazul cind calculul expresiei din dreapta semnului := nu modific_ valorile variabilelor _i toate variabilele ce influen_eaz_ calculul apar explicit in expresie.

Absen_a efectelor laterale ne permite s_ prelucr_m expresiile pe baza unor propriet__i care ne sint familiare din matematic_, cum ar fi, de pild_, comutativitatea opera_iilor de adunare _i inmul_ire. In prezen_a efectelor laterale, aceste propriet__i nu se mai p_streaz_. Astfel, in exemplul anterior, expresia y + e are acela_i rezultat ca y + y dar e + y inseamn_ de fapt y + 1 (s-a considerat c_ evaluarea operanzilor se face de la stinga la dreapta).

Exemplu. Fie urm_torul program Pascal:

var a, b : integer;

function f(x : integer) : integer;

begin f := x + a end;

function g(x : integer) : integer;

begin

g := x + a; a := 2 * x

end;

begin

a := 1;

b := g(1) * g(1);

a := 1;

b := sqr(g(1));

a := 0; b := f(1);

a := 1; b := f(1);

end.

Func_ia g are efecte laterale deoarece modific_ valoarea variabilei globale a. Datorit_ efectului lateral, se constat_ c_ g(1) * g(1) nu este acela_i lucru cu p_tratul lui g(1).

Abateri de la propriet__ile matematice apar chiar _i atunci cind valorile variabilelor globale sint utilizate dar nu sint modificate (deci efectele laterale sint absente). Astfel, cele dou_ apari_ii ale expresiei f(1) dau valori diferite, in func_ie de context.

Din acest motiv, in programare se face deseori recomandarea ca func_iile s_ fie astfel scrise incit executarea lor s_ nu modifice argumente sau variabile globale. In limbajul Ada modificarea argumentelor unei func_ii este semnalat_ drept eroare de compilare; efecte laterale sint ins_ posibile _i in acest limbaj prin modificarea variabilelor globale.

Exist_ opinii dup_ care func_iile cu efecte laterale ar trebui interzise prin semnalarea lor de c_tre compilator ca subprograme eronate. Aceast_ atitudine sever_ fa__ de efectele laterale face posibil_ verificarea mai sistematic_ a instruc_iunilor.

2.3.2 Instruc_iuni de atribuire la variabile cu indici

Pin_ acum, in mod deliberat, au fost evitate exemplele in care apar in partea sting_ variabile cu indici, ca in cazul b[i] := e, deoarece instruc_iunea b[i]:=e nu este totdeauna corect_. Spre exemplu, fie instruc_iunile i:=1; b[i]:=5 . Deoarece (b[1]=0)^b[i]₅ este tot b[1]=0, regula instruc_iunii de atribuire, aplicat_ in acest mod, ar conduce la concluzia c_ instruc_iunile de mai inainte sint corecte; se vede totu_i c_ valoarea lui b[1] a fost schimbat_ in mod indirect.

Fie b un vector declarat prin

var b : array [m..n] of T;

unde m £ n.

Exist_ dou_ moduri de a privi un astfel de vector. Cel mai adesea in programare se consider_ c_ b este o colec_ie alc_tuit_ din variabilele b[m], b[m+1], b[n] (citeodat_ se face _i presupunerea c_ loca_iile de memorie rezervate lor sint consecutive). In aceast_ accep_iune, instruc_iunea b[i] := e, unde m £ i £ n este v_zut_ ca afectind doar variabila b[i] a colec_iei.

De_i uzual, acest mod de a privi un vector nu este potrivit pentru aplicarea regulii instruc_iunii de atribuire, dup_ cum s-a v_zut mai inainte. Neajunsul s_u este c_ in analiza atribuirii aten_ia este concentrat_ pe o variabil_ din colec_ie, pierzind din vedere vectorul in ansamblu.

Vectorul b poate fi ins_ v_zut _i ca o func_ie cu domeniu intervalul [m, n] _i codomeniu T. Deci b este func_ia b:[m, n] T iar b[i] este de fapt valoarea func_iei b in i, notat_ in matematic_ prin b(i). In aceast_ accep_iune, proprie lucr_rilor [Dij 76], [HoWir 73], [DaHoDij 72] instruc_iunea

b[i] := e

transform_ func_ia b intr-o alt_ func_ie, pe care o vom nota prin b _i o vom numi variant_ a lui b. Este evident c_ noua func_ie este definit_ pentru m £ i £ n astfel:

Se vede din aceast_ defini_ie c_ varianta lui b difer_ de b doar in punctul i, ca efect al atribuirii.

Observa_ie. Dac_ j nu este in domeniul de indici, atunci b [j] _i b[j] sint amindou_ nedefinite. In defini_ia variantei, doar asupra lui i s-a pus condi_ia s_ fac_ parte din domeniul de indici.

Exemplu. Fie vectorul var x : array [1..3] of integer;

Presupunem c_ x[1]=10; x[2]=20; x[3]=30. Prin instruc_iunea de atribuire x[2]:=100 se ob_ine varianta x a lui x, cu urm_toarele valori:

x[1]=10; x[2]=100; x[3]=30.

Faptul c_ b este o func_ie, ne permite s_ concepem instruc_iunea

b[i] := e

ca fiind echivalent_ cu

b := b.

Ultima instruc_iune nu este conform_ cu sintaxa limbajului Pascal, ci este folosit_ ca o nota_ie ce sugereaz_ c_ atribuirea afecteaz_ vechea func_ie b, creind una nou_ (varianta lui b). Noua instruc_iune are in membrul sting o variabil_ simpl_ (f_r_ indici), iar regula instruc_iunii de atribuire poate fi aplicat_ in forma urm_toare:

ATRIND:

instruc_iunea

& def(e) & m £ i £ n}

b[i] := e

este corect_.

Exemplu. Fie vectorul b declarat prin

var b : array[1..10] of integer;

instruc_iunea de atribuire b[i] := 5 _i proprietatea P: b[1] = 0. Rezult_ c_ instruc_iunea urm_toare:

& 1 £ i £ 10}

b[i] := 5

este corect_. Proprietatea (b[1] = 0)^b_b este de fapt b[1] = 0 (s-a substituit b prin b ). Conform defini_iei variantei b, avem

In consecin__, rela_ia b [1] = 0 este echivalent_ cu i ¹ 1 _i b[1] = 0. Prin urmare instruc_iunea

b[i] := 5

este corect_ in conformitate cu regula instruc_iunii de atribuire. La aceea_i concluzie se ajunge _i urm_rind modul de executare al instruc_iunii b[i] := 5; se constat_ c_ dac_ i ar avea valoarea 1, atunci b[1] ar deveni egal cu 5.

Remarc_. Dificultatea in aplicarea acestei reguli const_ in manipularea expresiilor in care intervin variantele de vectori. Este util s_ se re_in_ c_ o rela_ie de genul

b [j] = v, unde m £ i £ n

este echivalent_, _inind cont de defini_ia func_iei b cu

(i = j & e = v) (i ¹ j & b[j] = v).

Simplific_ri ulterioare pot fi ob_inute _inind cont de echivalen_ele:

false & P º false; false P º P;

true & P º P; true P º true etc. (anexa A.3).

Exemple. In cele ce urmeaz_ se consider_ c_ 1 £ i £ 10 iar vectorul b este declarat prin

var b: array[1..10] of integer;

a) b [1] = 0 este echivalent cu

(i = 1 & 5 = 0) (i ¹ 1 & b[1] = 0),

adic_ i ¹ 1 & b [1] = 0 (deoarece 5 = 0 este false);

b) b [j] = 5

º (i = j & 5 = 5) (i ¹ j & b[j] = 5)

º i = j (i ¹ j & b[j] = 5)

º (i = j i ¹ j) & (i = j b[j] = 5)

º true & (i = j b[j] = 5)

º i = j b[j] = 5.

Exemplu. Instruc_iunea

b[i] := 5

este corect_. Intr-adev_r, regula instruc_iunii de atribuire ne asigur_ c_ instruc_iunea

{(b[i] = 5)^b_b & 1 £ i £ 10}

b[i] := 5

este corect_.

Dar (b[i] = 5)^b_b º b [i] = 5 º 5 = 5 º true.

Exemplu. Instruc_iunea

b[i] := 5

este corect_. Intr-adev_r, conform regulii instruc_iunii de atribuire

{(b[j] = 5)^b_b & 1 £ i £ 10}

b[i] := 5

este corect_. Dar

(b[j] = 5)^b_b

º b [j] = 5

º i = j b[j] = 5,

dup_ cum s-a v_zut intr-un exemplu anterior.

Aplicarea acestei reguli in cazul variabilelor cu indici poate p_rea incomod_ la inceput; ea devine ins_ atractiv_ pe m_sur_ ce c_p_t_m experien__ _i prezint_ avantajul c_, spre deosebire de analiza direct_ a execut_rii instruc_iunii, este mai riguroas_.

Exemplu. Instruc_iunea urm_toare:

b[i] := 5

este corect_. Vom calcula _i simplifica P^b_b. Avem:

(b[i] = b[j])^b_b

º b [i] = b [j]

º 5 = b [j]

º (i = j & 5 = 5) (i ¹ j & 5 = b[j])

º i = j (i ¹ j & 5 = b[j])

º (i = j i ¹ j) & (i = j 5 = b[j])

º true & (i = j 5 = b[j])

º i = j 5 = b[j].

In ob_inerea acestor echivalen_e s-a utilizat faptul c_ 1 £ i £ 10. Se aplic_ apoi regula instruc_iunii de atribuire.

Exemplu. Instruc_iunea urm_toare este corect_:

b[b[i]] := i

In acest exemplu, analiza direct_ cere un efort comparabil cu cel al calculului propriet__ii P^b_b. Intr-adev_r, avem:

(b[i] = i)^b_b

º b [i] = i

º (i = b[i] & i = i) (i ¹ b[i] & b[i] = i)

º (i = b[i] & true) false

º i = b[i].

Exemplu. Instruc_iunea urm_toare este corect_:

b[i] := i

In acest exemplu se poate afirma c_ analiza direct_ este mai greoaie decit calculul formal. Intr-adev_r:

(b[b[i]] = i)^b_b

º b [b [i]] = i

º b [i] = i

º i = i

º true.