Obejmowanie mocy metod formalnych w mojej podróży do kodowania: Jak zostałem ewangelistą Dafny

blog 1AktualnościDevelopersEnterpriseBlockchain ExplainedWydarzenia i konferencjePrasaBiuletyny

Zapisz się do naszego newslettera.

Adres e-mail

Szanujemy twoją prywatność

HomeBlogDevelopers

Obejmowanie mocy metod formalnych w mojej podróży do kodowania: Jak zostałem ewangelistą Dafny

przez ConsenSys 22 grudnia 2020 Opublikowane w dniu 22 grudnia 2020

Zrzut ekranu 2020 12 15 o godzinie 6 46 32 1

Joanne Fuller

Chcę zacząć od stwierdzenia, że ​​piszę ten wpis na blogu w nadziei, że inni będą mogli doświadczyć tego objawienia, które miałem podczas nauki Dafny jako część mojej eksploracji metody formalne. Ponadto mam nadzieję, że ten post będzie katalizatorem dla innych, którzy uznają metody formalne za krytyczną i niezbędną umiejętność w arsenale każdego, kto pisze kod. Jako część Zespół automatycznej weryfikacji w R&D w ConsenSys, Używam Dafny do formalnej weryfikacji specyfikacji Ethereum 2 Phase 0 i chcę się podzielić, dlaczego uważam to za przydatne.

Moje tło

Powinienem wyjaśnić, że nie jestem programistą, ale raczej uważam się za programistę matematycznego z pewną wiedzą na temat tworzenia oprogramowania. Po raz pierwszy nauczyłem się pisać programy w ramach zajęć z matematyki w ostatniej klasie liceum i prawdopodobnie powinienem wspomnieć, że chociaż wtedy bardzo lubiłem używać komputerów, perspektywa nauki programowania przeraziła mnie do tego stopnia, że ​​prawie porzuciłem tę konkretną lekcję matematyki. Postanowiwszy zmierzyć się z lękiem przed porażką (w odniesieniu do nauki programowania i potencjalnego zrujnowania mojego wyniku na tych zajęciach), przeszedłem do pierwszego objawienia w kontekście programowania. Wciąż dobrze pamiętam, jak siedziałem na zajęciach i zdałem sobie sprawę, że pisanie programu rozwiązującego zadanie matematyczne nie było jakimś magicznym i tajemniczym procesem, to było prawie jak spisywanie, jak rozwiązałbym problem w mojej głowie. Po tym nie było odwrotu! 

Programowanie było ważnym aspektem wszystkiego, co robiłem od tamtej pory. Mój doktorat z kryptografii polegał w dużej mierze na umiejętności opracowywania algorytmów, a następnie programowania optymalnych implementacji. Moje programy zostały napisane w celu eksperymentowania i chociaż nie podejmowałem się tego, co teraz nazwalibyśmy testowaniem formalnym, nieformalnie sprawdzałem granice i przypadki testowe, używając logicznego rozumowania zamierzonego wyniku. Przez wiele lat pracowałem również jako pracownik naukowy, podejmując badania naukowe z zakresu finansów i ekonomii. Ponownie obejmowało to pisanie programów i ponownie użyłem własnych technik, aby nieformalnie przetestować i uzasadnić ich poprawność. 

Można śmiało powiedzieć, że chociaż doceniałem fakt, że testowanie zawsze będzie niepełne w tym sensie, że niemożliwe jest zbadanie każdego przypadku; że byłem dość pewny, że mój matematyczny sposób myślenia był całkiem dobry, jeśli chodzi o nieformalne testowanie w rygorystyczny sposób. W związku z tym zdecydowanie nie zdawałem sobie sprawy z różnicy między testowaniem a udowodnieniem poprawności, ani też wynikających z tego konsekwencji! W trakcie mojej kariery przed dołączeniem do ConsenSys byłem zadowolony, mogąc polegać na moich własnych nieformalnych technikach określania tego, co uważałem za poprawność za pomocą testów. 

