1 dienoraštisNewsDevelopersEnterpriseBlockchain ExplainedEvents and ConferencesPressNaujienlaiškiai

Užsiprenumeruokite mūsų naujienlaiškį.

Elektroninio pašto adresas

Mes gerbiame jūsų privatumą

Pagrindinis dienoraštisKūrėjai

Formalių metodų galios panaudojimas mano kodavimo kelionėje: kaip aš tapau „Dafny“ evangelistu

pateikė ConsenSys2020 m. gruodžio 22 d. paskelbta 2020 m. gruodžio 22 d

Ekrano kadras 2020 12 15, 6 46 32 pm 1

Autorius Joanne Fuller

Pirmiausia noriu pasakyti, kad rašau šį tinklaraščio įrašą tikėdamasis, kad kiti gali patirti epifanijos momentą, kurį turėjau mokydamasi Dafny kaip dalis mano žvalgymo į formalūs metodai. Be to, tikiuosi, kad šis įrašas taps katalizatoriumi kitiems vertinant oficialius metodus kaip kritinius ir būtinus įgūdžius kiekvieno, kas rašo kodą, arsenale. Kaip dalis Automatizuota tikrinimo grupė R&D „ConsenSys“, Aš naudoju „Dafny“ oficialiai tikrindamas „Ethereum 2 Phase 0“ specifikaciją ir noriu pasidalinti, kodėl man tai naudinga.

Mano kilmė

Turėčiau aiškiai pasakyti, kad nesu programinės įrangos kūrėjas, veikiau laikau save matematiniu programuotoju, turinčiu tam tikrų žinių apie programinės įrangos kūrimą. Pirmą kartą išmokau rašyti programas matematikos pamokoje paskutiniuose vidurinės mokyklos kursuose ir turbūt turėčiau paminėti, kad nors tuo metu man labai patiko naudotis kompiuteriais, perspektyva išmokti programuoti mane išgąsdino iki taško, kur beveik metė tą konkrečią matematikos klasę. Nusprendusi susidurti su nesėkmės baime (kalbant apie mokymąsi programuoti ir galimai sugadinti savo rezultatą šioje klasėje), aš patyriau savo pirmąjį epifanijos momentą programavimo kontekste. Aš vis dar puikiai atsimenu, kaip sėdėjau klasėje ir supratau, kad programos rašymas matematikos uždaviniui išspręsti nebuvo kažkoks stebuklingas ir paslaptingas procesas, tai buvo beveik kaip užrašyti, kaip aš dirbsiu per savo galvos problemą. Po to nebuvo jokio žvilgsnio atgal! 

Programavimas buvo svarbus aspektas viskam, ką nuo to laiko padariau. Mano daktaro laipsnis kriptografijos srityje labai priklausė nuo gebėjimo sukurti algoritmus ir tada užprogramuoti optimalų įgyvendinimą. Mano programos buvo parašytos eksperimentams ir, nors aš nesiėmiau to, ką dabar vadinsime formaliu testavimu, aš neoficialiai tikrinau ribas ir testavau atvejus, naudodamas loginius argumentus apie numatomą rezultatą. Taip pat daugelį metų dirbau kaip akademinė įmonė finansų ir ekonomikos srityje. Vėlgi, tai apėmė ir rašymo programas, ir aš vėl panaudojau savo metodiką, kad neoficialiai išbandyčiau ir pagrįstume jų teisingumą. 

Sąžininga sakyti, kad nors aš vertinau tai, kad testavimas visada bus neišsamus ta prasme, kad neįmanoma patikrinti kiekvieno atvejo; kad buvau pakankamai įsitikinęs, kad mano matematinis mąstymo būdas buvo gana geras, kai reikėjo griežtai neoficialiai išbandyti. Kaip toks, aš visiškai nevertinau skirtumo tarp testavimo ir teisingumo įrodymo, nei tokio padarinio! Per savo karjerą prieš prisijungdamas prie „ConsenSys“ turėjau pasikliauti savo neformaliais metodais, kad testuodamas galėčiau nustatyti, kas, mano manymu, yra teisingumas.. 

Todėl mano istorija yra istorijos dalis, nes pats esu šiek tiek nustebęs, kad anksčiau neatradau formalių metodų. Laikau save matematike; Man patinka matematika, algoritmai ir logika. Dabar atrodo beprotiška paprasčiausiai pasikliauti neišsamiu testavimu, tačiau taip pat atrodo beprotiška kiekvienam, kuris programuoja, bent jau neįvertinti, ką gali pasiūlyti oficialūs metodai, ir galimos klaidos praleidimo pasekmės, atsižvelgiant į daugybę būdų, kuriais yra kompiuterinės programos integruota į mūsų gyvenimą. Formalūs metodai leidžia neapsiriboti bandymais ir įrodyti, kad programa yra teisinga, palyginti su specifikacija, į kurią įeina išankstinės ir vėlesnės sąlygos. 

Pirmasis „Dafny“ pavyzdys

Paprastu pavyzdžiu laikykime neigiamo dividendo n sveikojo skaičiaus padalijimą iš teigiamo daliklio d; 

n / d

nurodyta apačioje:

Nors spausdinta programavimo kalba mes galime šiek tiek apriboti įvesties parametrus, to ne visada pakanka. Šiame pavyzdyje n ir d kaip natūraliųjų skaičių nurodymas reiškia, kad abu įvestys turi būti ne neigiami sveikieji skaičiai, tačiau joje nenumatytas d apribojimas teigiamu sveikuoju skaičiumi. Naudojant išankstinę sąlygą sakinyje reikalauja, numatomas toks apribojimas ir tai reiškia, kad šį metodą galima naudoti tik tuo atveju, jei d > 0. Taigi, jei kuri nors kita programos dalis sukels „div“ iškvietimą, neįvykdžius tokios išankstinės sąlygos, programa netikrins. Tada užtikrinimo sakinyje pateikiama posto sąlyga ir pateikiama oficiali specifikacija, ką turi atitikti metodo išvestis.

Šis pavyzdys yra parašytas naudojant „Dafny“: „Funkcijų teisingumo kalbos ir programos tikrintojas“ ir atveda mane prie savo kito klausimo, tai yra, kodėl aš esu toks „Dafny“ gerbėjas. Manau, teisinga sakyti, kad daugeliui programuotojų mintis naudoti „formalius metodus“ programos teisingumui patikrinti yra šiek tiek baisi ir dažnai suvokiama kaip „per sunku“. Nesvarbu, ar tai yra dėl nepakankamo technikos taikymo, ar nepakankamai įvertinama nauda, ​​ar net dėl ​​nepakankamo mokymo šioje srityje; kad ir kokios būtų priežastys, manau, kad „Dafny“ turi galimybę leisti bet kuriam programuotojui greitai pasiekti sėkmės taikant oficialius metodus savo darbe. Žvelgdamas į aukščiau pateiktą kodo fragmentą, tikiuosi, kad kiekvienas, turintis šiek tiek programavimo žinių, galės perskaityti šį „Dafny“ kodą; „Dafny“ yra labai programuotojui draugiška kalba. Išmokus truputį „Dafny“, labai lengva pradėti eksperimentuoti ir iš esmės mokytis einant. Ir jei jus domina mokymasis „Dafny“, tai puiki vieta pradėti pamokų serijos pateikė „Microsoft“. Svetainėje taip pat yra internetinis redaktorius, todėl labai lengva išbandyti mokymo pavyzdžius. „YouTube“ kanalas „Patikrinimo kampas“ yra dar vienas naudingų nuorodų šaltinis.

Mano epifanijos akimirka

Galiausiai norėjau pasidalinti savo epifanijos akimirka, kai mokiausi Dafny. Aš tikrai girdėjau pasakojimų apie trumpus ir paprastus kodus iš didelių gerbiamų kompanijų, turinčių klaidų, kurios buvo praleistos ir galiausiai kainavo daug milijonų dolerių; bet manau, kad visa tai yra prasminga tik tada, kai suvoki save, kaip lengva būtų netyčia sukurti paprastos funkcijos klaidą! Tą akimirką, kai sakote sau: „O, taip lengva padaryti tą klaidą!“

Mano akimirka atėjo žiūrint vieną iš Patikrinimo kampo vaizdo įrašai

Šioje pamokoje Rustanas Leino pereina „SumMax“ metodą, kuris apima du skaičius, x ir y, ir pateikia sumą bei max, s ir m. Šis pavyzdys yra gana paprastas, o „Dafny“ kodas parodytas žemiau.

