Automation of Correctness Testing of the Software Written in An Imperative Language

Eng. Horaţiu Voicu
“Gh. Asachi” Technical University of Iassy
Faculty of Automatics and Computer Science

Abstract: 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).

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

View full text

CITE THIS PAPER AS:
Horaţiu Voicu, Automation of Correctness Testing of the Software Written in An Imperative Language, Romanian Journal of Information Technology and Automatic Control, ISSN 1220-1758, vol. 6(1), pp. 19-25, 1996.