Ten artykuł jest tłumaczeniem . Ale przed nią małe wprowadzenie. Jak powstają zombie? Każdy znalazł się w sytuacji, w której chce podciągnąć kolegę lub kolegę do swojego poziomu, ale nie wychodzi. I nie tyle z tobą, co z nim „nie wychodzi”: po jednej stronie skali jest normalna pensja, zadania i tak dalej, a po drugiej potrzeba myślenia. Myślenie jest nieprzyjemne i bolesne. Szybko się poddaje i kontynuuje pisanie kodu bez włączania mózgu. Wyobrażasz sobie, ile wysiłku wymaga pokonanie bariery wyuczonej bezradności i po prostu tego nie robisz. Tak powstają zombie, które, jak się wydaje, można wyleczyć, ale wygląda na to, że nikt tego nie zrobi.
Kiedy to zobaczyłem (tak, ten sam kolega z podręczników) i nie sporządza raportu, ale sesję pytań i odpowiedzi, byłem trochę ostrożny. Na wszelki wypadek Leslie jest światowej sławy naukowcem, autorem fundamentalnych prac z zakresu przetwarzania rozproszonego, można go też poznać po literach La w słowie LaTeX – „Lamport TeX”. Drugim niepokojącym czynnikiem jest jego wymaganie: każdy, kto przychodzi, musi (całkowicie bezpłatnie) wysłuchać wcześniej kilku jego raportów, wymyślić co najmniej jedno pytanie na ich temat i dopiero wtedy przyjść. Postanowiłem zobaczyć, co tam emituje Lamport – i jest super! To jest dokładnie to, magiczna pigułka łącząca do leczenia zombie. Ostrzegam: z tekstu mogą się wypalić miłośnicy superelastycznych metodologii i ci, którzy nie lubią sprawdzać tego, co jest napisane.
Po habrokacie rozpoczyna się właściwie tłumaczenie seminarium. Miłego czytania!
Niezależnie od tego, jakiego zadania się podejmiesz, zawsze musisz przejść przez trzy kroki:
- zdecyduj, jaki cel chcesz osiągnąć;
- zdecyduj, w jaki sposób osiągniesz swój cel;
- dojść do celu.
Dotyczy to również programowania. Pisząc kod musimy:
- zdecydować, co program powinien robić;
- określić, w jaki sposób ma wykonywać swoje zadanie;
- napisz odpowiedni kod.
Ostatni krok jest oczywiście bardzo ważny, ale nie będę o nim dzisiaj mówić. Zamiast tego omówimy pierwsze dwa. Każdy programista wykonuje je przed przystąpieniem do pracy. Nie siadasz do pisania, dopóki nie zdecydujesz, czy piszesz przeglądarkę, czy bazę danych. Pewna idea celu musi być obecna. I zdecydowanie zastanawiasz się, co dokładnie zrobi program, i nie piszesz jakoś w nadziei, że kod jakoś zamieni się w przeglądarkę.
Jak dokładnie odbywa się to wstępne myślenie kodu? Ile wysiłku powinniśmy w to włożyć? Wszystko zależy od tego, jak złożony problem rozwiązujemy. Załóżmy, że chcemy napisać system rozproszony odporny na uszkodzenia. W takim przypadku powinniśmy dokładnie przemyśleć wszystko, zanim usiądziemy do kodowania. Co jeśli potrzebujemy tylko zwiększyć zmienną całkowitą o 1? Na pierwszy rzut oka wszystko jest tutaj banalne i nie wymaga myślenia, ale potem przypominamy sobie, że może wystąpić przepełnienie. Dlatego nawet, aby zrozumieć, czy problem jest prosty, czy złożony, najpierw trzeba pomyśleć.
Jeśli z wyprzedzeniem pomyślisz o możliwych rozwiązaniach problemu, możesz uniknąć błędów. Ale to wymaga jasnego myślenia. Aby to osiągnąć, musisz zapisać swoje myśli. Bardzo podoba mi się cytat Dicka Guindona: „Kiedy piszesz, natura pokazuje ci, jak niedbałe jest twoje myślenie”. Jeśli nie piszesz, myślisz tylko, że myślisz. I musisz zapisać swoje przemyślenia w formie specyfikacji.
Specyfikacje pełnią wiele funkcji, szczególnie w dużych projektach. Ale powiem tylko o jednym z nich: pomagają nam jasno myśleć. Jasne myślenie jest bardzo ważne i dość trudne, dlatego tutaj potrzebujemy wszelkiej pomocy. W jakim języku pisać specyfikacje? Generalnie jest to zawsze pierwsze pytanie programistów: w jakim języku będziemy pisać. Nie ma na to jednej poprawnej odpowiedzi: problemy, które rozwiązujemy, są zbyt różnorodne. Dla niektórych TLA+ to opracowany przeze mnie język specyfikacji. Dla innych wygodniej jest używać języka chińskiego. Wszystko zależy od sytuacji.
Ważniejsze jest inne pytanie: jak osiągnąć jaśniejsze myślenie? Odpowiedź: Musimy myśleć jak naukowcy. Jest to sposób myślenia, który sprawdził się w ciągu ostatnich 500 lat. W nauce budujemy modele matematyczne rzeczywistości. Astronomia była być może pierwszą nauką w ścisłym tego słowa znaczeniu. W modelu matematycznym używanym w astronomii ciała niebieskie pojawiają się jako punkty z masą, położeniem i pędem, chociaż w rzeczywistości są to niezwykle złożone obiekty z górami i oceanami, pływami i przypływami. Ten model, jak każdy inny, został stworzony w celu rozwiązania pewnych problemów. Jest świetny do zastanawiania się, gdzie skierować teleskop, jeśli chcesz znaleźć planetę. Ale jeśli chcesz przewidzieć pogodę na tej planecie, ten model nie zadziała.
Matematyka pozwala nam określić właściwości modelu. A nauka pokazuje, jak te właściwości mają się do rzeczywistości. Porozmawiajmy o naszej nauce, informatyce. Rzeczywistość, z którą pracujemy, to różnego rodzaju systemy komputerowe: procesory, konsole do gier, komputery, programy wykonawcze i tak dalej. Opowiem o uruchamianiu programu na komputerze, ale ogólnie rzecz biorąc, wszystkie te wnioski dotyczą dowolnego systemu komputerowego. W naszej nauce posługujemy się wieloma różnymi modelami: maszyną Turinga, częściowo uporządkowanymi zbiorami zdarzeń i wieloma innymi.
Co to jest program? Jest to dowolny kod, który można rozpatrywać niezależnie. Załóżmy, że musimy napisać przeglądarkę. Wykonujemy trzy zadania: projektujemy widok programu dla użytkownika, następnie piszemy wysokopoziomowy diagram programu, a na koniec piszemy kod. Pisząc kod, zdajemy sobie sprawę, że musimy napisać formater tekstu. Tutaj ponownie musimy rozwiązać trzy problemy: określić, jaki tekst zwróci to narzędzie; wybierz algorytm formatowania; napisz kod. To zadanie ma swoje własne podzadanie: poprawnie wstaw myślnik do słów. To podzadanie również rozwiązujemy w trzech krokach – jak widać powtarzają się one na wielu poziomach.
Rozważmy bardziej szczegółowo pierwszy krok: jaki problem rozwiązuje program. Tutaj najczęściej modelujemy program jako funkcję, która pobiera pewne dane wejściowe i generuje pewne dane wyjściowe. W matematyce funkcja jest zwykle opisywana jako uporządkowany zestaw par. Na przykład funkcja podnosząca do kwadratu dla liczb naturalnych jest opisana jako zbiór {<0,0>, <1,1>, <2,4>, <3,9>, …}. Dziedziną takiej funkcji jest zbiór pierwszych elementów każdej pary, czyli liczby naturalne. Aby zdefiniować funkcję, musimy określić jej zakres i formułę.
Ale funkcje w matematyce to nie to samo, co funkcje w językach programowania. Matematyka jest dużo łatwiejsza. Ponieważ nie mam czasu na skomplikowane przykłady, rozważmy prosty: funkcję w C lub metodę statyczną w Javie, która zwraca największy wspólny dzielnik dwóch liczb całkowitych. W specyfikacji tej metody napiszemy: oblicza GCD(M,N) dla argumentów M и NGdzie GCD(M,N) - funkcja, której dziedziną jest zbiór par liczb całkowitych, a zwracaną wartością jest największa liczba całkowita podzielna przez M и N. Jak ten model ma się do rzeczywistości? Model działa na liczbach całkowitych, podczas gdy w C czy Javie mamy 32-bitowy int. Model ten pozwala nam zdecydować, czy algorytm jest poprawny GCD, ale nie zapobiegnie to błędom przepełnienia. Wymagałoby to bardziej złożonego modelu, na który nie ma czasu.
Porozmawiajmy o ograniczeniach funkcji jako modelu. Niektóre programy (takie jak systemy operacyjne) nie tylko zwracają określoną wartość dla określonych argumentów, ale mogą działać w sposób ciągły. Ponadto funkcja jako model nie nadaje się dobrze do drugiego kroku: planowania sposobu rozwiązania problemu. Sortowanie szybkie i sortowanie bąbelkowe obliczają tę samą funkcję, ale są to zupełnie inne algorytmy. Dlatego, aby opisać, w jaki sposób osiągany jest cel programu, posługuję się innym modelem, nazwijmy go standardowym modelem behawioralnym. Program w nim przedstawiony jest jako zbiór wszystkich dopuszczalnych zachowań, z których każde z kolei jest ciągiem stanów, a stan to przypisanie wartości do zmiennych.
Zobaczmy, jak wyglądałby drugi krok algorytmu Euclid. Musimy obliczyć GCD(M, N). Inicjujemy M jak xI N jak y, a następnie wielokrotnie odejmij mniejszą z tych zmiennych od większej, aż będą równe. Na przykład, jeśli M = 12I N = 18, możemy opisać następujące zachowanie:
[x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6]
A jeśli M = 0 и N = 0? Zero jest podzielne przez wszystkie liczby, więc w tym przypadku nie ma największego dzielnika. W tej sytuacji musimy wrócić do pierwszego kroku i zadać sobie pytanie: czy naprawdę musimy obliczać NWD dla liczb nie dodatnich? Jeśli nie jest to konieczne, wystarczy zmienić specyfikację.
W tym miejscu powinniśmy zrobić małą dygresję dotyczącą produktywności. Często mierzy się ją liczbą linii kodu pisanych dziennie. Ale twoja praca jest o wiele bardziej użyteczna, jeśli pozbędziesz się pewnej liczby linii, ponieważ masz mniej miejsca na błędy. A najłatwiejszym sposobem na pozbycie się kodu jest pierwszy krok. Jest całkiem możliwe, że po prostu nie potrzebujesz wszystkich dzwonków i gwizdków, które próbujesz wdrożyć. Najszybszym sposobem na uproszczenie programu i zaoszczędzenie czasu jest nierobienie rzeczy, których nie powinno się robić. Drugi krok jest drugim co do wielkości potencjałem oszczędzania czasu. Jeśli mierzysz produktywność w kategoriach napisanych linijek, myślenie o tym, jak wykonać zadanie, sprawi, że będziesz mniej wydajne, ponieważ ten sam problem można rozwiązać przy użyciu mniejszej ilości kodu. Nie jestem w stanie podać tutaj dokładnych statystyk, ponieważ nie mam jak policzyć ilości linijek, których nie napisałem ze względu na to, że spędziłem czas nad specyfikacją, czyli nad pierwszym i drugim krokiem. I tu też nie da się ustawić eksperymentu, bo w eksperymencie nie mamy prawa wykonać pierwszego kroku, zadanie jest z góry ustalone.
W nieformalnych specyfikacjach łatwo przeoczyć wiele trudności. Nie ma nic trudnego w napisaniu ścisłych specyfikacji funkcji, nie będę tego omawiał. Zamiast tego porozmawiamy o napisaniu silnych specyfikacji dla standardowych zachowań. Istnieje twierdzenie, które mówi, że każdy zestaw zachowań można opisać za pomocą właściwości bezpieczeństwa (bezpieczeństwo) i właściwości przeżywalności (żywotność). Bezpieczeństwo oznacza, że nic złego się nie stanie, program nie poda błędnej odpowiedzi. Przeżywalność oznacza, że prędzej czy później wydarzy się coś dobrego, czyli program prędzej czy później poda poprawną odpowiedź. Z reguły bezpieczeństwo jest ważniejszym wskaźnikiem, tutaj najczęściej występują błędy. Dlatego, aby zaoszczędzić czas, nie będę mówić o przeżywalności, chociaż jest to oczywiście również ważne.
Osiągamy bezpieczeństwo, przepisując najpierw zbiór możliwych stanów początkowych. Po drugie, relacje ze wszystkimi możliwymi następnymi stanami dla każdego stanu. Zachowujmy się jak naukowcy i zdefiniujmy stany matematycznie. Zbiór stanów początkowych jest opisany wzorem, np. w przypadku algorytmu Euclid: (x = M) ∧ (y = N). Dla określonych wartości M и N jest tylko jeden stan początkowy. Relację ze stanem następnym opisuje wzór, w którym zmienne stanu następnego są zapisywane liczbą pierwszą, a zmienne stanu bieżącego są zapisywane bez liczby pierwszej. W przypadku algorytmu Euklidesa będziemy mieli do czynienia z dysjunkcją dwóch formuł, z których jedna x jest największą wartością, a w drugim - y:
W pierwszym przypadku nowa wartość y jest równa poprzedniej wartości y, a nową wartość x otrzymujemy odejmując mniejszą zmienną od większej. W drugim przypadku robimy odwrotnie.
Wróćmy do algorytmu Euklidesa. Załóżmy ponownie, że M = 12, N = 18. Definiuje to pojedynczy stan początkowy, (x = 12) ∧ (y = 18). Następnie podstawiamy te wartości do powyższego wzoru i otrzymujemy:
Oto jedyne możliwe rozwiązanie: x' = 18 - 12 ∧ y' = 12i otrzymujemy zachowanie: [x = 12, y = 18]. Podobnie możemy opisać wszystkie stany w naszym zachowaniu: [x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6].
W ostatnim stanie [x = 6, y = 6] obie części wyrażenia będą fałszywe, więc nie ma następnego stanu. Mamy więc pełną specyfikację drugiego kroku – jak widać, jest to całkiem zwyczajna matematyka, jak u inżynierów i naukowców, a nie dziwna, jak w informatyce.
Te dwie formuły można połączyć w jedną formułę logiki temporalnej. Jest elegancka i łatwa do wytłumaczenia, ale teraz nie ma na nią czasu. Możemy potrzebować logiki temporalnej tylko dla właściwości żywotności, nie jest ona potrzebna dla bezpieczeństwa. Nie lubię logiki temporalnej jako takiej, to nie do końca zwykła matematyka, ale w przypadku żywotności to zło konieczne.
W algorytmie Euklidesa dla każdej wartości x и y mają wyjątkowe walory x' и y', które sprawiają, że związek z następnym stanem jest prawdziwy. Innymi słowy, algorytm Euclida jest deterministyczny. Aby modelować algorytm niedeterministyczny, obecny stan musi mieć wiele możliwych przyszłych stanów, a każda nieprimowana wartość zmiennej ma wiele pierwotnych wartości zmiennych, tak aby relacja do następnego stanu była prawdziwa. Jest to łatwe do zrobienia, ale nie będę teraz podawać przykładów.
Aby stworzyć narzędzie robocze, potrzebujesz formalnej matematyki. Jak sformalizować specyfikację? Aby to zrobić, potrzebujemy formalnego języka, np. . Specyfikacja algorytmu Euclid wyglądałaby tak w tym języku:
Symbol znaku równości z trójkątem oznacza, że wartość po lewej stronie znaku jest zdefiniowana jako równa wartości po prawej stronie znaku. Zasadniczo specyfikacja jest definicją, w naszym przypadku dwiema definicjami. Do specyfikacji w TLA+ trzeba dodać deklaracje i trochę składni, jak na powyższym slajdzie. W ASCII wyglądałoby to tak:
Jak widać, nic skomplikowanego. Specyfikację dla TLA+ można przetestować, czyli ominąć wszystkie możliwe zachowania w małym modelu. W naszym przypadku tym modelem będą określone wartości M и N. Jest to bardzo wydajna i prosta metoda weryfikacji, która jest całkowicie automatyczna. Możliwe jest również pisanie formalnych dowodów prawdziwości i sprawdzanie ich mechanicznie, ale zajmuje to dużo czasu, więc prawie nikt tego nie robi.
Główną wadą TLA+ jest to, że jest to matematyka, a programiści i informatycy boją się matematyki. Na pierwszy rzut oka brzmi to jak żart, ale niestety mówię to z całą powagą. Mój kolega właśnie opowiadał mi, jak próbował wytłumaczyć TLA+ kilku programistom. Gdy tylko formuły pojawiły się na ekranie, natychmiast stały się szklistymi oczami. Więc jeśli TLA+ cię przeraża, możesz użyć , to rodzaj zabawkowego języka programowania. Wyrażenie w PlusCal może być dowolnym wyrażeniem TLA+, czyli ogólnie dowolnym wyrażeniem matematycznym. Ponadto PlusCal ma składnię dla algorytmów niedeterministycznych. Ponieważ PlusCal może napisać dowolne wyrażenie TLA+, PlusCal jest znacznie bardziej wyrazisty niż jakikolwiek prawdziwy język programowania. Następnie PlusCal jest kompilowany w czytelną specyfikację TLA+. Nie oznacza to oczywiście, że złożona specyfikacja PlusCal zamieni się w prostą na TLA+ - po prostu zgodność między nimi jest oczywista, dodatkowej złożoności nie będzie. Wreszcie, tę specyfikację można zweryfikować za pomocą narzędzi TLA+. Podsumowując, PlusCal może pomóc przezwyciężyć fobię matematyczną i jest łatwy do zrozumienia nawet dla programistów i informatyków. W przeszłości przez jakiś czas (około 10 lat) publikowałem na nim algorytmy.
Być może ktoś zarzuci, że TLA+ i PlusCal to matematyka, a matematyka działa tylko na wymyślonych przykładach. W praktyce potrzebny jest prawdziwy język z typami, procedurami, obiektami i tak dalej. To jest źle. Oto, co pisze Chris Newcomb, który pracował w Amazonie: „Użyliśmy TLA+ w dziesięciu dużych projektach i w każdym przypadku użycie jej miało znaczący wpływ na rozwój, ponieważ byliśmy w stanie wychwycić niebezpieczne błędy, zanim trafiliśmy do produkcji, oraz ponieważ dało nam to wgląd i pewność, których potrzebowaliśmy, aby dokonuj agresywnych optymalizacji wydajności bez wpływu na prawdziwość programu”. Często można usłyszeć, że używając metod formalnych otrzymujemy nieefektywny kod – w praktyce wszystko jest dokładnie na odwrót. Ponadto istnieje opinia, że menedżerów nie da się przekonać do potrzeby stosowania metod formalnych, nawet jeśli programiści są przekonani o ich przydatności. A Newcomb pisze: „Menedżerowie usilnie naciskają teraz, aby napisać specyfikacje dla TLA +, a konkretnie przeznaczyć na to czas”. Kiedy więc menedżerowie widzą, że TLA+ działa, chętnie to akceptują. Chris Newcomb napisał to jakieś pół roku temu (październik 2014), ale teraz, o ile mi wiadomo, TLA+ jest używane w 14 projektach, a nie w 10. Inny przykład dotyczy projektu Xboksa 360. Do Charlesa Thackera przyszedł stażysta i napisał specyfikację systemu pamięci. Dzięki tej specyfikacji znaleziono błąd, który w przeciwnym razie pozostałby niezauważony, przez co każdy XBox 360 ulegał awarii po czterech godzinach użytkowania. Inżynierowie IBM potwierdzili, że ich testy nie wykryłyby tego błędu.
Możesz przeczytać więcej o TLA + w Internecie, ale teraz porozmawiajmy o nieformalnych specyfikacjach. Rzadko musimy pisać programy, które obliczają najmniejszy wspólny dzielnik i tym podobne. Znacznie częściej piszemy programy takie jak narzędzie ładnej drukarki, które napisałem dla TLA+. Po najprostszym przetworzeniu kod TLA+ wyglądałby tak:
Ale w powyższym przykładzie użytkownik najprawdopodobniej chciał wyrównać koniunkcję i znaki równości. Poprawne formatowanie wyglądałoby więc mniej więcej tak:
Rozważ inny przykład:
Tutaj wręcz przeciwnie, wyrównanie znaków równości, dodawania i mnożenia w źródle było przypadkowe, więc wystarczy najprostsze przetwarzanie. Ogólnie rzecz biorąc, nie ma dokładnej matematycznej definicji poprawnego formatowania, ponieważ „poprawne” w tym przypadku oznacza „to, czego chce użytkownik”, a tego nie można określić matematycznie.
Wydawać by się mogło, że jeśli nie mamy definicji prawdy, to specyfikacja jest bezużyteczna. Ale to nie jest. To, że nie wiemy, co program ma robić, nie oznacza, że nie musimy myśleć o tym, jak on działa — wręcz przeciwnie, musimy włożyć w to jeszcze więcej wysiłku. Specyfikacja jest tutaj szczególnie ważna. Nie da się określić optymalnego programu do druku strukturalnego, ale to nie znaczy, że nie powinniśmy go w ogóle brać, a pisanie kodu jako strumienia świadomości nie jest dobrą rzeczą. W końcu napisałem specyfikację sześciu reguł wraz z definicjami w formie komentarzy w pliku javy. Oto przykład jednej z zasad: a left-comment token is LeftComment aligned with its covering token. Ta reguła jest zapisana, powiedzmy, matematycznym angielskim: LeftComment aligned, left-comment и covering token - terminy wraz z definicjami. Matematycy tak opisują matematykę: tworzą definicje terminów i na ich podstawie reguły. Zaletą takiej specyfikacji jest to, że sześć reguł jest znacznie łatwiejszych do zrozumienia i debugowania niż 850 linii kodu. Muszę powiedzieć, że napisanie tych reguł nie było łatwe, ich debugowanie zajęło sporo czasu. Specjalnie w tym celu napisałem kod informujący, która reguła została zastosowana. Dzięki temu, że przetestowałem te sześć reguł na kilku przykładach, nie musiałem debugować 850 linii kodu, a błędy okazały się dość łatwe do znalezienia. Java ma do tego świetne narzędzia. Gdybym tylko napisał kod, zajęłoby mi to znacznie więcej czasu, a formatowanie byłoby gorszej jakości.
Dlaczego nie można było użyć formalnej specyfikacji? Z jednej strony poprawne wykonanie nie jest tu zbyt ważne. Wydruki strukturalne na pewno nikomu nie przypadną do gustu, więc nie musiałem doprowadzać go do porządku we wszystkich dziwnych sytuacjach. Jeszcze ważniejszy jest fakt, że nie miałem odpowiednich narzędzi. Kontroler modelu TLA+ jest tutaj bezużyteczny, więc musiałbym ręcznie pisać przykłady.
Powyższa specyfikacja posiada cechy wspólne dla wszystkich specyfikacji. Jest wyższy niż kod. Może być zaimplementowany w dowolnym języku. Wszelkie narzędzia lub metody są bezużyteczne do jej napisania. Żaden kurs programowania nie pomoże Ci napisać takiej specyfikacji. I nie ma narzędzi, które mogłyby uczynić tę specyfikację zbędną, chyba że piszesz język specjalnie do pisania programów do drukowania strukturalnego w TLA+. Wreszcie, ta specyfikacja nie mówi nic o tym, jak dokładnie napiszemy kod, stwierdza tylko, co robi kod. Piszemy specyfikację, aby pomóc nam przemyśleć problem, zanim zaczniemy myśleć o kodzie.
Ale ta specyfikacja ma również cechy, które odróżniają ją od innych specyfikacji. 95% innych specyfikacji jest znacznie krótszych i prostszych:
Ponadto ta specyfikacja jest zbiorem zasad. Z reguły jest to oznaka złej specyfikacji. Zrozumienie konsekwencji zestawu reguł jest dość trudne, dlatego musiałem poświęcić dużo czasu na ich debugowanie. Jednak w tym przypadku nie mogłem znaleźć lepszego sposobu.
Warto powiedzieć kilka słów o programach, które działają w sposób ciągły. Z reguły działają równolegle, na przykład systemy operacyjne lub systemy rozproszone. Bardzo niewielu ludzi jest w stanie zrozumieć je mentalnie lub na papierze, a ja nie jestem jednym z nich, chociaż kiedyś mi się to udało. Dlatego potrzebujemy narzędzi, które sprawdzą naszą pracę – na przykład TLA+ czy PlusCal.
Po co było pisać specyfikację, skoro już wiedziałem, co dokładnie powinien robić kod? Właściwie, po prostu myślałem, że to wiem. Ponadto dzięki specyfikacji osoba z zewnątrz nie musi już zagłębiać się w kod, aby zrozumieć, co dokładnie robi. Mam zasadę: nie powinno być żadnych ogólnych zasad. Jest oczywiście wyjątek od tej reguły, jest to jedyna ogólna zasada, której się trzymam: specyfikacja tego, co robi kod, powinna powiedzieć ludziom wszystko, co powinni wiedzieć, kiedy go używają.
Co dokładnie programiści powinni wiedzieć o myśleniu? Na początek to samo, co wszyscy inni: jeśli nie piszesz, to tylko wydaje ci się, że myślisz. Ponadto musisz pomyśleć, zanim zaczniesz kodować, co oznacza, że musisz pisać, zanim zaczniesz kodować. Specyfikacja jest tym, co piszemy, zanim zaczniemy kodować. Specyfikacja jest potrzebna dla każdego kodu, który może być używany lub modyfikowany przez kogokolwiek. A tym „ktoś” może być sam autor kodu miesiąc po jego napisaniu. Specyfikacja jest potrzebna w przypadku dużych programów i systemów, klas, metod, a czasem nawet złożonych sekcji pojedynczej metody. Co dokładnie należy napisać o kodzie? Musisz opisać, co robi, czyli do czego może się przydać dowolnej osobie korzystającej z tego kodu. Czasami może być również konieczne określenie, w jaki sposób kod realizuje swój cel. Jeśli przeszliśmy przez tę metodę w trakcie algorytmów, nazywamy to algorytmem. Jeśli jest to coś bardziej wyjątkowego i nowego, nazywamy to projektowaniem na wysokim poziomie. Nie ma tu formalnej różnicy: oba są abstrakcyjnym modelem programu.
Jak dokładnie napisać specyfikację kodu? Najważniejsze: powinien być o jeden poziom wyższy niż sam kod. Powinien opisywać stany i zachowania. Powinien być tak rygorystyczny, jak wymaga tego zadanie. Jeśli piszesz specyfikację dotyczącą sposobu realizacji zadania, możesz napisać ją w pseudokodzie lub za pomocą PlusCal. Musisz nauczyć się pisać specyfikacje na formalnych specyfikacjach. To da ci niezbędne umiejętności, które pomogą ci również w nieformalnych. Jak nauczyć się pisać formalne specyfikacje? Kiedy nauczyliśmy się programować, pisaliśmy programy, a następnie je debugowaliśmy. Tutaj jest tak samo: napisz specyfikację, sprawdź ją w sprawdzaniu modeli i napraw błędy. TLA+ może nie być najlepszym językiem do formalnej specyfikacji, a inny język prawdopodobnie będzie lepszy dla Twoich konkretnych potrzeb. Zaletą TLA+ jest to, że bardzo dobrze uczy myślenia matematycznego.
Jak połączyć specyfikację i kod? Za pomocą komentarzy łączących koncepcje matematyczne i ich realizację. Jeśli pracujesz z wykresami, to na poziomie programu będziesz mieć tablice węzłów i tablice łączy. Dlatego musisz dokładnie napisać, w jaki sposób graf jest realizowany przez te struktury programistyczne.
Należy zauważyć, że żadne z powyższych nie dotyczy rzeczywistego procesu pisania kodu. Kiedy piszesz kod, czyli wykonujesz trzeci krok, musisz też przemyśleć i przemyśleć program. Jeśli podzadanie okaże się skomplikowane lub nieoczywiste, należy napisać dla niego specyfikację. Ale nie mówię tutaj o samym kodzie. Możesz użyć dowolnego języka programowania, dowolnej metodologii, nie chodzi o nie. Ponadto żadne z powyższych nie eliminuje potrzeby testowania i debugowania kodu. Nawet jeśli model abstrakcyjny jest napisany poprawnie, mogą wystąpić błędy w jego implementacji.
Pisanie specyfikacji jest dodatkowym krokiem w procesie kodowania. Dzięki niemu wiele błędów można wychwycić mniejszym wysiłkiem – wiemy to z doświadczenia programistów z Amazona. Wraz ze specyfikacjami jakość programów staje się wyższa. Dlaczego więc tak często chodzimy bez nich? Bo pisanie jest trudne. A pisanie jest trudne, bo do tego trzeba myśleć, a myślenie też jest trudne. Zawsze łatwiej jest udawać to, co się myśli. Tutaj możesz narysować analogię do biegania - im mniej biegasz, tym wolniej biegasz. Musisz ćwiczyć mięśnie i ćwiczyć pisanie. Potrzebujesz praktyki.
Specyfikacja może być błędna. Być może popełniłeś gdzieś błąd, wymagania mogły się zmienić lub konieczne może być wprowadzenie ulepszeń. Każdy kod, którego ktoś używa, musi zostać zmieniony, więc wcześniej czy później specyfikacja nie będzie już pasować do programu. Idealnie w takim przypadku musisz napisać nową specyfikację i całkowicie przepisać kod. Doskonale wiemy, że nikt tego nie robi. W praktyce łatamy kod i ewentualnie aktualizujemy specyfikację. Jeśli prędzej czy później tak się stanie, to po co w ogóle pisać specyfikacje? Po pierwsze, dla osoby, która będzie edytować Twój kod, każde dodatkowe słowo w specyfikacji będzie na wagę złota, a tą osobą możesz być Ty sam. Często obwiniam się za to, że nie otrzymałem wystarczającej specyfikacji podczas edytowania kodu. I piszę więcej specyfikacji niż kodu. Dlatego podczas edycji kodu specyfikacja zawsze wymaga aktualizacji. Po drugie, z każdą poprawką kod się pogarsza, staje się coraz trudniejszy do odczytania i utrzymania. Jest to wzrost entropii. Ale jeśli nie zaczniesz od specyfikacji, każda napisana linia będzie edycją, a kod będzie nieporęczny i trudny do odczytania od samego początku.
Jak zostało powiedziane , żadnej bitwy nie wygrywa się planem i żadnej bitwy nie wygrywa się bez planu. I wiedział co nieco o bitwach. Panuje opinia, że pisanie specyfikacji to strata czasu. Czasami to prawda, a zadanie jest tak proste, że nie ma co się nad nim zastanawiać. Ale zawsze powinieneś pamiętać, że kiedy mówi się ci, żebyś nie pisał specyfikacji, mówi się ci, żebyś nie myślał. I warto o tym myśleć za każdym razem. Przemyślenie zadania nie gwarantuje, że nie popełnisz błędów. Jak wiemy, czarodziejskiej różdżki nikt nie wynalazł, a programowanie to trudne zadanie. Ale jeśli nie przemyślisz problemu, masz gwarancję, że popełnisz błędy.
Więcej o TLA+ i PlusCal można przeczytać na specjalnej stronie internetowej, można tam wejść z mojej strony domowej . To wszystko z mojej strony, dziękuję za uwagę.
Proszę zauważyć, że jest to tłumaczenie. Pisząc komentarze pamiętaj, że autor ich nie przeczyta. Jeśli naprawdę chcesz porozmawiać z autorem, to będzie on na konferencji Hydra 2019, która odbędzie się 11-12 lipca 2019 r. W Petersburgu. Bilety można kupić .
Źródło: www.habr.com