Bucla invariant este o expresie matematică (în mod tipic - egalitatea), în care include, în mod inevitabil, cel puțin unele variabile ale căror valori variază de la un pasaj la un alt ciclu. Invarianta este construit astfel încât să fie adevărat, imediat înainte de a ciclului de execuție (înainte de a intra prima iterație) și după fiecare iterație. Mai mult decât atât, în cazul în care variabilele invariante sunt definite într-un ciclu (de exemplu, contra ciclu pentru Ada sau Pascal), pentru a intra în ciclul în care sunt considerate acele valori care vor primi în momentul de inițializare.
Dovada corectitudinii unui ciclu cu utilizarea unui invariant
Ordinea de dovedire a operabilității unui ciclu cu ajutorul unui invariant reduce la următoarele:
- Se dovedește că expresia invariantului este adevărată înainte de începerea ciclului.
- Se demonstrează că expresia invarianților își păstrează adevărul după execuția corpului ciclului; Astfel, prin inducție se dovedește că, la sfârșitul întregului ciclu, invariabilul va fi satisfăcut.
- Este dovedit faptul că adevărul invariante dincolo de variabilele ciclului va fi exact valoarea pe care doriți să obțineți (acest lucru este determinat de expresia elementară a invariante și cunoscute valorile finite ale variabilelor pe care starea de finalizare a ciclului).
- Se dovedește (posibil fără utilizarea unui invariant) că ciclul este finalizat, adică, condiția de terminare va fi îndeplinită mai devreme sau mai târziu.
- Adevărul afirmațiilor dovedite în etapele anterioare indică clar că ciclul va fi executat într-un timp finit și va da rezultatul dorit.
De asemenea, invarianții sunt utilizați în proiectarea și optimizarea algoritmilor ciclici. De exemplu, pentru a se asigura că ciclul optimizat a fost corect, este suficient pentru a dovedi că invarianta bucla nu este rupt, iar starea este ciclu realizabil este complet.
notițe
Articole similare
Trimiteți-le prietenilor: