NyheterUtviklereEnterpriseBlockchain ExplainedBegivenheter og konferanserPresseNyhetsbrev
Abonner på vårt nyhetsbrev.
Epostadresse
Vi respekterer personvernet ditt
HomeBlogDevelopers
Å omfavne kraften til formelle metoder i min kodingsreise: Hvordan jeg ble en Dafny-evangelist
av ConsenSys 22. desember 2020 Publisert 22. desember 2020
Av Joanne Fuller
Jeg vil begynne med å si at jeg skriver dette blogginnlegget i håp om at andre kan oppleve det åpenbare øyeblikket jeg hadde mens jeg lærte Dafny som en del av utforskningen min formelle metoder. Videre er det mitt håp at dette innlegget vil fungere som en katalysator for andre å betrakte formelle metoder som en kritisk og nødvendig ferdighet i arsenalet til alle som skriver kode. Som en del av Automatisert verifiseringsteam innen R&D hos ConsenSys, Jeg bruker Dafny i den formelle verifiseringen av Ethereum 2 fase 0-spesifikasjonen, og jeg vil dele hvorfor jeg synes det er nyttig.
Min bakgrunn
Jeg bør gjøre det klart at jeg ikke er programvareutvikler, men heller anser meg for å være en matematisk programmerer med litt kunnskap om programvareutvikling. Jeg lærte først å skrive programmer som en del av matematikktimen i løpet av det siste året på videregående skole, og jeg burde sannsynligvis nevne at selv om jeg ganske likte å bruke datamaskiner på den tiden, var muligheten for å lære å programmere skremte meg til det punktet droppet akkurat den matematikkkursen. Etter å ha bestemt meg for å møte frykten for å mislykkes (med hensyn til å lære å programmere og potensielt ødelegge resultatet mitt i denne klassen), fortsatte jeg med å oppleve mitt første epifani-øyeblikk i programmeringssammenheng. Jeg kan fremdeles med glede huske at jeg satt i timen og hadde forståelsen av at det å skrive et program for å løse et matteproblem ikke var noen magisk og mystisk prosess, det var nesten som å skrive ned hvordan jeg ville jobbe gjennom et problem i hodet mitt. Det var ingen å se tilbake etter det!
Programmering har vært et viktig aspekt av alt jeg har gjort siden. Doktorgraden min i kryptografi stolte sterkt på en evne til å utvikle algoritmer og deretter programmere optimale implementeringer. Programmene mine ble skrevet for eksperimentering, og selv om jeg ikke foretok det vi nå ville referere til som formell testing, ville jeg uformelt sjekke grenser og teste saker ved hjelp av logisk resonnement om den tiltenkte utgangen. Jeg jobbet også i mange år som akademisk forskningsfelt innen finans og økonomi. Igjen inkluderte dette skriveprogrammer, og igjen brukte jeg mine egne teknikker for å uformelt teste og resonnere om deres korrekthet.
Det er rettferdig å si at selv om jeg hadde forståelse for at testing alltid ville være ufullstendig i den forstand at det var umulig å teste alle tilfeller; at jeg var rimelig trygg på at min matematiske tankegang var ganske god når det gjaldt uformell testing på en streng måte. Som sådan hadde jeg definitivt ikke full forståelse av forskjellen mellom å teste og bevise korrekthet, og heller ikke konsekvensene av slike! I løpet av karrieren min før jeg begynte i ConsenSys, var jeg fornøyd med å stole på mine egne uformelle teknikker for å bestemme hva jeg trodde var riktig via testing.
Bakgrunnen min er derfor en del av historien, da jeg selv er litt overrasket over at jeg ikke oppdaget formelle metoder tidligere. Jeg anser meg selv som en matematiker; Jeg elsker matte, algoritmer og logikk. Det virker nå sprøtt å bare stole på ufullstendig testing, men det virker også sprøtt for alle som programmer ikke minst har noen forståelse for hva formelle metoder kan tilby og de potensielle konsekvensene av å savne en feil gitt de mange måtene som dataprogrammer er integrert i livene våre. Formelle metoder tillater oss å gå utover testing, for å bevise at et program stemmer med en spesifikasjon som inkluderer forhold før og etter.
Et første Dafny-eksempel
Som et enkelt eksempel kan du vurdere heltalsdeling av et ikke-negativt utbytte n med en positiv divisor d;
n / d
Vist under:
Selv om vi i et tastet programmeringsspråk kan begrense inngangsparametrene noe, er det ikke alltid tilstrekkelig. I dette eksemplet betyr spesifikasjonen av n og d som naturlige tall at begge inngangene må være ikke-negative heltall, men det gir ikke begrensning av d til å være et positivt heltall. Bruken av en forutsetning i form av krav-uttalelsen gir en slik begrensning og betyr at denne metoden bare kan kalles hvis d > 0. Derfor, hvis noen andre deler av programmet vil føre til at div blir kalt uten at en slik forutsetning er oppfylt, vil ikke programmet bekrefte. Sikrer erklæringen gir deretter innleggsbetingelsen og gir en formell spesifikasjon av hva metodeutgangen må tilfredsstille.
Dette eksemplet er skrevet ved hjelp av Dafny: “A language and program verifier for functionalness correctness” og bringer meg til mitt neste punkt, det er hvorfor jeg er en så fan av Dafny. Jeg synes det er greit å si at tanken på å bruke “formelle metoder” for å verifisere programkorrektheten for mange programmerere er noe skummel og ofte oppleves som “for” vanskelig. Enten dette er på grunn av mangel på eksponering for teknikkene, manglende forståelse av fordelene, eller til og med mangel på trening på dette området; Uansett årsakene, tror jeg at Dafny har evnen til å tillate programmerere å raskt oppnå suksess med å anvende formelle metoder i sitt arbeid. Ser jeg på kodebiten ovenfor, forventer jeg at alle med litt programmeringskunnskap kan lese denne Dafny-koden; Dafny er veldig mye et programmeringsvennlig språk. Når du først har lært litt av Dafny, er det veldig enkelt å begynne å eksperimentere og deretter i grunn lære når du går. Og hvis du er interessert i å lære Dafny, er et flott sted å starte opplæringsserie av Microsoft. Nettstedet inneholder også en online editor, så det er veldig enkelt å prøve ut veiledningseksemplene. De Verification Corner YouTube-kanal er en annen kilde til nyttige referanser.
Mitt epifanie øyeblikk
Til slutt ønsket jeg å dele mitt epifani-øyeblikk fra da jeg lærte Dafny. Jeg har absolutt hørt historier om korte og enkle koder, fra store anerkjente selskaper, som har bugs som ble savnet og til slutt kostet mange millioner dollar; men jeg tror det er først når du skjønner hvor lett det ville være å utilsiktet lage en feil i en enkel funksjon at det hele gir mening! Øyeblikket når du sier til deg selv “Å, det ville være så lett å gjøre den feilen!”
Øyeblikket mitt kom mens jeg så på et av Verification Corner videoer.
I denne opplæringen går Rustan Leino gjennom en SumMax-metode som tar to heltall, x og y, og returnerer henholdsvis summen og max, s og m. Dette eksemplet er relativt greit, og Dafny-koden er vist nedenfor.
Inngangene x og y er spesifisert som heltall gjennom å skrive, og det kreves ingen andre forutsetninger. De tre postbetingelsene gir kontroller om at utdataene faktisk oppfyller spesifikasjonene, nemlig at s gjør lik x + y, og at m er lik enten x eller y og at m ikke overstiger x og y. SumMaxBackwards-metoden presenteres deretter som en øvelse, og det er her den blir mer interessant. Spesifikasjonen er det motsatte av SumMax, dvs. gitt summen og maksimal retur heltallene x og y. Ok, så et første forsøk kan være med de samme postforholdene; ettersom forholdet mellom innganger og utganger fortsatt holder. Hvis vi lar x være maksimumet, forteller en rask bit av algebra oss at y skal være lik summen minus maksimumet. Å sette dette inn i online-redaktøren gir følgende.
Det bekrefter ikke. Så hva gikk galt? Vi blir fortalt at en posttilstand ikke holdt, og spesielt posttilstanden på linje 3 (sikrer x<= m && y <= m) holder kanskje ikke. Når vi ser nærmere på, ser vi at denne posttilstanden spesifiserer at x <= m og y <= m. Vel, vi vet at x er mindre enn eller lik m når vi setter x lik m, så dette betyr at y <= m del bekrefter ikke. Hvordan kan dette skje? Vår algebra fortalte oss at y: = s – m. La oss si at s er 5 og m er 3, så y = 5 – 3 = 2 som sikrer y <= m; men la oss si at vi kaller denne metoden med s lik 5 og m lik 1. Ingenting vil hindre oss i å kalle metoden med disse inngangsparametrene, men å gjøre det vil forårsake et problem som y = 5 – 1 = 4 og deretter y > m. I utgangspunktet det vi ser her er at selv om inngangsparameteren er ment å være maksimalt to heltall som skaper summen, er det ikke noe som hindrer oss i å prøve å kalle metoden med en inngang som ikke er gyldig. Med mindre en forutsetning er inkludert for å begrense inngangene til s og m til gyldige heltall som vil resultere i utganger x og y som oppfyller spesifikasjonen, kan metoden vår gi feil resultater. Hvilket forhold trenger vi mellom s og m for å gi gyldige innganger? Litt mer algebra viser oss at s <= m * 2 for at det skal være en gyldig løsning av x og y. Hvis vi legger til dette som en forutsetning, kan Dafny nå bekrefte koden som vist nedenfor.
Dette var eksemplet der jeg kunne se hvor enkelt det er å introdusere en feil i koden. Bare fordi vi kaller inngangsparametrene ‘s’ for sum og ‘m’ for maksimum, betyr ikke det at metoden vil bli kalt riktig og som sådan som en del av et større program, kan det være mange utilsiktede konsekvenser som følger av dette type feil. Jeg håper det er nyttig for alle andre som lærer om Dafny eller formelle metoder mer generelt.
Det jeg jobber med nå
Vel, det fører meg til slutten av innlegget mitt. Hvis du vil se hva jeg jobber med Dafny for øyeblikket, så sjekk ut dette GitHub repo. Jeg er en del av det automatiserte verifiseringsteamet innen R&D hos ConsenSys, og vi bruker Dafny i den formelle verifiseringen av Ethereum 2 fase 0-spesifikasjonen. Bruken av formelle metoder i blockchain-rommet er et spennende nytt forskningsområde som har blitt omfavnet av ConsenSys, og jeg vil oppmuntre alle som er interessert i å lære mer om Eth 2.0 for å se på ressursene som er tilgjengelige i vårt prosjektrapport.
Abonner på vårt nyhetsbrev for de siste Ethereum-nyhetene, bedriftsløsninger, utviklerressurser og mer.
