Sprejemanje moči formalnih metod v mojem kodiranju: Kako sem postala evangelistka Dafny

blog 1NewsDevelopersEnterpriseBlockchain ExplainedDogodki in konferencePressGlasila

Naročite se na naše novice.

Email naslov

Spoštujemo vašo zasebnost

DomovBlogDevelopers

Sprejemanje moči formalnih metod v mojem kodiranju: Kako sem postala evangelistka Dafny

avtor ConsenSys 22. december 2020 Objavljeno 22. decembra 2020

Posnetek zaslona 2020 12 15 ob 6 46 32 pm 1

Joanne Fuller

Za začetek bi rad rekel, da pišem to objavo v blogu v upanju, da bodo drugi lahko izkusili epifanijski trenutek, ki sem ga imel med učenjem Dafny kot del mojega raziskovanja formalne metode. Nadalje upam, da bo ta objava delovala kot katalizator za druge, ki bodo formalne metode obravnavali kot kritično in potrebno veščino v arzenalu vsakogar, ki piše kodo. Kot del Skupina za avtomatizirano preverjanje znotraj R&D pri ConsenSys, Dafny uporabljam pri uradnem preverjanju specifikacije Ethereum 2 Phase 0 in želim povedati, zakaj se mi zdi koristen.

Moje ozadje

Jasno bi moral povedati, da nisem razvijalec programske opreme, temveč se imam za matematičnega programerja z nekaj znanja o razvoju programske opreme. Prvič sem se naučil pisati programe v okviru pouka matematike v zadnjem letniku srednje šole in verjetno bi moral omeniti, da čeprav sem takrat rad uporabljal računalnike, me je možnost učenja programiranja prestrašila do te mere, da sem skoraj opustil ta razred matematike. Ko sem se odločil, da se bom soočil s svojim strahom pred neuspehom (kar se tiče učenja programiranja in morebitnega uničenja mojega rezultata v tem razredu), sem prvi trenutek epifanije doživel v okviru programiranja. Še vedno se živo spominjam, kako sem sedel v razredu in se zavedal, da pisanje programa za reševanje matematičnega problema ni bil kakšen čaroben in skrivnosten postopek, skoraj kot da bi si zapisal, kako bom rešil problem v glavi. Po tem ni bilo pogleda nazaj! 

Programiranje je pomemben vidik vsega, kar sem počel od takrat. Moj doktorat iz kriptografije se je močno zanašal na sposobnost razvijanja algoritmov in nato programiranja optimalnih izvedb. Moji programi so bili napisani za eksperimentiranje, in čeprav se nisem lotil tega, kar bi zdaj imenovali kot formalno testiranje, bi neformalno preverjal meje in preizkušal primere z logičnim sklepanjem o predvidenih rezultatih. Dolga leta sem delal tudi kot akademsko raziskovalno podjetje na področju financ in ekonomije. Tudi to je vključevalo pisanje programov in spet sem uporabil lastne tehnike za neformalno preizkušanje in utemeljevanje njihove pravilnosti. 

Pošteno je reči, da čeprav sem cenil dejstvo, da bo testiranje vedno nepopolno v smislu, da je nemogoče preizkusiti vsak primer; da sem bil upravičeno prepričan, da je bil moj matematični način razmišljanja precej dober, ko je šlo za neformalno testiranje na strog način. Kot tak definitivno nisem popolnoma spoznal razlike med testiranjem in dokazovanjem pravilnosti niti posledic takega! V svoji karieri, preden sem se pridružil ConsenSys, sem se zadovoljen zanašal na lastne neformalne tehnike, s katerimi sem s testiranjem ugotovil, kaj je pravilno. 

Moje ozadje je torej del zgodbe, saj sem tudi sam nekoliko presenečen, da prej nisem odkril formalnih metod. Imam se za matematika; Obožujem matematiko, algoritme in logiko. Zdaj se zdi noro, če se preprosto zanašamo na nepopolno preizkušanje, prav tako pa se zdi noro, da vsak, ki programira, vsaj ne razume, kaj lahko formalne metode ponujajo, in morebitne posledice, če bi pogrešali napako glede na številne načine, na katere so računalniški programi vključeni v naše življenje. Formalne metode nam omogočajo, da presežemo testiranje in dokažemo, da je program pravilen glede na specifikacijo, ki vključuje pogoje pred in po objavi. 

Prvi primer Dafnyja

Kot preprost primer upoštevamo celoštevilčno delitev nenegativne dividende n s pozitivnim deliteljem d; 


n / d

prikazano spodaj:

Čeprav lahko v vtipkanem programskem jeziku nekoliko omejimo vhodne parametre, to ni vedno dovolj. V tem primeru specifikacija n in d kot naravni števili pomeni, da morata biti oba vhoda celo negativna cela števila, vendar ne predvideva omejitve d na pozitivno celo število. Uporaba predpogoja prek stavka require predvideva takšno omejitev in pomeni, da je to metodo mogoče poklicati le, če je d > 0. Torej, če bi kateri koli drug del programa povzročil klic div, ne da bi bil tak pogoj izpolnjen, potem program ne bo preveril. Izjava zagotavlja nato poda pogoj post in formalno specifikacijo, kaj mora izpolnjevati izhod metode.

Ta primer je napisan z uporabo Dafnyja: »Preverjevalec jezika in programa za funkcionalno pravilnost« in me pripelje do naslednje točke, torej, zakaj sem tako navdušen nad Dafnyjem. Mislim, da je pošteno reči, da je pri mnogih programerjih misel o uporabi “formalnih metod” za preverjanje pravilnosti programa nekoliko zastrašujoča in se pogosto dojema kot “preveč” težka. Ne glede na to, ali gre za pomanjkanje izpostavljenosti tehnikam, zanemarjanje prednosti ali celo pomanjkanje usposabljanja na tem področju; ne glede na razloge, verjamem, da ima Dafny možnost, da programerjem omogoči hitro doseganje uspeha pri uporabi formalnih metod pri svojem delu. Če pogledam zgornji delček kode, bi pričakoval, da bo lahko kdo Dafny prebral kdo z nekaj programskega znanja; Dafny je zelo prijazna do programerjev jezik. Ko se malo naučiš Dafnyja, je zelo enostavno začeti eksperimentirati in se v bistvu učiti, ko greš. In če vas zanima učenje Dafny, je odličen kraj za začetek vadbena serija Microsoft. Spletno mesto vključuje tudi spletni urejevalnik, zato je zelo enostavno preizkusiti primere vadnic. The YouTube-ov potrditveni kotiček je še en vir uporabnih referenc.

Moj trenutek epifanije

Končno sem želel deliti svoj epifanijski trenutek, ko sem se učil Dafny. Zagotovo sem že slišal zgodbe o kratkih in preprostih delih kode velikih uglednih podjetij, ki so pogrešale napake in so na koncu stale več milijonov dolarjev; mislim pa, da je šele takrat, ko se zaveš, kako enostavno bi bilo nenamerno ustvariti napako v preprosti funkciji, smiselno! Trenutek, ko si rečete: “Oh, tako enostavno bi bilo narediti to napako!”

Moj trenutek je nastopil med gledanjem enega od Video posnetki v kotu za preverjanje

V tej vadnici Rustan Leino prehaja skozi metodo SumMax, ki zavzame dve celi števili x in y ter vrne vsoto oziroma max, s in m. Ta primer je razmeroma enostaven, koda Dafny pa je prikazana spodaj.

Vnosa x in y sta s tipkanjem podana kot celo število in nobeni drugi predpogoji niso potrebni. Ti trije pogoji zagotavljajo preverjanje, ali izhod resnično izpolnjuje zahteve, in sicer da je s enako x + y in da je m enako x ali y in da m ne presega x in y. Metoda SumMaxBackwards je nato predstavljena kot vaja in tu postane bolj zanimiva. Specifikacija je obratna vrednost SumMax, to je glede na vsoto in največjo vrnitev celih števil x in y. Ok, torej prvi poskus je lahko z enakimi postpogoji; saj razmerja med vhodi in izhodi še vedno obstajajo. Če pustimo, da je x največ, potem hitri del algebre pove, da mora biti y enak vsoti minus maksimumu. Če to vstavite v spletni urejevalnik, dobite naslednje.

Posnetek zaslona 2020 12 15 ob 6 38 37 pm 1 Posnetek zaslona 2020 12 16 ob 17.35

Ne preveri. Torej, kaj je šlo narobe? Povedali so nam, da postkondicija ni držala in še posebej postkondicija v vrstici 3 (zagotavlja x<= m && y <= m) morda ne drži. Če pogledamo natančneje, vidimo, da ta pogoj objave določa, da je x <= m in y <= m. No, vemo, da je x manj ali enako m, saj x nastavimo na m, zato to pomeni, da je y <= m del ne preveri. Kako se to lahko zgodi? Naša algebra nam je povedala, da je y: = s – m. Recimo, da je s 5 in m 3, potem je y = 5 – 3 = 2, kar zagotavlja y <= m; vendar recimo, da to metodo pokličemo s s enako 5 in m enako 1. Nič nam ne bo preprečilo, da bi metodo poklicali s temi vhodnimi parametri, vendar bo to povzročilo težavo, saj je y = 5 – 1 = 4 in nato y > m. V bistvu to, kar vidimo tukaj, je, da čeprav naj bi bil vhodni parameter največ dve celoštevilki, ki ustvarjata vsoto s, nas nič ne ustavi, da bi metodo poskusili poklicati z neveljavnim vhodom. Če ni vključen predpogoj za omejitev vhodov s in m na veljavna cela števila, ki bodo povzročila izhoda x in y, ki ustrezata specifikaciji, potem lahko naša metoda povzroči napačne rezultate. Kakšno razmerje potrebujemo med s in m, da zagotovimo veljavne vnose? Nekaj ​​več algebre nam pokaže, da s <= m * 2, da obstaja veljavna rešitev x in y. Če to dodamo kot predpogoj, lahko Dafny zdaj preveri kodo, kot je prikazano spodaj. 

Posnetek zaslona 2020 12 15 ob 6 46 32 pm 1 Posnetek zaslona 2020 12 16 ob 5 37 39 pm

To je bil primer, ko sem videl, kako enostavno je v kodo uvesti napako. Samo zato, ker vhodne parametre imenujemo ‘s’ za vsoto in ‘m’ za največ, še ne pomeni, da bo metoda pravilno poklicana in kot taka kot del nekega večjega programa lahko iz tega sledi veliko neželenih posledic vrsta napake. Upam, da je koristno za koga drugega, ki se uči o Dafny ali formalnih metodah na splošno.

Na čem zdaj delam

No, to me pripelje do konca moje objave. Če bi radi videli, na čem trenutno delam z Dafny, si oglejte to Repo za GitHub. Sem del skupine za avtomatizirano preverjanje znotraj R&D pri ConsenSys in Dafny uporabljamo pri formalni verifikaciji specifikacije Ethereum 2 Phase 0. Uporaba formalnih metod v prostoru verige blokov je vznemirljivo novo področje raziskav, ki ga je sprejel ConsenSys, in vse, ki jih zanima več o Eth 2.0, pozivam, naj si ogledajo vire, ki so na voljo v okviru repo projekta.

Na naše novice se naročite na najnovejše novice o Ethereumu, rešitve za podjetja, vire za razvijalce in drugo.

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