De kracht van formele methoden omarmen tijdens mijn coderingstraject: hoe ik een Dafny-evangelist werd

blog 1NieuwsOntwikkelaarsEnterpriseBlockchain ExplainedEvenementen en conferentiesPersNieuwsbrieven

Abonneer op onze nieuwsbrief.

E-mailadres

Wij respecteren uw privacy

HomeBlogOntwikkelaars

De kracht van formele methoden omarmen tijdens mijn coderingstraject: hoe ik een Dafny-evangelist werd

door ConsenSys 22 december 2020 Geplaatst op 22 december 2020

Schermopname 2020 12 15 om 6 46 32 uur 1

Door Joanne Fuller

Ik wil beginnen met te zeggen dat ik deze blogpost aan het schrijven ben in de hoop dat anderen het openbaringmoment kunnen ervaren dat ik had tijdens het leren Dafny als onderdeel van mijn verkenning van formele methoden. Verder hoop ik dat dit bericht als katalysator zal werken voor anderen om formele methoden te beschouwen als een kritische en noodzakelijke vaardigheid binnen het arsenaal van iedereen die code schrijft. Als onderdeel van Geautomatiseerd verificatieteam binnen R&D bij ConsenSys, Ik gebruik Dafny bij de formele verificatie van de Ethereum 2 Phase 0-specificatie en ik wil delen waarom ik het nuttig vind.

Mijn achtergrond

Ik moet duidelijk maken dat ik geen softwareontwikkelaar ben, maar dat ik mezelf beschouw als een wiskundige programmeur met enige kennis van softwareontwikkeling. Ik leerde voor het eerst programma’s schrijven als onderdeel van mijn wiskundelessen tijdens mijn laatste jaar van de middelbare school en ik moet waarschijnlijk vermelden dat hoewel ik in die tijd heel graag computers gebruikte, het vooruitzicht om te leren programmeren me zo bang maakte dat ik bijna heeft die specifieke wiskundeles laten vallen. Nadat ik had besloten mijn faalangst onder ogen te zien (met betrekking tot het leren programmeren en mogelijk mijn resultaat in deze klas verpesten), beleefde ik mijn eerste openbaringmoment in de context van programmeren. Ik kan me nog levendig herinneren dat ik in de klas zat en het besef had dat het schrijven van een programma om een ​​wiskundig probleem op te lossen geen magisch en mysterieus proces was, het was bijna alsof ik opschreef hoe ik een probleem in mijn hoofd zou oplossen. Daarna was er geen weg terug! 

Programmeren is een belangrijk aspect geweest van alles wat ik sindsdien heb gedaan. Mijn doctoraat in cryptografie was sterk afhankelijk van het vermogen om algoritmen te ontwikkelen en vervolgens optimale implementaties te programmeren. Mijn programma’s zijn geschreven om mee te experimenteren en hoewel ik niet deed wat we nu formeel testen zouden noemen, controleerde ik informeel de grenzen en testte ik gevallen door logisch te redeneren over de beoogde output. Ik heb ook vele jaren gewerkt als een academische onderneming die onderzoek deed op het gebied van financiën en economie. Wederom omvatte dit het schrijven van programma’s, en opnieuw gebruikte ik mijn eigen technieken om informeel hun correctheid te testen en erover te redeneren. 

Het is eerlijk om te zeggen dat, hoewel ik waardering had voor het feit dat testen altijd onvolledig zouden zijn in de zin dat het onmogelijk was om elk geval te testen; dat ik er redelijk zeker van was dat mijn wiskundige manier van denken behoorlijk goed was als het ging om informeel testen op een rigoureuze manier. Als zodanig had ik absoluut geen volledige waardering voor het verschil tussen testen en correctheid bewijzen, noch de gevolgen daarvan! Tijdens mijn carrière voordat ik bij ConsenSys kwam, was ik tevreden om te vertrouwen op mijn eigen informele technieken om te bepalen wat ik dacht dat juistheid was door middel van testen. 