Moje tło jest więc częścią opowieści, ponieważ sam jestem nieco zaskoczony, że wcześniej nie odkryłem formalnych metod. Uważam się za matematyka; Uwielbiam matematykę, algorytmy i logikę. Teraz po prostu poleganie na niekompletnych testach wydaje się szalone, ale również wydaje się szalone, że każdy, kto programuje, przynajmniej nie zdaje sobie sprawy z tego, jakie formalne metody mogą zaoferować i jakie są potencjalne konsekwencje pominięcia błędu, biorąc pod uwagę wiele sposobów, w jakie programy komputerowe są zintegrowane z naszym życiem. Formalne metody pozwalają nam wyjść poza testowanie i udowodnić, że program jest poprawny w stosunku do specyfikacji, która zawiera warunki przed i po. 

Pierwszy przykład Dafny

Jako prosty przykład rozważmy dzielenie całkowite nieujemnej dywidendy n przez dodatni dzielnik d; 


n / d

pokazane poniżej:

Chociaż w typowym języku programowania możemy nieco ograniczyć parametry wejściowe, nie zawsze jest to wystarczające. W tym przykładzie określenie n i d jako liczb naturalnych oznacza, że ​​oba dane wejściowe muszą być nieujemnymi liczbami całkowitymi, ale nie przewiduje ograniczenia d do bycia dodatnią liczbą całkowitą. Użycie warunku wstępnego w formie instrukcji wymaga takiego ograniczenia i oznacza, że ​​metoda ta może zostać wywołana tylko wtedy, gdy d > 0. Stąd, jeśli jakakolwiek inna część programu spowodowałaby wywołanie div bez spełnienia takiego warunku wstępnego, to program nie będzie weryfikował. Instrukcja zapewnia następnie warunek wysłania i podaje formalną specyfikację tego, co musi spełniać wynik metody.

Ten przykład jest napisany przy użyciu Dafny: „Weryfikator języka i programu pod kątem poprawności funkcjonalnej” i prowadzi mnie do następnego punktu, czyli dlaczego jestem takim fanem Dafny. Myślę, że można uczciwie powiedzieć, że dla wielu programistów myśl o użyciu „formalnych metod” weryfikacji poprawności programu jest nieco przerażająca i często jest postrzegana jako „zbyt” trudna. Czy jest to spowodowane brakiem kontaktu z technikami, brakiem oceny korzyści, czy nawet brakiem szkolenia w tej dziedzinie; bez względu na powody uważam, że Dafny może pozwolić każdemu programiście szybko osiągnąć sukces w stosowaniu formalnych metod w swojej pracy. Patrząc na powyższy fragment kodu, spodziewałbym się, że każdy z pewną wiedzą programistyczną będzie w stanie przeczytać ten kod Dafny; Dafny jest bardzo przyjaznym językiem programistom. Kiedy nauczysz się trochę Dafny, bardzo łatwo jest zacząć eksperymentować, a następnie w zasadzie uczyć się w trakcie. A jeśli jesteś zainteresowany nauką Dafny, świetnym miejscem do rozpoczęcia jest seria samouczków przez Microsoft. Witryna zawiera również edytor online, więc bardzo łatwo jest wypróbować przykłady samouczków. Plik Kanał Weryfikacji na YouTube to kolejne źródło przydatnych odniesień.

Moment mojego objawienia

W końcu chciałem podzielić się moim objawieniem z czasów, gdy uczyłem się Dafny. Z pewnością słyszałem historie o krótkich i prostych fragmentach kodu od dużych renomowanych firm, w których błędy zostały pominięte i ostatecznie kosztują wiele milionów dolarów; ale myślę, że tylko wtedy, gdy zdasz sobie sprawę, jak łatwo byłoby nieumyślnie stworzyć błąd w prostej funkcji, wszystko ma sens! Moment, w którym powiesz sobie „Och, tak łatwo byłoby popełnić ten błąd!”

Moja chwila nadeszła podczas oglądania jednego z plików Filmy z kącika weryfikacji

W tym samouczku Rustan Leino przechodzi przez metodę SumMax, która pobiera dwie liczby całkowite, x i y, i zwraca odpowiednio sumę oraz max, s i m. Ten przykład jest stosunkowo prosty, a kod Dafny pokazano poniżej.

