NewsDevelopersEnterpriseBlockchain ExplainedEvents and ConferencesPressButlletins informatius

Subscriu-te al nostre butlletí.

Correu electrònic

Respectem la vostra privadesa

IniciBlogDesenvolupadors

Abraçant el poder dels mètodes formals en el meu viatge de codificació: com em vaig convertir en un evangelista de Dafny

per ConsenSys, 22 de desembre de 2020 Publicat el 22 de desembre de 2020

A càrrec de Joanne Fuller

Vull començar dient que escric aquesta publicació del bloc amb l’esperança que altres puguin experimentar el moment d’epifania que vaig tenir mentre aprenia Dafny com a part de la meva exploració cap a mètodes formals. A més, espero que aquest post actuï com a catalitzador perquè altres considerin els mètodes formals com una habilitat crítica i necessària dins de l’arsenal de qualsevol que escrigui codi. Com a part del Equip de verificació automatitzada dins de R&D a ConsenSys, Estic fent servir Dafny per a la verificació formal de l’especificació de la fase 0 d’Ethereum 2 i vull compartir per què em sembla útil.

Els meus antecedents

Hauria de deixar clar que no sóc desenvolupador de programari, sinó que em considero un programador matemàtic amb cert coneixement del desenvolupament de programari. Primer vaig aprendre a escriure programes com a part de la meva classe de matemàtiques durant el darrer any de batxillerat i probablement hauria d’esmentar que, tot i que en aquella època em va agradar molt l’ús d’ordinadors, la perspectiva d’aprendre a programar em va espantar fins al punt va deixar aquesta classe de matemàtiques en particular. Després d’haver decidit afrontar la meva por al fracàs (pel que fa a aprendre a programar i potencialment arruïnar el meu resultat en aquesta classe), vaig passar a viure el meu primer moment d’epifania en el context de la programació. Encara puc recordar vivament que m’he assegut a classe i que m’he adonat que escriure un programa per resoldre un problema de matemàtiques no era un procés màgic i misteriós, era gairebé com escriure com treballaria un problema al cap. Després d’això no es va poder mirar enrere! 

La programació ha estat un aspecte important de tot el que he fet des de llavors. El meu doctorat en criptografia depenia en gran mesura de la capacitat per desenvolupar algoritmes i després programar implementacions òptimes. Els meus programes es van escriure per experimentar i, tot i que no em vaig encarregar del que ara faríem referència a proves formals, comprovaria els límits i els casos de prova de manera informal mitjançant un raonament lògic sobre la producció prevista. També vaig treballar durant molts anys com a empresa acadèmica investigadora en el camp de les finances i l’economia. De nou, això incloïa programes d’escriptura i, de nou, vaig utilitzar les meves pròpies tècniques per provar i raonar de manera informal sobre la seva correcció. 

És just dir que, tot i que vaig apreciar el fet que les proves sempre fossin incompletes en el sentit que era impossible provar tots els casos; que tenia una confiança raonable que la meva manera de pensar matemàtica era força bona a l’hora de provar de manera informal de manera rigorosa. Com a tal, definitivament no vaig tenir una plena comprensió de la diferència entre provar i demostrar la seva correcció, ni les conseqüències d’això. Durant la meva carrera professional abans d’incorporar-me a ConsenSys, em conformava amb confiar en les meves pròpies tècniques informals per determinar el que pensava que era correcte mitjançant proves. 

Per tant, el meu bagatge forma part de la història, ja que em sorprèn una mica que no hagi descobert mètodes formals abans. Em considero matemàtic; M’encanten les matemàtiques, els algorismes i la lògica. Ara sembla una bogeria confiar simplement en proves incompletes, però també sembla una bogeria que qualsevol persona que programi no tingui una certa apreciació del que poden oferir els mètodes formals i de les possibles conseqüències de perdre un error donades les múltiples maneres en què es troben els programes d’ordinador. integrat a les nostres vides. Els mètodes formals ens permeten anar més enllà de les proves, per demostrar que un programa és correcte en comparació amb una especificació que inclou condicions de pre i post. 

Un primer exemple de Dafny

Com a exemple simple, considereu la divisió sencera d’un dividend no negatiu per un divisor positiu d; 

n / d

mostrat a continuació:

Tot i que en un llenguatge de programació mecanografiat podem restringir una mica els paràmetres d’entrada, no sempre és suficient. En aquest exemple, l’especificació de n i d com a nombres naturals significa que les dues entrades han de ser enters no negatius, però no preveu la restricció de d a ser un enter positiu. L’ús d’una condició prèvia mitjançant la declaració require preveu aquesta restricció i significa que aquest mètode només es pot cridar si d > 0. Per tant, si alguna altra part del programa provocaria que es cridés div sense que es compleixi aquesta condició prèvia, el programa no es verificarà. A continuació, la declaració assegura proporciona la condició de publicació i proporciona una especificació formal del que ha de satisfer el resultat del mètode.