Mijn achtergrond maakt dan ook deel uit van het verhaal, aangezien ik zelf enigszins verbaasd ben dat ik niet eerder formele methoden ontdekte. Ik beschouw mezelf als een wiskundige; Ik hou van wiskunde, algoritmen en logica. Het lijkt nu gek om gewoon te vertrouwen op onvolledige tests, maar het lijkt ook gek voor iedereen die programmeert om niet op zijn minst enige waardering te hebben voor wat formele methoden kunnen bieden en de mogelijke gevolgen van het missen van een bug, gezien de vele manieren waarop computerprogramma’s worden gebruikt. geïntegreerd in ons leven. Formele methoden stellen ons in staat om verder te gaan dan testen, om te bewijzen dat een programma correct is tegen een specificatie die pre- en postcondities bevat. 

Een eerste Dafny-voorbeeld

Beschouw als een eenvoudig voorbeeld de integer deling van een niet-negatief dividend n door een positieve deler d; 


n / d

hieronder weergegeven:

Hoewel we in een getypte programmeertaal de invoerparameters enigszins kunnen beperken, is dit niet altijd voldoende. In dit voorbeeld betekent de specificatie van n en d als natuurlijke getallen dat beide invoer niet-negatieve gehele getallen moeten zijn, maar het voorziet niet in de beperking van d tot een positief geheel getal. Het gebruik van een randvoorwaarde door middel van de requirements statement voorziet in een dergelijke beperking en betekent dat deze methode alleen kan worden aangeroepen als d > 0. Dus als enig ander deel van het programma ervoor zou zorgen dat div wordt aangeroepen zonder dat aan een dergelijke voorwaarde is voldaan, zal het programma niet verifiëren. De assurance-instructie geeft vervolgens de postconditie en geeft een formele specificatie van waaraan de uitvoer van de methode moet voldoen.

Dit voorbeeld is geschreven met Dafny: “Een taal- en programmaverificateur voor functionele correctheid” en brengt me bij mijn volgende punt, dat is waarom ik zo’n fan ben van Dafny. Ik denk dat het eerlijk is om te zeggen dat voor veel programmeurs de gedachte om “formele methoden” te gebruiken om de juistheid van programma’s te verifiëren, enigszins beangstigend is en vaak als “te” moeilijk wordt ervaren. Of dit komt door een gebrek aan kennis van de technieken, een gebrek aan waardering voor de voordelen of zelfs een gebrek aan opleiding op dit gebied; wat de redenen ook mogen zijn, ik geloof dat Dafny het vermogen heeft om programmeurs in staat te stellen snel succes te boeken bij het toepassen van formele methoden in hun werk. Als ik naar het bovenstaande codefragment kijk, zou ik verwachten dat iemand met enige programmeerkennis deze Dafny-code kan lezen; Dafny is een programmeervriendelijke taal. Als je eenmaal een klein beetje Dafny hebt geleerd, is het heel gemakkelijk om te beginnen met experimenteren en dan in principe te leren terwijl je bezig bent. En als je geïnteresseerd bent in het leren van Dafny, dan is een geweldige plek om te beginnen de tutorial serie door Microsoft. De site bevat ook een online editor, dus het is heel gemakkelijk om de tutorialvoorbeelden uit te proberen. De Verificatiehoek YouTube-kanaal is een andere bron van nuttige referenties.

Mijn openbaring moment

Eindelijk wilde ik mijn openbaring moment delen vanaf het moment dat ik Dafny leerde. Ik heb zeker verhalen gehoord over korte en eenvoudige stukjes code, van grote gerenommeerde bedrijven, met bugs die werden gemist en die uiteindelijk vele miljoenen dollars kosten; maar ik denk dat het pas logisch is als je je realiseert hoe gemakkelijk het zou zijn om per ongeluk een bug te creëren in een eenvoudige functie! Het moment waarop je tegen jezelf zegt: “Oh, het zou zo gemakkelijk zijn om die fout te maken!”

Mijn moment kwam toen ik naar een van de Verificatiehoekvideo’s

In deze tutorial doorloopt Rustan Leino een SumMax-methode die twee gehele getallen nodig heeft, x en y, en die respectievelijk de som en max, s en m retourneert. Dit voorbeeld is relatief eenvoudig en de Dafny-code wordt hieronder weergegeven.