Wejścia x i y są określane jako liczby całkowite poprzez wpisywanie i nie są wymagane żadne inne warunki wstępne. Trzy warunki końcowe zapewniają sprawdzenie, czy wynik rzeczywiście spełnia specyfikacje, a mianowicie, że s jest równe x + y, oraz że m jest równe albo x, albo y, oraz że m nie przekracza x i y. Metoda SumMaxBackwards jest następnie prezentowana jako ćwiczenie i tutaj staje się bardziej interesująca. Specyfikacja jest odwrotnością SumMax, tj. Biorąc pod uwagę sumę i maksymalny zwrot liczb całkowitych x i y. Ok, więc pierwsza próba może mieć takie same warunki końcowe; ponieważ relacje między wejściami i wyjściami są nadal aktualne. Jeśli przyjmiemy, że x będzie maksimum, to szybki fragment algebry mówi nam, że y powinno równać się sumie minus maksimum. Umieszczenie tego w edytorze online daje następujące rezultaty.

Zrzut ekranu 2020 12 15 o 6 38 37 1 Zrzut ekranu 2020 12 16 o godzinie 5 35 22

Nie weryfikuje. Więc co poszło nie tak? Powiedziano nam, że warunek końcowy nie został spełniony, a konkretnie warunek końcowy w linii 3 (zapewnia x<= m && y <= m) może nie wytrzymać. Przyglądając się bliżej, widzimy, że ten warunek postu określa, że ​​x <= mi y <= m. Cóż, wiemy, że x jest mniejsze lub równe m, ponieważ ustawiamy x równe m, więc oznacza to, że y <= m część nie weryfikuje się. Jak to się stało? Nasza algebra powiedziała nam, że y: = s – m. Powiedzmy, że s to 5, a m to 3, a następnie y = 5 – 3 = 2, co zapewnia y <= m; ale powiedzmy, że nazywamy tę metodę z s równym 5 im równym 1. Nic nie powstrzyma nas przed wywołaniem metody z tymi parametrami wejściowymi, ale spowoduje to problem, ponieważ y = 5 – 1 = 4, a następnie y > m. Zasadniczo widzimy tutaj, że nawet jeśli parametr wejściowy ma być maksymalnie dwiema liczbami całkowitymi, które tworzą sumę s, nie ma nic, co mogłoby powstrzymać nas przed próbą wywołania metody z nieprawidłowymi danymi wejściowymi. O ile nie zostanie uwzględniony warunek wstępny, aby ograniczyć dane wejściowe s i m do prawidłowych liczb całkowitych, które spowodują, że dane wyjściowe x i y będą zgodne ze specyfikacją, wówczas nasza metoda może dać nieprawidłowe wyniki. Jakiej relacji potrzebujemy między s i m, aby zapewnić prawidłowe dane wejściowe? Trochę więcej algebry pokazuje nam, że s <= m * 2, aby istniało prawidłowe rozwiązanie x i y. Jeśli dodamy to jako warunek wstępny, Dafny może teraz zweryfikować kod, jak pokazano poniżej. 

Zrzut ekranu 2020 12 15 o godzinie 6 46 32 1 Zrzut ekranu 2020 12 16 o godzinie 5 37 39

To był przykład, w którym mogłem zobaczyć, jak łatwo jest wprowadzić błąd do kodu. Tylko dlatego, że nazywamy parametry wejściowe „s” dla sumy i „m” dla maksimum, nie oznacza, że ​​metoda zostanie odpowiednio wywołana i jako taka będzie częścią większego programu, może to spowodować wiele niezamierzonych konsekwencji rodzaj błędu. Mam nadzieję, że będzie to przydatne dla każdego, kto uczy się o Dafny lub bardziej ogólnie formalnych metodach.

Nad czym teraz pracuję

Cóż, to prowadzi mnie do końca mojego postu. Jeśli chcesz zobaczyć, nad czym obecnie pracuję z Dafny, sprawdź to Repozytorium GitHub. Należę do zespołu automatycznej weryfikacji w R&D w ConsenSys i używamy Dafny do formalnej weryfikacji specyfikacji Ethereum 2 Phase 0. Wykorzystanie metod formalnych w przestrzeni blockchain to ekscytujący nowy obszar badań, który został objęty przez ConsenSys i zachęcałbym wszystkich zainteresowanych, aby dowiedzieć się więcej o Eth 2.0, do zapoznania się z zasobami dostępnymi w naszym repozytorium projektów.

Biuletyn Zapisz się do naszego newslettera, aby otrzymywać najnowsze wiadomości dotyczące Ethereum, rozwiązania dla przedsiębiorstw, zasoby dla programistów i nie tylko.

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