Automatizarea verificării corectitudinii programelor scrise în limbaj imperativ

ing. Horaţiu Voicu
Universitatea Tehnică “Gh. Asachi”, laşi
Facultatea de Automatică şi Calculatoare

Rezumat: Lucrarea prezintă o modalitate în care se poate realiza verificarea automată a corectitudinii programelor scrise în limbaje imperative. Pornind de la noțiunile teoretice necesare inițierii în domeniu (logica Floyd-Hoare [1]), se prezintă o implementare în limbajul CAML Light a unui verificator de programe care este format din două funcții principale: un demonstrator de teoreme (a) şi un generator de condiţii de verificare (b). Programul (algoritmul care se doreşte a fi testat) este furnizat verificatorului de programe, care prin intermediul funcţiei (b), generează o serie de condiţii de verificare, furnizate funcţiei (a) care încearcă să le demonstreze. În caz că reuşeşte, înseamnă că programul este corect. În caz contrar, nu se poate trage nici o concluzie. Un astfel de program este util în practică atunci când o testare exhaustivă a unui algoritm este imposibil de realizat şi este utilizat, mai ales, în domeniul producerii software-ului care controlează activități potenţial dăunătoare omului (convertirea energiei atomice în energie electrică, ghidarea navetelor spaţiale).

Cuvinte cheie: condiţii de verificare, demonstrator de teoreme, ß-conversie, specificaţie, adnotare, limbaj funcțional.

Vizualizează articolul complet

COORDONATELE PENTRU CITAREA ACESTUI ARTICOL SUNT URMĂTOARELE:
Horaţiu Voicu, Automatizarea verificării corectitudinii programelor scrise în limbaj imperativ, Revista Română de Informatică şi Automatică (Romanian Journal of Information Technology and Automatic Control), ISSN 1220-1758, vol. 6(1), pp. 19-25, 1996.