A formális módszerek erejének felhasználása a kódolási utazásomban: Hogyan lettem Dafny evangélista

blog 1NewsDevelopersEnterpriseBlockchain ExplainedEvents and ConferencesPressHírlevelek

Iratkozzon fel hírlevelünkre.

Email cím

Tiszteletben tartjuk a magánéletét

HomeBlogDevelopers

A formális módszerek erejének felhasználása a kódolási utazásomban: Hogyan lettem Dafny evangélista

Készítette ConsenSys 2020. december 22. Feladva 2020. december 22-én

Képernyőkép - 2020 12 15, 6 46 32 pm 1

Írta: Joanne Fuller

Először azt akarom mondani, hogy ezt a blogbejegyzést abban a reményben írom, hogy mások is megtapasztalhatják az epifániai pillanatot, amelyet a tanulás során éltem át Dafny -ig tartó feltárásom részeként formális módszerek. Remélem továbbá, hogy ez a bejegyzés katalizátorként hat arra, hogy mások a formális módszereket kritikus és szükséges készségnek tekintsék bárkinek, aki kódot ír. A Automatizált ellenőrző csoport az R-en belül&D a ConsenSys-nél, A Dafny-t használom az Ethereum 2 Phase 0 specifikáció hivatalos ellenőrzésében, és szeretném megosztani, miért találom hasznosnak.

Az én hátterem

Világossá kell tennem, hogy nem vagyok szoftverfejlesztő, inkább matematikai programozónak tartom magam, aki ismeri a szoftverfejlesztést. A matematika órám részeként tanultam először programokat írni a gimnázium utolsó évében, és valószínűleg meg kell említenem, hogy bár abban az időben nagyon szerettem használni a számítógépeket, a programozás megtanulásának lehetősége odáig rémített, hogy szinte elejtette azt a bizonyos matematika órát. Miután elhatároztam, hogy szembesülök a kudarctól való félelmemmel (a programozás megtanulása és az osztályban elért eredményem potenciális tönkretétele tekintetében), megtapasztaltam első epifániai pillanatomat a programozás összefüggésében. Még mindig élénken emlékszem arra, hogy az osztályban ültem, és rájöttem, hogy egy matematikai probléma megoldására program írása nem valami varázslatos és titokzatos folyamat volt, szinte olyan volt, mintha leírnám, hogyan dolgoznék át egy problémát a fejemben. Utána nem lehetett visszanézni! 

A programozás fontos szempont mindannak, amit azóta csináltam. A rejtjelezéssel foglalkozó doktorom nagyban támaszkodott algoritmusok kifejlesztésének, majd az optimális megvalósítások programozásának képességére. A programjaim kísérleti célokra készültek, és bár nem vállaltam el, amit most formális tesztelésnek neveznénk, informálisan ellenőriztem a határokat és az eseteket a tervezett kimenetre vonatkozó logikai érvelés segítségével. Hosszú évekig akadémikusként dolgoztam a pénzügyi és a közgazdasági területen. Ez megint tartalmazta a programok írását, és ismét saját technikáimat használtam informális tesztelésre és indoklásra azok helyességéről. 

Igaz mondani, hogy bár nagyra értékeltem azt a tényt, hogy a tesztelés mindig hiányos lenne abban az értelemben, hogy lehetetlen minden esetet tesztelni; hogy eléggé biztos voltam abban, hogy matematikai gondolkodásmódom nagyon jó volt, amikor informális, szigorú módon teszteltem. Mint ilyen, határozottan nem értékeltem teljes mértékben a különbséget a tesztelés és a helyesség bizonyítása között, sem annak következményeit! Pályafutásom során, mielőtt csatlakoztam volna a ConsenSys-hez, megelégedtem azzal, hogy saját informális technikáimra támaszkodtam, hogy tesztelés útján megállapíthassam a helyességet. 

A hátterem tehát része a történetnek, mivel magam is meglepődtem, hogy korábban nem fedeztem fel a formális módszereket. Matematikusnak tartom magam; Szeretem a matematikát, az algoritmusokat és a logikát. Őrültségnek tűnik egyszerűen a hiányos tesztelésre hagyatkozni, de az is őrültségnek tűnik, hogy aki programoz, legalább ne vegye tiszteletben a formális módszerek kínálatát és a hiba hiányának lehetséges következményeit, tekintettel a számítógépes programok sokféleképpen integrálódott az életünkbe. A formális módszerek lehetővé teszik számunkra, hogy túllépjünk a tesztelésen, bebizonyítsuk, hogy egy program helyes-e az elő- és utáni feltételeket tartalmazó specifikációval szemben. 

