Prihvaćanje moći formalnih metoda u svom putovanju sa kodiranjem: Kako sam postala evanđelistica Dafny

blog 1NewsDevelopersEnterpriseBlockchain ObjašnjeniDogađaji i konferencijePressBilteni

Pretplatite se na naše obavijesti.

Email adresa

Poštujemo vašu privatnost

HomeBlogDevelopers

Prihvaćanje moći formalnih metoda u svom putovanju sa kodiranjem: Kako sam postala evanđelistica Dafny

od ConsenSys, 22. prosinca 2020. Objavljeno 22. prosinca 2020

Snimka zaslona 2020. 12. 15 u 6 46 32 sati 1

Napisala Joanne Fuller

Želim započeti rekavši da pišem ovaj post na blogu u nadi da će drugi moći doživjeti trenutak bogojavljenja koji sam imao dok sam učio Dafny kao dio mog istraživanja formalne metode. Nadam se, nadam se da će ovaj post djelovati kao katalizator za druge da formalne metode smatraju kritičnom i potrebnom vještinom u arsenalu svakoga tko piše kod. Kao dio Automatizirani tim za provjeru unutar R&D na ConsenSys, Koristim Dafny u formalnoj provjeri specifikacije Ethereum 2 Phase 0 i želim podijeliti zašto ga smatram korisnim.

Moja pozadina

Morao bih jasno reći da nisam programer, već se smatram matematičkim programerom s određenim znanjem o razvoju softvera. Prvi sam put naučio pisati programe u sklopu predavanja iz matematike tijekom završne godine srednje škole i vjerojatno bih trebao spomenuti da, iako sam u to vrijeme prilično volio koristiti računala, mogućnost učenja programiranja uplašila me do te mjere da sam gotovo napustio taj čas matematike. Odlučivši se suočiti sa svojim strahom od neuspjeha (s obzirom na učenje programiranja i potencijalno uništavanje mog rezultata u ovoj klasi), nastavio sam proživljavati svoj prvi trenutak epifanije u kontekstu programiranja. Još se uvijek mogu živo sjetiti kako sam sjedio na nastavi i shvatio da pisanje programa za rješavanje matematičkog problema nije bio neki čaroban i tajanstven proces, bilo je gotovo kao da zapisujem kako ću riješiti problem u svojoj glavi. Nakon toga nije bilo osvrtanja! 

Programiranje je važan aspekt svega što sam od tada radio. Moj doktorat iz kriptografije uvelike se oslanjao na sposobnost razvijanja algoritama i zatim programiranja optimalnih implementacija. Moji su programi napisani za eksperimentiranje i, iako nisam poduzimao ono što bismo sada nazivali formalnim testiranjem, neformalno bih provjeravao granice i slučajeve testiranja koristeći logično rezoniranje o željenom rezultatu. Dugo sam godina radio i kao akademski istraživač na polju financija i ekonomije. To je opet uključivalo programe pisanja i opet sam koristio vlastite tehnike za neformalno testiranje i obrazloženje njihove ispravnosti. 

Pošteno je reći da, iako sam cijenio činjenicu da će testiranje uvijek biti nepotpuno u smislu da je nemoguće testirati svaki slučaj; da sam bio prilično uvjeren da je moj matematički način razmišljanja bio prilično dobar kada je riječ o neformalnom testiranju na rigorozan način. Kao takav definitivno nisam u potpunosti uvidio razliku između testiranja i dokazivanja ispravnosti, kao ni posljedice takvih! Tijekom svoje karijere prije pridruživanja ConsenSysu zadovoljio sam se oslanjanjem na vlastite neformalne tehnike za određivanje ispravnosti onoga što sam smatrao testiranjem. 

Moje je porijeklo stoga dio priče, jer sam i sam pomalo iznenađen što ranije nisam otkrio formalne metode. Smatram se matematičarem; Volim matematiku, algoritme i logiku. Sada se čini suludo jednostavno oslanjati se na nepotpuno testiranje, ali također izgleda ludo za svakoga tko programira da barem ne shvati što formalne metode mogu ponuditi i potencijalne posljedice propuštanja programske pogreške s obzirom na mnoge načine na koje su računalni programi integrirani u naš život. Formalne metode omogućuju nam da idemo dalje od testiranja, kako bismo dokazali da je program točan u odnosu na specifikaciju koja uključuje uvjete prije i poslije. 

Prvi primjer Dafnyja

Kao jednostavan primjer razmotrimo cjelobrojnu podjelu nenegativne dividende n pozitivnim djeliteljem d; 


n / d

prikazano ispod:

Iako u tipiziranom programskom jeziku možemo donekle ograničiti ulazne parametre, to nije uvijek dovoljno. U ovom primjeru specifikacija n i d kao prirodnih brojeva znači da oba ulaza moraju biti negativne cijele brojeve, ali ne predviđa ograničenje d na pozitivan cijeli broj. Korištenje preduvjeta putem naredbe require predviđa takvo ograničenje i znači da se ova metoda može nazvati samo ako je d > 0. Stoga, ako bi bilo koji drugi dio programa uzrokovao pozivanje div-a bez da je ispunjen takav preduvjet, program neće provjeriti. Izjava osiguranja tada pruža uvjet postovanja i daje formalnu specifikaciju onoga što izlaz metode mora zadovoljiti.

Ovaj primjer napisan je pomoću Dafnyja: “Provjerivač jezika i programa za funkcionalnu ispravnost” i dovodi me do moje sljedeće točke, odnosno zašto sam toliko ljubitelj Dafnyja. Mislim da je pošteno reći da je za mnoge programere pomisao na korištenje “formalnih metoda” za provjeru ispravnosti programa pomalo zastrašujuća i često se smatra “previše” teškom. Je li to zbog nedostatka izloženosti tehnikama, nedostatka uvažavanja prednosti ili čak nedostatka obuke u ovom području; bez obzira na razloge, vjerujem da Dafny može omogućiti programerima da brzo postignu uspjeh u primjeni formalnih metoda u svom radu. Gledajući gornji isječak koda, očekivao bih da će itko s nekim programskim znanjem moći pročitati ovaj Dafnyjev kod; Dafny je u velikoj mjeri jezik prilagođen programerima. Jednom kada naučite malo Dafny, vrlo je lako započeti eksperimentiranje, a zatim u osnovi učiti kako idete. A ako ste zainteresirani za učenje Dafny, sjajno mjesto za početak je tutorial serija tvrtke Microsoft. Stranica također uključuje mrežni urednik, pa je vrlo jednostavno isprobati primjere tutorijala. The YouTube kanal za kutak za potvrdu je još jedan izvor korisnih referenci.

Moj trenutak bogojavljenja

Napokon sam želio podijeliti svoj trenutak epifanije iz vremena kada sam učio Dafny. Svakako sam čuo priče o kratkim i jednostavnim dijelovima koda, od velikih renomiranih tvrtki, koje su imale propuštene greške i koje su u konačnici koštale milijune dolara; ali mislim da tek onda kad shvatite koliko bi bilo lako nenamjerno stvoriti grešku u jednostavnoj funkciji sve to ima smisla! Trenutak kada sebi kažete “Oh, bilo bi tako lako napraviti tu pogrešku!”

Moj trenutak došao je dok sam gledao jednog od Video za provjeru u kutu

U ovom vodiču Rustan Leino prolazi kroz SumMax metodu koja uzima dvije cijele vrijednosti, x i y, i vraća zbroj, odnosno max, s i m. Ovaj je primjer relativno jednostavan, a Dafny kôd prikazan je u nastavku.

Unosi x i y specificiraju se kao cijeli brojevi tipkanjem i nisu potrebni drugi preduvjeti. Tri post uvjeta omogućuju provjeru da li izlaz doista udovoljava specifikacijama, naime da je s jednako x + y, te da je m jednako x ili y i da m ne prelazi x i y. Tada se metoda SumMaxBackwards predstavlja kao vježba i tu postaje zanimljivija. Specifikacija je obrnuta od SumMax, tj. S obzirom na zbroj i maksimalni povrat cjelobrojnih x i y. Ok, tako da bi prvi pokušaj mogao biti s istim postuslovima; kako odnosi između ulaza i izlaza još uvijek postoje. Ako dopustimo da je x maksimum, brzi bit algebre govori nam da bi y trebao biti jednak zbroju umanjenom za maksimum. Stavljanje ovog u mrežni uređivač daje sljedeće.

Snimka zaslona 2020. 12. 15 u 6 38 37 sati 1 Snimka zaslona 2020. 12. 16 u 17.35

Ne provjerava. Pa što je pošlo po zlu? Rečeno nam je da postuslov nije vrijedio, a posebno postuslov na liniji 3 (osigurava x<= m && g <= m) možda neće vrijediti. Ako pažljivije pogledamo, vidimo da ovaj uvjet postavljanja navodi x <= m i y <= m. Pa, znamo da je x manje ili jednako m budući da x postavljamo jednako m, pa to znači da je y <= m dio ne potvrđuje. Kako se to može dogoditi? Naša nam je algebra rekla da je y: = s – m. Recimo da je s 5, a m 3, tada je y = 5 – 3 = 2 što osigurava y <= m; ali recimo da ovu metodu zovemo s s jednako 5 i m jednako 1. Ništa nas neće spriječiti da metodu pozovemo s tim ulaznim parametrima, ali ako to učinimo, stvorit ćemo problem jer je y = 5 – 1 = 4, a zatim y > m. Uglavnom, ono što ovdje vidimo je da, iako je ulazni parametar namijenjen maksimalno dvjema cijelim brojevima koji stvaraju zbroj s, ne postoji ništa što bi nas zaustavilo u pokušaju pozivanja metode s ulazom koji nije valjan. Ako nije uključen preduvjet za ograničavanje ulaza s i m na valjane cijele brojeve koji će rezultirati izlazima x i y koji udovoljavaju specifikaciji, tada naša metoda može dati netočne rezultate. Kakav odnos trebamo između s i m da bismo dali valjane unose? Nešto više algebre pokazuje nam da je s <= m * 2 da bi postojalo valjano rješenje x i y. Ako to dodamo kao preduvjet, Dafny sada može provjeriti kôd kao što je prikazano u nastavku. 

Snimka zaslona 2020. 12. 15 u 6 46 32 pm 1 Snimka zaslona 2020. 12. 16 u 17.37

Ovo je bio primjer gdje sam mogao vidjeti koliko je lako uvesti bug u kod. Samo zato što ulazne parametre nazivamo ‘zbroj’, a ‘m’ maksimum, ne znači da će se metoda pozvati na odgovarajući način i kao takva kao dio nekog većeg programa, iz toga bi moglo proizaći mnogo neželjenih posljedica vrsta greške. Nadam se da je korisno za sve druge koji uče o Dafny ili formalnim metodama općenitije.

Na čemu sada radim

Pa to me dovodi do kraja mog posta. Ako želite vidjeti na čemu trenutno radim s Dafny, pogledajte ovo GitHub repo. Dio sam Automatiziranog tima za provjeru unutar R&D na ConsenSysu i koristimo Dafny u formalnoj provjeri specifikacije Ethereum 2 Phase 0. Korištenje formalnih metoda u blockchain prostoru uzbudljivo je novo područje istraživanja koje je prihvatio ConsenSys i ohrabrio bih sve zainteresirane da saznaju više o Eth 2.0 da pogledaju resurse dostupne u našem repo projektu.

Newsletter Pretplatite se na naš newsletter za najnovije vijesti o Ethereumu, rješenja za poduzeća, resurse za programere i još mnogo toga. Adresa e-pošte

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