Įvestys x ir y nurodomos kaip sveikieji skaičiai, įvedant tekstą, ir nereikia jokių kitų išankstinių sąlygų. Trijose posto sąlygose tikrinama, ar išvestis iš tikrųjų atitinka specifikacijas, būtent, kad s lygus x + y, o m yra lygus x arba y ir kad m neviršija x ir y. Tada „SumMaxBackwards“ metodas pristatomas kaip pratimas, ir čia jis tampa įdomesnis. Specifikacija yra atvirkštinė „SumMax“, t. Y. Atsižvelgiant į sumą ir didžiausią grąžą sveikieji skaičiai x ir y. Gerai, todėl pirmas bandymas gali būti su tomis pačiomis sąlygomis; nes vis dar išlieka santykiai tarp įvesties ir išvesties. Jei leisime x būti maksimaliu, tada greitas algebros bitas mums sako, kad y turėtų būti lygi sumai, atėmus maksimalią. Tai įvedus į internetinį redaktorių, gaunama:.

Ekrano kadras 2020 12 15, 6 38 37 pm 1 Ekrano kadras 2020 12 16, 5 35 22 val

Tai netikrina. Taigi kas nutiko ne taip? Mums sakoma, kad postcondition neturėjo, o konkrečiai 3 linijos postcondition (užtikrina x<= m && y <= m) gali nelaikyti. Pažvelgus atidžiau, matome, kad ši įrašo sąlyga nurodo, kad x <= m ir y <= m. Na, mes žinome, kad x yra mažesnis arba lygus m, kai nustatome x, lygų m, taigi tai reiškia, kad y <= m dalis nepatikrina. Kaip tai gali atsitikti? Mūsų algebra mums pasakė, kad y: = s – m. Tarkime, kad s yra 5, o m yra 3, tada y = 5 – 3 = 2, kuris užtikrina y <= m; bet tarkime, kad mes vadiname šį metodą, kai s lygus 5 ir m lygus 1. Niekas netrukdys mums skambinti metodu su šiais įvesties parametrais, bet tai padarys, nes y = 5 – 1 = 4 ir tada y > m. Iš esmės tai, ką mes matome, yra tai, kad net jei įvesties parametras yra didžiausias iš dviejų sveikųjų skaičių, kuris sukuria sumą s, niekas netrukdo mums bandyti iškviesti metodą su įvestimi, kuri nėra tinkama. Jei nėra įtraukta išankstinė sąlyga apriboti s ir m įvestis tik su sveikais skaičiais, dėl kurių x ir y išvestys atitiks specifikaciją, mūsų metodas gali suteikti neteisingus rezultatus. Koks mums reikalingas s ir m ryšys, kad galėtume pateikti tinkamus duomenis? Šiek tiek daugiau algebros mums parodo, kad s <= m * 2, kad būtų galiojantis x ir y sprendimas. Jei tai pridėsime kaip išankstinę sąlygą, „Dafny“ dabar gali patikrinti kodą, kaip parodyta žemiau. 

Ekrano kadras 2020 12 15, 6 46 32 pm 1 Ekrano kadras 2020 12 16, 5 37 39 val

Tai buvo pavyzdys, kai mačiau, kaip lengva įvesti klaidą į kodą. Tai, kad įvesties parametrus vadiname „s“ sumai, o „m“ – maksimaliai, dar nereiškia, kad metodas bus tinkamai iškviestas ir kaip dalis didesnės programos gali kilti daugybė nenumatytų pasekmių klaidos tipas. Tikiuosi, kad tai naudinga visiems kitiems, sužinantiems apie „Dafny“ ar formalius metodus apskritai.

Ką aš dabar dirbu

Na, tai atveda mane prie savo įrašo pabaigos. Jei norite pamatyti, ką šiuo metu dirbu su „Dafny“, patikrinkite tai „GitHub“ atpirkimas. Esu „R“ automatinio tikrinimo grupės dalis&D „ConsenSys“ ir mes naudojame „Dafny“ oficialiai tikrinant „Ethereum 2 Phase 0“ specifikaciją. Oficialių metodų naudojimas „blockchain“ erdvėje yra nauja įdomi tyrimų sritis, kurią apėmė „ConsenSys“, ir aš norėčiau paraginti visus, norinčius sužinoti daugiau apie „Etht 2.0“, pažvelgti į mūsų projekto repo šaltinius..

Užsiprenumeruokite mūsų naujienlaiškį, kuriame rasite naujausias „Ethereum“ naujienas, įmonės sprendimus, kūrėjų išteklius ir dar daugiau. El. Pašto adresas

Mike Owergreen Administrator
Sorry! The Author has not filled his profile.
follow me