Az első Dafny példa

Egyszerű példaként vegyük figyelembe egy nem negatív n osztalék egész számának pozitív d osztóval való osztását; 


n / d

lásd alább:

Bár egy beírt programozási nyelven némileg korlátozhatjuk a bemeneti paramétereket, ez nem mindig elegendő. Ebben a példában n és d természetes számok megadása azt jelenti, hogy mindkét bemenetnek nem negatív egész számnak kell lennie, de nem írja elő a d pozitív egész számra való korlátozását. Az előfeltétel használata a utasításként ilyen korlátozást ír elő, és azt jelenti, hogy ez a módszer csak akkor hívható meg, ha d > 0. Ezért, ha a program bármely más része miatt a div meghívható anélkül, hogy egy ilyen előfeltétel teljesülne, akkor a program nem fogja ellenőrizni. Ezután a sure utasítás megadja a poszt feltételét és hivatalos specifikációt ad arról, hogy a metódus kimenetének mit kell teljesítenie.

Ez a példa a Dafny segítségével íródott: „A nyelv és a program ellenőrzője a funkcionális helyességért”, és eljut a következő kérdésemhez, vagyis miért rajongok annyira a Dafnyért. Úgy gondolom, hogy méltányos azt mondani, hogy sok programozó számára az a gondolat, hogy „formális módszereket” alkalmaznak a program helyességének ellenőrzésére, kissé ijesztő, és gyakran „túl” nehéznek tartják. Akár a technikáknak való kitettség hiánya, akár az előnyök felmérésének hiánya, akár a képzés hiánya miatt van ezen a területen; bármi is legyen az oka, úgy gondolom, hogy a Dafny képes megengedni, hogy bármely programozó gyorsan elérje a formális módszerek munkájában való alkalmazását. A fenti kódrészletet nézve azt várnám, hogy bárki, aki rendelkezik valamilyen programozási ismerettel, képes elolvasni ezt a Dafny-kódot; A Dafny nagyon programozóbarát nyelv. Miután megtanult egy kicsit a Dafny-ból, nagyon könnyű elkezdeni a kísérletezést, majd alapvetően megtanulni menet közben. És ha érdekel a Dafny megtanulása, akkor remek kiindulópont a oktatósorozat a Microsoft. Az oldalon található egy online szerkesztő is, így nagyon egyszerű kipróbálni a bemutató példákat. A Ellenőrző sarok YouTube-csatorna a hasznos hivatkozások másik forrása.

Vízkereszt pillanatom

Végül meg akartam osztani a vízkereszt pillanatát, amikor Dafnyt tanultam. Bizonyára hallottam rövid és egyszerű kóddarabokról szóló történeteket nagy neves cégektől, amelyek hibáit kihagyták, és végül sok millió dollárba kerültek; de szerintem csak akkor van értelme, ha rájön, milyen egyszerű lenne akaratlanul hibát létrehozni egy egyszerű funkcióban! Abban a pillanatban, amikor azt mondod magadnak: „Ó, olyan könnyű lenne ezt a hibát elkövetni!”

Az egyik pillanat megtekintése közben eljött a pillanatom Ellenőrző sarok videók

Ebben az oktatóanyagban Rustan Leino egy SumMax módszeren megy keresztül, amely két egész számot vesz fel, x-et és y-t, és visszaadja az összeget, valamint a max, s és m értékeket. Ez a példa viszonylag egyszerű, és a Dafny-kód alább látható.