De invoer x en y worden door middel van typen gespecificeerd als gehele getallen en er zijn geen andere voorwaarden vereist. De drie postvoorwaarden zorgen ervoor dat de uitvoer inderdaad voldoet aan de specificaties, namelijk dat s gelijk is aan x + y, en dat m gelijk is aan x of y en dat m niet groter is dan x en y. De SumMaxBackwards-methode wordt dan gepresenteerd als een oefening en dit is waar het interessanter wordt. De specificatie is het omgekeerde van SumMax, d.w.z. gegeven de som en het maximale rendement de gehele getallen x en y. Oké, dus een eerste poging zou kunnen zijn met dezelfde postcondities; aangezien de relaties tussen de inputs en outputs nog steeds bestaan. Als we x het maximum laten zijn, vertelt een snel stukje algebra ons dat y gelijk moet zijn aan de som min het maximum. Als u dit in de online editor plaatst, krijgt u het volgende.

Schermopname 2020 12 15 om 6 38 37 uur 1 Screen Shot 2020 12 16 om 5 35 22 uur

Het verifieert niet. Dus wat ging er mis? Er wordt ons verteld dat een postconditie niet klopte en met name de postconditie op regel 3 (verzekert x<= m && y <= m) mag niet gelden. Als we beter kijken, zien we dat deze postvoorwaarde specificeert dat x <= m en y <= m. We weten dat x kleiner is dan of gelijk is aan m omdat we x gelijk stellen aan m, dus dit betekent dat de y <= m deel verifieert niet. Hoe kan dit gebeuren? Onze algebra vertelde ons dat y: = s – m. Laten we zeggen dat s 5 is en m 3, dan is y = 5 – 3 = 2 wat y garandeert <= m; maar laten we zeggen dat we deze methode aanroepen met s gelijk aan 5 en m gelijk aan 1. Niets zal ons ervan weerhouden de methode aan te roepen met deze invoerparameters, maar dit zal een probleem veroorzaken aangezien y = 5 – 1 = 4 en dan y > m. Wat we hier in feite zien, is dat, hoewel de invoerparameter bedoeld is als het maximum van twee gehele getallen die de som s maken, niets ons ervan weerhoudt om de methode aan te roepen met een invoer die niet geldig is. Tenzij een voorwaarde is opgenomen om de invoer van s en m te beperken tot geldige gehele getallen die resulteren in uitvoer x en y die voldoen aan de specificatie, kan onze methode onjuiste resultaten opleveren. Welke relatie hebben we nodig tussen s en m om geldige invoer te leveren? Een beetje meer algebra toont ons dat s <= m * 2 voor een geldige oplossing van x en y. Als we dit als voorwaarde toevoegen, kan Dafny nu de code verifiëren zoals hieronder weergegeven. 

Schermopname 2020 12 15 om 6 46 32 uur 1 Screen Shot 2020 12 16 om 5 37 39 uur

Dit was het voorbeeld waarin ik kon zien hoe gemakkelijk het is om een ​​bug in de code te introduceren. Alleen omdat we de invoerparameters ‘s’ voor som en ‘m’ voor maximum noemen, wil dat nog niet zeggen dat de methode op de juiste manier wordt aangeroepen en als onderdeel van een groter programma, er kunnen veel onbedoelde gevolgen zijn die hieruit voortvloeien. type bug. Ik hoop dat het nuttig is voor iemand anders die meer in het algemeen over Dafny of formele methoden leert.

Waar ik nu aan werk

Nou, dat brengt me aan het einde van mijn post. Als je wilt zien waar ik momenteel met Dafny aan werk, kijk dan hier GitHub-opslagplaats. Ik maak deel uit van het Automated Verification Team binnen R&D bij ConsenSys en we gebruiken Dafny bij de formele verificatie van de Ethereum 2 Phase 0-specificatie. Het gebruik van formele methoden in de blockchain-ruimte is een opwindend nieuw onderzoeksgebied dat is omarmd door ConsenSys en ik zou iedereen die geïnteresseerd is om meer te weten te komen over Eth 2.0 willen aanmoedigen om te kijken naar de beschikbare bronnen binnen onze projectrepository..

Abonneer u op onze nieuwsbrief voor het laatste Ethereum-nieuws, bedrijfsoplossingen, bronnen voor ontwikkelaars en meer

Mike Owergreen Administrator
Sorry! The Author has not filled his profile.
follow me
Like this post? Please share to your friends:
Adblock
detector
map