blogul 1NewsDevelopersEnterpriseBlockchain Explained Evenimente și conferințe ApăsațiBuletine informative

Aboneaza-te la newsletter-ul nostru.

Adresa de email

Vă respectăm confidențialitatea

AcasăBlogDezvoltatori

Îmbrățișând puterea metodelor formale în călătoria mea de codificare: Cum am devenit evanghelist Dafny

de ConsenSys 22 decembrie 2020 Postat pe 22 decembrie 2020

Captură de ecran 2020 12 15 la 6 46 32 pm 1

De Joanne Fuller

Vreau să încep prin a spune că scriu această postare pe blog în speranța că alții pot experimenta momentul de epifanie pe care l-am avut în timp ce învățam Dafny ca parte a explorării mele în metode formale. Mai mult, sper că acest post va acționa ca un catalizator pentru ca alții să considere metodele formale ca o abilitate critică și necesară în cadrul arsenalului oricui scrie cod. Ca parte a Echipa de verificare automată din cadrul R&D la ConsenSys, Folosesc Dafny în verificarea formală a specificației Ethereum 2 Faza 0 și vreau să vă spun de ce mi se pare util.

Trecutul meu

Ar trebui să precizez că nu sunt dezvoltator de software, ci mai degrabă mă consider un programator matematic cu o anumită cunoaștere a dezvoltării de software. Am învățat mai întâi să scriu programe ca parte a clasei de matematică în ultimul an de liceu și probabil ar trebui să menționez că, deși îmi plăcea destul de mult să folosesc computerele în acel moment, perspectiva de a învăța cum să programez m-a speriat până la punctul în care aproape a renunțat la cursul de matematică. După ce am decis să mă confrunt cu teama mea de eșec (în ceea ce privește învățarea de a programa și potențialul de a-mi distruge rezultatul în această clasă), am continuat să experimentez primul meu moment de epifanie în contextul programării. Încă îmi amintesc clar că am stat la curs și am realizat că scrierea unui program pentru rezolvarea unei probleme de matematică nu era un proces magic și misterios, era aproape ca să scriu cum aș rezolva o problemă din capul meu. După aceea, nu mai era nici o privire înapoi! 

Programarea a fost un aspect important al tot ceea ce am făcut de atunci. Doctoratul meu în criptografie s-a bazat în mare măsură pe abilitatea de a dezvolta algoritmi și apoi de a programa implementări optime. Programele mele au fost scrise pentru experimentare și, deși nu m-am angajat la ceea ce vom numi acum ca testare formală, aș verifica informal limitele și a testa cazurile folosind raționamente logice despre rezultatul dorit. De asemenea, am lucrat mulți ani ca cercetare în domeniul financiar și economic. Din nou, acest lucru a inclus programe de scriere și, din nou, mi-am folosit propriile tehnici pentru a testa informal și a raționa despre corectitudinea lor. 

Este corect să spun că, deși am apreciat faptul că testarea ar fi întotdeauna incompletă în sensul că a fost imposibil să testez fiecare caz; că eram destul de încrezător că modul meu de gândire matematic era destul de bun atunci când venea să testez informal într-o manieră riguroasă. Ca atare, cu siguranță nu am avut o apreciere deplină a diferenței dintre testare și dovedirea corectitudinii și nici consecințele acestora! În timpul carierei mele înainte de a mă alătura ConsenSys, m-am mulțumit să mă bazez pe propriile mele tehnici informale pentru a determina ceea ce credeam că este corectitudinea prin testare. 

Prin urmare, fundalul meu face parte din poveste, întrucât sunt oarecum surprins că nu am descoperit metodele formale mai devreme. Mă consider un matematician; Ador matematica, algoritmii și logica. Acum pare o nebunie să te bazezi pur și simplu pe teste incomplete, dar, de asemenea, pare o nebunie pentru oricine programează să nu aibă măcar o oarecare apreciere a ceea ce pot oferi metodele formale și consecințele potențiale ale lipsei unei erori, având în vedere numeroasele moduri în care sunt programele de calculator. integrat în viețile noastre. Metodele formale ne permit să mergem dincolo de testare, pentru a demonstra că un program este corect în raport cu o specificație care include condiții pre și post. 