Aquest exemple està escrit amb Dafny: “Un verificador de llenguatge i de programes per a la correcció funcional” i em porta al meu següent punt, és a dir, per què sóc tan fanàtic de Dafny. Crec que és just dir que per a molts programadors, la idea d’utilitzar “mètodes formals” per verificar la correcció del programa és una mica aterridora i sovint es percep com “massa” dura. Ja sigui per manca d’exposició a les tècniques, per manca d’apreciació dels beneficis o, fins i tot, per falta de formació en aquest àmbit; siguin quines siguin les raons, crec que Dafny té la capacitat de permetre a qualsevol programador aconseguir ràpidament èxit en aplicar mètodes formals en el seu treball. Si mireu el fragment de codi que hi ha més amunt, m’esperaria que qualsevol que tingui coneixements de programació pugui llegir aquest codi de Dafny; Dafny és un llenguatge fàcil de programar. Un cop heu après una mica de Dafny, és molt fàcil començar a experimentar i després bàsicament aprendre a mesura que aneu. I si esteu interessats en aprendre Dafny, és un lloc ideal per començar sèries de tutorials de Microsoft. El lloc també inclou un editor en línia, de manera que és molt fàcil provar els exemples de tutorial. El Canal de YouTube Corner de verificació és una altra font de referències útils.

El meu moment d’epifania

Finalment, volia compartir el meu moment d’epifania de quan aprenia Dafny. Sens dubte, he escoltat històries sobre trossos de codi breus i senzills, de grans empreses de bona reputació, que tenien errors que es van perdre i que finalment costaven molts milions de dòlars; però crec que només quan us adoneu de la facilitat que seria crear sense voler un error en una senzilla funció, tot té sentit. El moment en què et dius “Oh, seria tan fàcil cometre aquest error!”

El meu moment va arribar mentre mirava un dels Vídeos del racó de verificació. 

En aquest tutorial, Rustan Leino passa per un mètode SumMax que pren dos enters, x i y, i retorna la suma i el màxim, s i m, respectivament. Aquest exemple és relativament senzill i el codi Dafny es mostra a continuació.

Les entrades xey s’especifiquen com a enters mitjançant l’escriptura i no es requereixen altres condicions prèvies. Les tres condicions de post proporcionen comprovacions de si la sortida compleix les especificacions, és a dir, que s igual a x + y, i que m és igual a x o y i que m no supera xy. A continuació, el mètode SumMaxBackwards es presenta com un exercici i és aquí on resulta més interessant. L’especificació és el revers de SumMax, és a dir, donada la suma i el màxim retornen els enters x i y. D’acord, per tant, un primer intent podria tenir les mateixes postcondicions; ja que les relacions entre les entrades i les sortides encara es mantenen. Si deixem que x sigui el màxim, llavors una mica d’àlgebra ens diu que y hauria de ser igual a la suma menys el màxim. Posar-ho a l’editor en línia proporciona el següent.

No es verifica. Què va fallar, doncs? Ens diuen que no es mantenia una postcondició i, en concret, la postcondició de la línia 3 (assegura x<= m && y <= m) no pot contenir. Mirant més de prop veiem que aquesta condició de publicació especifica que x <= m i y <= m. Bé, sabem que x és menor o igual a m ja que establim x igual a m, de manera que això significa que la y <= m part no es verifica. Com pot passar això? La nostra àlgebra ens va dir que y: = s – m. Diguem que s és 5 i m és 3, llavors y = 5 – 3 = 2 que assegura y <= m; però diguem que anomenem aquest mètode amb s igual a 5 i m igual a 1. Res no ens impedirà trucar al mètode amb aquests paràmetres d’entrada, però fer-ho provocarà un problema com y = 5 – 1 = 4 i després y > m. Bàsicament el que estem veient aquí és que, tot i que el paràmetre d’entrada ha de ser el màxim de dos enters que crea la suma s, no hi ha res que ens impedeixi intentar trucar al mètode amb una entrada que no sigui vàlida. Tret que s’inclogui una condició prèvia per restringir les entrades de s i m a nombres enters vàlids que donaran lloc a sortides xey que compleixin l’especificació, el nostre mètode pot produir resultats incorrectes. Quina relació necessitem entre s i m per proporcionar entrades vàlides? Una mica més d’àlgebra ens mostra que s <= m * 2 perquè hi hagi una solució vàlida de x i y. Si afegim això com a condició prèvia, Dafny ara pot verificar el codi tal com es mostra a continuació. 

Aquest va ser l’exemple en què vaig poder veure el fàcil que és introduir un error al codi. El fet que anomenem els paràmetres d’entrada “s” per a suma i “m” per a màxim, no vol dir que el mètode es cridi adequadament i, com a tal, com a part d’algun programa més gran, hi podria haver moltes conseqüències no desitjades tipus d’error. Espero que sigui útil per a qualsevol altra persona que conegui Dafny o els mètodes formals de manera més general.

En què estic treballant ara

Doncs això em porta al final de la meva publicació. Si voleu veure en què estic treballant actualment amb Dafny, consulteu això Reposició de GitHub. Formo part de l’equip de verificació automatitzada de R&D a ConsenSys i estem utilitzant Dafny per a la verificació formal de l’especificació Ethereum 2 Phase 0. L’ús de mètodes formals a l’espai blockchain és una nova i interessant àrea d’investigació que ha estat adoptada per ConsenSys i animo a qualsevol persona interessada a aprendre més sobre Eth 2.0 a mirar els recursos disponibles dins del repositori del nostre projecte..

Subscriviu-vos al nostre butlletí per obtenir les últimes novetats, solucions empresarials, recursos per a desenvolupadors i molt més sobre Ethereum.