Rezumat: Considerăm o schemă pentru construirea unui ciclu "în timp" cu ajutorul unui invariant, adică o afirmație care este menținută de fiecare dată când corpul bucla este executat. Aplicarea acestei scheme face posibilă construirea conștientă a unui algoritm și demonstrarea corectitudinii muncii sale asupra textului, fără a se recurge la testare. Aplicarea schemei este ilustrată prin exemple: algoritmul euclidian pentru calculul celui mai mare divizor comun, algoritmul de exponentizare rapidă, algoritmul Euclidian extins, calculul aproximativ al logaritmului fără utilizarea extensiei seriilor.
Utilizarea corectă a designului unei bucla prezintă întotdeauna unele dificultăți. Utilizarea teoriei elementare ajută la evitarea greșelilor și facilitează scrierea programelor complexe.
Ideea de bază este după cum urmează. În timpul executării unui ciclu, valorile unui set de variabile se modifică. Este necesar să se găsească relația dintre schimbarea variabilelor, care rămâne constantă. Această relație se numește ciclul invariant. Construcția conștientă a ciclului "încă" este întotdeauna legată de formularea și utilizarea explicită a ciclului invariant.
Formula explicită a invariantului ajută la scrierea inițializării variabilelor care sunt executate înainte de începerea buclei. și corpul ciclului. Inițializarea trebuie să garanteze că invarianta este executată înainte ca buclele să înceapă. Corpul ciclului trebuie construit astfel încât să asigure conservarea invarianților. (Mai exact, din faptul că invarianta este executată înainte de execuția corpului buclei, invarianta trebuie să se termine după sfârșitul corpului buclei.) În execuția corpului buclei, invarianta poate fi încălcată.)
Terminați ciclul. ca regulă, este asociată cu o valoare limitată. care crește sau scade monotonic în mod monotonic cu fiecare împlinire a corpului ciclului. Bucla "până" se termină când starea după cuvântul "până" în antetul bucla devine falsă. În consecință, această condiție trebuie să depindă direct sau indirect de o cantitate care scade monotonic sau crește pe măsură ce ciclul se desfășoară. Când atinge o anumită valoare, condiția trebuie să devină falsă. Condiția pentru finalizarea unui ciclu este negarea condiției după cuvântul "în timp" în antetul buclă.
Execuția ciclului invariant și, în același timp, condiția de terminare trebuie să asigure rezolvarea sarcinii cerute.
Schema generală
Indicăm prin X setul tuturor seturilor posibile de valori ale tuturor variabilelor care se modifică în timpul executării ciclului. Setul X este denumit uneori faza, sau configurația, spațiul problemei. Un invariant este o condiție I (x). care depinde de punctul x din setul X și presupune valoarea "true" sau "false". (Matematicienii numesc astfel de condiții predicate.) În procesul de inițializare, x primește valoarea x0. că condiția I (x0) este adevărată.
Denumim condiția de terminare a ciclului prin Q (x). Condițiile I (x) și Q (x) trebuie alese astfel încât adevărul simultan I (x) și Q (x) să furnizeze soluția la problema necesară: găsirea punctului x cu proprietățile cerute.
Corpul unui ciclu poate fi tratat ca o mapare a unui punct x la un nou punct T (x) din același set X:
Starea I (x) este invariantă pentru T. dacă I (x) este adevărată, atunci I (T (x)) este de asemenea adevărată.
Schema generală pentru construirea unui ciclu folosind un invariant este după cum urmează:
Bineînțeles, această schemă nu are nicio valoare fără capacitatea de ao aplica în practică. Să luăm în considerare câteva exemple importante de utilizare a acesteia.