Un prim exemplu Dafny

Ca un exemplu simplu, considerați divizarea întreagă a unui dividend n-negativ n cu un divizor pozitiv d; 

n / d

prezentat mai jos:

Deși într-un limbaj de programare tastat putem restricționa oarecum parametrii de intrare, nu este întotdeauna suficient. În acest exemplu, specificația lui n și d ca numere naturale înseamnă că ambele intrări trebuie să fie numere întregi non-negative, dar nu prevede restricția lui d pentru a fi un număr întreg pozitiv. Utilizarea unei condiții prealabile prin declarația require prevede o astfel de restricție și înseamnă că această metodă poate fi apelată numai dacă d > 0. Prin urmare, dacă orice altă parte a programului ar determina apelarea divului fără ca o astfel de condiție prealabilă să fie îndeplinită, atunci programul nu va verifica. Declarația de asigurare oferă apoi condiția post și oferă o specificație formală a ceea ce trebuie să satisfacă rezultatul metodei.

Acest exemplu este scris folosind Dafny: „Un limbaj și un program de verificare pentru corectitudinea funcțională” și mă aduce la următorul meu punct, adică de ce sunt un astfel de fan al lui Dafny. Cred că este corect să spunem că pentru mulți programatori, gândul de a folosi „metode formale” pentru a verifica corectitudinea programului este oarecum înfricoșător și este adesea perceput ca fiind „prea” greu. Fie că acest lucru se datorează lipsei expunerii la tehnici, lipsei de apreciere a beneficiilor sau chiar lipsei de instruire în acest domeniu; oricare ar fi motivele, cred că Dafny are capacitatea de a permite oricărui programator să obțină rapid succes în aplicarea metodelor formale în munca lor. Privind fragmentul de cod de mai sus, m-aș aștepta ca oricine are unele cunoștințe de programare să poată citi acest cod Dafny; Dafny este foarte mult un limbaj prietenos cu programatorii. Odată ce ați învățat puțin din Dafny, este foarte ușor să începeți experimentarea și apoi să învățați în timp ce mergeți. Și dacă sunteți interesat să învățați Dafny, un loc minunat pentru a începe este serie de tutoriale de către Microsoft. Site-ul include și un editor online, deci este foarte ușor să încercați exemplele de tutoriale. Canalul YouTube de pe colțul de verificare este o altă sursă de referințe utile.

Momentul meu de epifanie

În cele din urmă, am vrut să împărtășesc momentul meu de epifanie de când învățam Dafny. Cu siguranță am auzit povești despre bucăți de cod scurte și simple, de la companii mari cu reputație, având bug-uri care au fost ratate și au costat în cele din urmă multe milioane de dolari; dar cred că doar atunci când îți dai seama cât de ușor ar fi să creezi în mod neintenționat un bug într-o funcție simplă, totul are sens! Momentul în care îți spui „Oh, ar fi atât de ușor să greșești!”

Momentul meu a venit în timp ce mă uitam la unul dintre Videoclipuri din colțul de verificare

În acest tutorial Rustan Leino trece printr-o metodă SumMax care ia două numere întregi, x și y, și returnează suma și max, s și respectiv m. Acest exemplu este relativ simplu, iar codul Dafny este prezentat mai jos.