Az x és y bemeneteket egész számként adjuk meg gépeléssel, és nincs szükség más előfeltételekre. A három utólagos feltétel ellenőrzi, hogy a kimenet valóban megfelel-e a specifikációknak, nevezetesen, hogy s egyenlő x + y-vel, és m egyenlő akár x-vel, akár y-vel, és hogy m nem haladja meg az x-et és az y-t. A SumMaxBackwards módszert ezután gyakorlatként mutatják be, és ez válik érdekesebbé. A specifikáció a SumMax fordítottja, vagyis megadva az x és y egész számok összegét és maximális hozamát. Oké, tehát az első próbálkozás ugyanazokkal az utólagos feltételekkel történhet; mivel a bemenetek és a kimenetek közötti kapcsolatok továbbra is fennállnak. Ha hagyjuk, hogy x legyen a maximum, akkor az algebra egy gyors bitje azt mondja nekünk, hogy y-nak meg kell egyeznie az összeggel, levonva a maximumot. Ha ezt beteszi az online szerkesztőbe, a következőket kapja.

Képernyőfelvétel 2020 12 15, 6 38 37, pm 1 Képernyőfelvétel 2020 12 16, 5 35, 22 óra

Nem igazolja. Tehát mi ment rosszul? Nekünk azt mondják, hogy egy utófeltétel nem állt fenn, és konkrétan a 3. vonal utókondíciója (biztosítja az x-et<= m && y <= m) nem tarthat. Jobban megnézve azt látjuk, hogy ez az utólagos feltétel meghatározza, hogy x <= m és y <= m. Nos, tudjuk, hogy x kisebb vagy egyenlő m-rel, mivel x-et állítjuk m-nek, tehát ez azt jelenti, hogy az y <= m rész nem igazolja. Hogyan történhet ez meg? Algebránk elmondta, hogy y: = s – m. Tegyük fel, hogy s értéke 5 és m értéke 3, akkor y = 5 – 3 = 2, ami biztosítja y-t <= m; de tegyük fel, hogy ezt a módszert úgy hívjuk, hogy s értéke 5, m értéke pedig 1. Semmi sem akadályoz meg bennünket abban, hogy a bemeneti paraméterekkel hívjuk meg a módszert, de ez problémát okoz, mivel y = 5 – 1 = 4, majd y > m. Alapvetően azt látjuk itt, hogy annak ellenére, hogy a bemeneti paraméter két egész szám maximális számát jelenti, amely létrehozza az s összeget, semmi sem akadályozza meg, hogy érvénytelen bemenettel próbáljuk meghívni a módszert. Hacsak nincs előfeltétel az s és m bemenetek érvényes egész számokra való korlátozása, amelyek x és y kimenetet eredményeznek, amelyek megfelelnek a specifikációnak, akkor módszerünk hibás eredményeket produkálhat. Milyen kapcsolatra van szükségünk s és m között az érvényes bemenetek biztosításához? Egy kicsit több algebra megmutatja nekünk, hogy s <= m * 2, hogy x és y érvényes megoldása legyen. Ha ezt előfeltételként hozzáadjuk, a Dafny mostantól képes ellenőrizni a kódot az alábbiak szerint. 

Képernyőkép - 2020 12 15, 6 46 32 pm 1 Képernyőfelvétel 2020 12 16, 5 37 39 órakor

Ez volt az a példa, ahol láthattam, milyen egyszerű egy hibát bevezetni a kódba. Az, hogy a bemeneti paramétereket ‘s’ összegnek hívjuk, az ‘m’ pedig a maximumot, nem jelenti azt, hogy a metódust megfelelően hívják meg, és mint ilyen valamilyen nagyobb program részeként, ebből sok nem szándékos következmény lehet típusú hiba. Remélem, hogy bárki más számára hasznos, aki megismeri a Dafny-t vagy a formális módszereket általánosabban.

Amivel most dolgozom

Nos, ezzel a bejegyzésem végére jutok. Ha szeretné megnézni, min dolgozom jelenleg Dafnyval, akkor nézze meg ezt GitHub repo. Az R csoporton belül az automatizált ellenőrzési csoport tagja vagyok&D a ConsenSys-nél, és a Dafny-t használjuk az Ethereum 2 Phase 0 specifikáció hivatalos ellenőrzéséhez. A formális módszerek használata a blokklánc térben egy izgalmas új kutatási terület, amelyet a ConsenSys átfogott, és arra bátorítanék mindenkit, aki szeretne többet megtudni az Eth 2.0-ról, hogy nézze meg a projekt-repónkban rendelkezésre álló erőforrásokat.

Iratkozzon fel hírlevelünkre a legfrissebb Ethereum-hírekről, vállalati megoldásokról, fejlesztői erőforrásokról és egyebekről. E-mail cím

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