Cunoscutul cercetător olandez Edsger W. Dijkstra a remarcat că "testarea poate demonstra prezenţa erorilor, nu absenţa lor". În fapt singura metodă definitivă de a spune dacă un soft este corect scris, fără erori, este prin matematică. Se cunoaşte că este dificil să scrii cod fără buguri. De când Friedrich L. Bauer a organizat prima conferinţă privind "ingineria software" în 1968, cercetătorii în informatică au creat metodologii pentru a structura şi ghida scrierea de soft.

 



Una dintre aceste metodologii, numite inginerie software tare (eng. strong software engineering) ori, mai uzual, "metode formale", foloseşte matematica pentru a asigura programarea fără erori.

Pe măsură ce economia devine mai computerizată şi mai conectată la Internet, erorile softurilor duc din în ce în ce mai mult la costuri economice.

 





Inginerie software formală


Doi cercetători britanici în domeniul informaticii, Tony Hoare şi Robin Milner, au primit Premiul Turing, echivalentul Premiului Nobel pentru acest domeniu, pentru rezultatele lor în domeniul metodelor formale.

Cercetătorul britanic Cliff B. Jones a fost unul dintre inventatorii Metodei de dezvoltare Viena în timp ce lucra la IBM, în Viena, IBM UK şi Laboratorul de Calcul al Universităţii Oxford, condus de Tony Hoare. Jones a câştigat Premiul Reginei pentru Realizări Tehnologice for rezultatele sale în formalizarea softului CICS al IBM. Pe parcurs acesta a dezvoltat notarea Z, care a devenit una dintre metodele formale principale.

Utilizarea metodei formale începe prin a descrie ce este de aşteptat să facă un program, folosindu-se notaţia logică şi matematică, apoi se folosesc dovezi logice şi matematice pentru a verifica că programul face într-adevăr ceea ce ar trebui să facă. De exemplu, următoarea formulă logică Hoare ce descrie o funcţie a unui program arată cum pot metodele formale să reducă codul la ceva de tipul 1 + 1 = 2.

 

 

Formula logică Hoare: dacă un program S a fost iniţiat într-o stare ce satisface P ne duce către o stare ce satisface Q şi programul T ne duce de la Q la R, apoi făcând S şi apoi T ne duce dela P la R


Predate la majoritatea universităţilor britanice de la mijlocul anilor 1980, metodele formale au fost consistent utilizate în industria sistemelor de securitate critice. Recentele progrese au atins un punct ce permite metodelor formale să verifice cod prin intermediul unor instrumente automate puternice.

Guvernul a priceput mesajul

Profesorul Jim Norton, fost preşedinte al Societăţii Informatice Britanice (British Computer Society), în faţa Comitetului Afacerilor Interne, în aprilie 2013, a explicat: "Avem nevoie de un software mai bun şi ştim să scriem software mult mai bun decât o facem în practică în cele mai multe cazuri. Noi nu folosim metodele matematice formale pe care le avem la dispoziţie de 40 de ani".

Bazându-se pe informaţiile furnizate de Norton, comitetul a scris următoarea recomandare: "softul pentru infrastructura importantă va fi securizată în mod demonstrabil, folosindu-se abordări matematice pentru a scrie cod".

Două luni mai târziu, Comitetul de Ştiinţă şi Tehnologie a colectat date despre programul Digital by Default privind servicii publice furnizate prin intermediul Internetului. Un expert invitat a fost Martyn Thomas, fondatorul companiei Praxis, una dintre firmele de marcă ce folosesc metodele formale pentru dezvoltarea sistemelor de securitate critice. Întrebat cum se poate obţine nivelul cerut de securitate, Thomas a răspuns: "Testarea asiduă nu va asigura nivelul de încredere necesar. Trebuie ca analiza să fie baza. Asta înseamnă că softul trebuie astfel scris încât să poată fi analizat, iar o astfel de abordare înseamnă o schimbare fundamentală pentru industrie".

Prin urmare, condiţiile pentru a scrie software fără erori sunt îndeplinite: există posibilităţi tehnice şi factorii de decizie sunt informaţi asupra problemelor şi soluţiilor. Mai rămâne ca metodele formale să fie implementate în procesul de scriere a codului.

Pentru mai multe detalii privind efectele codului cu erori, în ce constă metodele formale, limbajul Z etc. citiţi această prezentare.

Traducere după Flaw-free-software


Dacă găsiţi scientia.ro util, sprijiniţi-ne cu o donaţie.


PayPal ()
CoinGate Payment ButtonCriptomonedă
Susţine-ne pe Patreon!