Extras din curs

În limbajul Pascal exist_ trei instruc_iuni iterative: while, repeat _i for. Fa__ de situa_ia în care erau utilizate doar instruc_iuni de atribuire _i de decizie, justificarea corectitudinii algoritmilor iterativi cere un plus de creativitate. Verificarea instruc_iunii {P} x := e {Q} se reduce la verificarea implica_iei P Þ Qxe & def(e) iar verificarea instruc_iunii {P} if c then A else B{Q}

se reduce la verificarea implica_iei P Þ def(c) _i a instruc_iunilor {P&c} A {Q} _i {P & not c} B {Q}. Se observ_ c_ aceast_ ac_iune de reducere este extrem de simpl_, deoarece propriet__ile Qxe, P & not c, P & c se ob_in direct din constituen_ii instruc_iunii ini_iale prin opera_ia de substituire sau prin aplicarea unor operatori logici (not, & etc.)

În contrast, corectitudinea instruc_iunilor iterative se stabile_te utilizînd propriet__i a c_ror formulare este mai dificil_.

2.5.1 Regula instruc_iunii while

În limbajul Pascal, instruc_iunea while are forma:

while c do B

Instruc_iunea B este executat_ în mod repetat, atîta timp cît condi_ia c este adev_rat_. O executare a instruc_iunii B se nume_te itera_ie. Dup_ ultima itera_ie condi_ia c devine fals_. Dac_ c este fals_ de la început, atunci exist_ zero itera_ii. Dac_ c este totdeauna adev_rat_, num_rul de itera_ii este infinit _i instruc_iunea while nu se termin_.

Reamintim c_ o instruc_iune {P} A {Q} este corect_ dac_ atunci cînd datele de intrare satisfac proprietatea P rezult_ c_:

a) instruc_iunea A se termin_ în interval finit de timp;

b) datele de ie_ire satisfac proprietatea Q.

În cazul instruc_iunii de atribuire _i a instruc_iunii de decizie s-a insistat mai mult pe punctul b al acestei defini_ii deoarece punctul a rezult_ direct. Într-adev_r, dac_ evaluarea expresiei e se face în timp finit, atunci evident c_ instruc_iunea x:=e se termin_ în timp finit. În cazul instruc_iunii while ambele puncte au o tratare echilibrat_, deoarece problema termin_rii acestei instruc_iuni este mai dificil_.

Exemplul 1.§.2.5.1. Fie instruc_iunile urm_toare, prin care se calculeaz_ suma elementelor unui _ir finit x1,... xn de numere întregi, unde 0 £ n £ 100:

{P: 0 £ n £ 100}

s := 0; i := 1;

while i <= n do begin

s := s + x[i];

i := i + 1

end

{Q: s = x[k]}

_irul x1,... xn este presupus a fi reprezentat printr-un vector x ce are indicii în intervalul [1, 100]; numai primele n componente ale vectorului sînt definite (adic_ au valori atribuite). Suma cerut_ va fi dat_ de valoarea variabilei s.

În mod obi_nuit, testarea acestor instruc_iuni se face verificînd valoarea lui s pentru cîteva cazuri particulare ale lui n _i ale _irului x1,... xn. Se poate observa c_ dac_ n = 0, atunci programul se termin_ cu valoarea 0 pentru s, ceea ce este corect deoarece prin defini_ie x[k] este 0. Dac_ n = 1, atunci în instruc_iunea while se execut_ o singur_ itera_ie, dup_ care programul se termin_ (deoarece dup_ aceast_ itera_ie i devine 2 _i condi_ia i <= n nu mai este îndeplinit_). Valoarea calculat_ a lui s este corect_, deoarece 0 + x[1] este x[k].

Verificarea poate fi continuat_ _i pentru alte valori ale lui n; se va constata de fiecare dat_ c_ instruc_iunile sînt corecte. De aici nu se poate îns_ afirma c_ instruc_iunile sînt corecte pentru orice valoare a variabilei n; se poate recunoa_te în test_rile efectuate etapa de verificare dintr-o demonstra_ie prin induc_ie matematic_ a unei propriet__i P(n); lipse_te îns_ etapa P(k) Þ P(k+1). Aceast_ lips_ va fi suplinit_ prin regulile de corectitudine prezentate în acest paragraf.

Prin urmare, se va încerca un alt ra_ionament din care s_ rezulte cu rigurozitate c_, dac_ datele de intrare satisfac propriet__ile cerute, atunci:

a) procesul de calcul se termin_ într-un interval finit de timp.