Intrările x și y sunt specificate ca numere întregi prin tastare și nu sunt necesare alte condiții prealabile. Cele trei condiții de post asigură verificarea faptului că rezultatul îndeplinește într-adevăr specificațiile, și anume că s este egal cu x + y și că m este egal fie cu x, fie cu y și că m nu depășește x și y. Metoda SumMaxBackwards este apoi prezentată ca un exercițiu și aici devine mai interesant. Specificația este inversa SumMax, adică având în vedere suma și maximul returnează numerele întregi x și y. Ok, deci o primă încercare ar putea fi cu aceleași condiții postale; întrucât relațiile dintre intrări și ieșiri se păstrează încă. Dacă lăsăm x să fie maxim, atunci un bit rapid de algebră ne spune că y ar trebui să fie egală cu suma minus maximul. Punerea acestui lucru în editorul online oferă următoarele.

Captură de ecran 2020 12 15 la 6 38 37 pm 1 Screen Shot 2020 12 16 la 5 35 22 pm

Nu se verifică. Deci, ce a mers prost? Ni se spune că o condiție postală nu a deținut și în mod specific condiția postală de pe linia 3 (asigură x<= m && y <= m) nu poate ține. Privind mai atent vedem că această condiție de postare specifică că x <= m și y <= m. Ei bine, știm că x este mai mic sau egal cu m, așa cum stabilim x egal cu m, deci asta înseamnă că y <= m partea nu se verifică. Cum se poate întâmpla asta? Algebra noastră ne-a spus că y: = s – m. Să presupunem că s este 5 și m este 3, apoi y = 5 – 3 = 2 care asigură y <= m; dar să presupunem că numim această metodă cu s egal cu 5 și m egal cu 1. Nimic nu ne va împiedica să apelăm metoda cu acești parametri de intrare, dar să facem acest lucru va cauza o problemă ca y = 5 – 1 = 4 și apoi y > m. Practic, ceea ce vedem aici este că, deși parametrul de intrare este menit să fie maximul a două numere întregi care creează suma s, nu există nimic care să ne împiedice să încercăm să apelăm metoda cu o intrare care nu este validă. Dacă nu este inclusă o condiție prealabilă pentru a restricționa intrările lui s și m la numere întregi valide care vor avea ca rezultat ieșiri x și y care îndeplinesc specificațiile, atunci metoda noastră poate produce rezultate incorecte. De ce relație avem nevoie între s și m pentru a furniza intrări valide? Un pic mai mult algebră ne arată că s <= m * 2 pentru a exista o soluție validă pentru x și y. Dacă adăugăm aceasta ca o condiție prealabilă, Dafny este acum capabil să verifice codul așa cum se arată mai jos. 

Captură de ecran 2020 12 15 la 6 46 32 pm 1 Screen Shot 2020 12 16 la 5 37 39 pm

Acesta a fost exemplul în care am putut vedea cât de ușor este să introduc un bug în cod. Doar pentru că numim parametrii de intrare „s” pentru sumă și „m” pentru maxim, nu înseamnă că metoda va fi apelată în mod corespunzător și, ca atare, ca parte a unui program mai mare, ar putea exista multe consecințe neintenționate care decurg din aceasta tip de bug. Sper că este util pentru oricine altcineva care învață despre Dafny sau metodele formale mai general.

La ce lucrez acum

Ei bine, asta mă duce la sfârșitul postării mele. Dacă doriți să vedeți la ce lucrez în prezent cu Dafny, verificați acest lucru Repo GitHub. Fac parte din echipa de verificare automată din cadrul R&D la ConsenSys și îl folosim pe Dafny în verificarea formală a specificației Ethereum 2 Faza 0. Utilizarea metodelor formale în spațiul blockchain este un nou domeniu interesant de cercetare care a fost acceptat de ConsenSys și aș încuraja pe oricine este interesat să afle mai multe despre Eth 2.0 să analizeze resursele disponibile în cadrul repo al proiectului nostru.

Newsletter Abonați-vă la newsletter-ul nostru pentru cele mai recente știri Ethereum, soluții pentru întreprinderi, resurse pentru dezvoltatori și multe altele.

Mike Owergreen Administrator
Sorry! The Author has not filled his profile.
follow me