Corectitudinea programelor

Despre corectitudinea programelor au curs râuri de cerneală şi matematicienii au dezvoltat nenumărate teorii. Spre nefericirea generală, exemplificările au fost făcute cam în toate cazurile pe programe care implementau algoritmul lui EUCLID, deşi programele aflate în uz curent au o cu totul altă dimensiune şi sunt construite cu totul altfel. Au existat încercări de a face automatizarea procesului de demonstrare a corectitudinii, dar mă abţin să fac comentarii pe acest subiect.
Cred că se demonstrează doar corectitudinea parţială prin testarea programului, dacă şi numai dacă, se construiesc baterii de teste cât mai complete, care să activeze toate punctele esenţiale ale programului. Corectitudinea se certifică după derularea unui proces de auditare cât de cât obiectiv, de o echipă care respectă standarde unanim acceptate.