To jest artykuł-przekład . Ale przed tym krótkie wprowadzenie. Jak powstają zombie? Każdy z nas znalazł się w sytuacji, gdy chciałby pociągnąć przyjaciela lub kolegę na swój poziom, a to się nie udaje. Przy czym „nie udaje się” nie dotyczy tyle ciebie, co jego: na jednej szali znajduje się normalna pensja, zadania itd., a na drugiej — konieczność myślenia. Myślenie jest nieprzyjemne i bolesne. On szybko się poddaje i dalej pisze kod, zupełnie nie angażując mózgu. Wyobrażasz sobie, ile energii trzeba włożyć, aby pokonać barierę wyuczonej bezradności, i po prostu tego nie robisz. Tak powstają zombie, których można by uzdrowić, ale nikt się tym nie zajmie.
Kiedy zobaczyłem, że (tak, ten sam gość z podręczników) i robi nie wykład, a sesję pytań i odpowiedzi, trochę się zaniepokoiłem. Na wszelki wypadek, Leslie to światowej sławy naukowiec, autor fundamentalnych prac w dziedzinie obliczeń rozproszonych, a także możesz go znać z liter La w słowie LaTeX — „Lamport TeX”. Drugim czynnikiem niepokojącym jest jego żądanie: każdy, kto przyjdzie, musi (zupełnie za darmo) wcześniej wysłuchać kilku jego wykładów, wymyślić do nich przynajmniej jedno pytanie i dopiero wtedy przyjść. Postanowiłem sprawdzić, co Lamport głosi — i to jest wspaniałe! To jest dokładnie to, magiczny link-tablet na wyleczenie z zombie. Ostrzegam: tekst może mocno zdenerwować miłośników super-elastycznych metodologii i niechętnych do testowania napisanego.
Po hubrockcie, w zasadzie, zaczyna się tłumaczenie seminarium. Miłej lektury!
Jakiekolwiek zadanie nie podejmujesz, zawsze musisz przejść przez trzy kroki:
- określić, jaki cel chcesz osiągnąć;
- zdecydować, jak dokładnie będziesz dążyć do celu;
- osiągnąć swój cel.
Dotyczy to również programowania. Kiedy piszemy kod, musimy:
- zdecydować, co dokładnie powinna robić program;
- określić, jak dokładnie powinna wykonywać swoje zadanie;
- napisać odpowiedni kod.
Ostatni krok jest oczywiście bardzo ważny, ale dzisiaj o nim nie będę mówić. Zamiast tego omówimy pierwsze dwa. Każdy programista musi je wykonać, zanim zacznie pracować. Nie siadasz do pisania, jeśli nie wiesz, co dokładnie piszesz: przeglądarka czy baza danych. Musisz mieć wyraźne pojęcie o celu. I zawsze musisz przemyśleć, co konkretnie będzie robić program, a nie pisać na oślep, mając nadzieję, że kod jakoś zamieni się w przeglądarkę.
Jak dokładnie odbywa się to wstępne przemyślenie kodu? Ile wysiłku powinniśmy na to poświęcić? To wszystko zależy od tego, jak skomplikowany problem rozwiązujemy. Załóżmy, że chcemy napisać odporny na awarie system rozproszony. W takim przypadku musimy dokładnie przemyśleć wszystko, zanim usiądziemy do kodu. A jeśli po prostu musimy zwiększyć zmienną całkowitą o 1? Na pierwszy rzut oka wszystko wydaje się trywialne i nie potrzebujemy żadnych przemyśleń, ale potem przypominamy sobie, że może nastąpić przepełnienie. Dlatego nawet aby zrozumieć, czy problem jest prosty, czy skomplikowany — należy najpierw pomyśleć.
Jeśli wcześniej przemyślisz możliwe rozwiązania problemu, możesz uniknąć błędów. Ale aby to zrobić, twoje myślenie musi być jasne. Aby to osiągnąć, musisz zapisać swoje myśli. Bardzo lubię cytat Dika Gindona: „Kiedy piszesz, natura pokazuje ci, jak chaotyczne jest twoje myślenie”. Jeśli nie piszesz, tylko wydaje ci się, że myślisz. A myśli należy zapisywać w formie specyfikacji.
Specyfikacje pełnią wiele funkcji, szczególnie w dużych projektach. Ale ja będę mówić tylko o jednej z nich: pomagają nam myśleć jasno. Jasne myślenie jest bardzo ważne i dość trudne, dlatego potrzebujemy tu jakiejkolwiek pomocy. W jakim języku powinniśmy pisać specyfikacje? To zawsze pierwsze pytanie dla programistów: w jakim języku będziemy pisać. Nie ma jednej poprawnej odpowiedzi na nie: problemy, które rozwiązujemy, są zbyt różnorodne. Dla niektórych przydatny jest TLA+ — to język specyfikacji, który opracowałem. Dla innych wygodniej jest posługiwać się chińskim. Wszystko zależy od sytuacji.
Inny, ważniejszy temat brzmi: jak osiągnąć jaśniejsze myślenie? Odpowiedź: musimy myśleć jak naukowcy. To sposób myślenia, który doskonale sprawdził się w ciągu ostatnich 500 lat. W nauce tworzymy modele matematyczne rzeczywistości. Astronomia była prawdopodobnie pierwszą nauką w ścisłym tego słowa znaczeniu. W matematycznym modelu używanym w astronomii ciała niebieskie przedstawione są jako punkty z masą, położeniem i pędem, choć w rzeczywistości są to niezwykle skomplikowane obiekty z górami i oceanami, przypływami i odpływami. Ten model, podobnie jak każdy inny, stworzony jest w celu rozwiązania określonych problemów. Doskonale nadaje się do określenia kierunku, w którym należy skierować teleskop, jeśli trzeba 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. Nauka zaś pokazuje, jak te właściwości mają się do rzeczywistości. Porozmawiajmy o naszej nauce, komputerowej. Rzeczywistość, z którą pracujemy, to różnorodne systemy obliczeniowe: procesory, konsole do gier, komputery wykonujące programy i tak dalej. Będę mówił o wykonywaniu programu na komputerze, ale w dużej mierze wszystkie te wnioski mają zastosowanie do każdego systemu obliczeniowego. W naszej nauce używamy wielu różnych modeli: maszyna Turinga, częściowo uporządkowane zbiory zdarzeń i wiele innych.
Czym jest program? To każdy kod, który można rozpatrywać samodzielnie. Załóżmy, że musimy napisać przeglądarkę. Wykonujemy trzy zadania: projektujemy interfejs programu dla użytkownika, następnie piszemy wysokopoziomowy schemat programu, a na koniec piszemy kod. W trakcie pisania kodu rozumiemy, że musimy stworzyć narzędzie do formatowania tekstu. Tutaj znów musimy rozwiązać trzy zadania: określić, jaki tekst to narzędzie będzie zwracać; wybrać algorytm do formatowania; napisać kod. To zadanie ma swoją podzadanie: prawidłowe wstawianie dywizu w słowach. Tę podzadanie również rozwiązujemy w trzech krokach — jak widać, powtarzają się one na wielu poziomach.
Przyjrzyjmy się dokładniej pierwszemu krokowi: jakie zadanie rozwiązuje program. Tutaj najczęściej modelujemy program jako funkcję, która otrzymuje pewne dane wejściowe i zwraca pewne dane wyjściowe. W matematyce funkcja zazwyczaj opisywana jest jako uporządkowany zbiór par. Na przykład, funkcja podnoszenia do kwadratu dla liczb naturalnych opisywana jest jako zbiór {, , , , …}. Zakres definiujący taką funkcję to zbiór pierwszych elementów każdej pary, czyli liczby naturalne. Aby zdefiniować funkcję, musimy określić jej zakres definiujący oraz wzór.
Ale funkcje w matematyce to nie to samo co funkcje w językach programowania. Matematyka jest znacznie prostsza. Ponieważ nie mam czasu na złożone przykłady, rozważmy prosty: funkcja w języku C lub statyczna metoda 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 i N, gdzie GCD(M,N) — funkcja, której zakres definiujący to zbiór par liczb całkowitych, a wartość zwracana to największa liczba całkowita, przez którą dzieli się M i N. Jak ta model odnosi się do rzeczywistości? Model operuje liczbami całkowitymi, a w C lub Javie mamy 32-bitowy int. Ten model pozwala nam rozwiązać, czy algorytm jest poprawny GCD, ale nie zapobiega błędom przepełnienia. Aby to zrobić, potrzebny byłby bardziej skomplikowany model, na co nie ma czasu.
Porozmawiajmy o ograniczeniach funkcji jako modelu. Działanie niektórych programów (na przykład systemów operacyjnych) nie sprowadza się do zwracania określonej wartości dla określonych argumentów, mogą one działać nieprzerwanie. Ponadto, funkcja jako model słabo nadaje się do drugiego kroku: planowania sposobu rozwiązania zadania. Szybkie sortowanie i sortowanie bąbelkowe obliczają tę samą funkcję, ale to całkowicie różne algorytmy. Dlatego do opisania sposobu osiągnięcia celu programu użyję innego modelu, nazwijmy go standardowy model zachowania. Program w nim przedstawiony jest jako zbiór wszystkich dozwolonych zachowań, z których każde z kolei jest sekwencją stanów, a stan to przypisanie wartości zmiennym.
Zobaczmy, jak będzie wyglądać drugi krok algorytmu Euklidesa. Musimy obliczyć NWD(M, N). Inicjujemy M jak x, a N jak y, a następnie powtarzamy odejmowanie mniejszej z tych zmiennych od większej, aż będą równe. Na przykład, jeśli M = 12, a 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 i N = 0? Ноль делится на все числа, поэтому наибольшего делителя в этом случае нет. В этой ситуации нам нужно вернуться к первому шагу и спросить: действительно ли нам нужно вычислять НОД для неположительных чисел? Если в этом нет необходимости, то нужно просто изменить спецификацию.
Tutaj należy zrobić mały dygresję na temat produktywności. Często mierzy się ją liczbą linii kodu napisanych w ciągu dnia. Jednak twoja praca jest znacznie bardziej wartościowa, jeśli udało ci się zredukować pewną liczbę linii, ponieważ miało to wpływ na zmniejszenie miejsca na błędy. Najłatwiej jest eliminować kod na pierwszym kroku. Może się okazać, że nie potrzebujesz wszystkich tych złożoności, które próbujesz wdrożyć. Najszybszy sposób na uproszczenie programu i oszczędność czasu to nie robić rzeczy, których nie warto robić. Drugi krok jest na drugim miejscu pod względem potencjału oszczędności czasu. Jeśli mierzysz produktywność według liczby napisanych linii, to przemyślenie sposobu wykonania zadania sprawi, że będziesz mniej produktywny, ponieważ będziesz w stanie rozwiązać to samo zadanie mniejszą ilością kodu. Nie mogę podać dokładnej statystyki, ponieważ nie mam sposobu na policzenie liczby linii, których nie napisałem, dzięki temu, że poświęciłem czas na specyfikację, czyli na pierwszy i drugi krok. Eksperymentów również nie można tu przeprowadzić, ponieważ w eksperymencie nie mamy prawa wykonać pierwszego kroku, zadanie jest z góry określone.
W nieformalnych specyfikacjach łatwo jest pominąć wiele trudności. Nie ma nic trudnego w pisaniu ścisłych specyfikacji funkcji, o tym nie będę dyskutować. Zamiast tego porozmawiamy o pisaniu ścisłych specyfikacji dla standardowych modeli zachowań. Jest twierdzenie, że każde zbiorowisko zachowań można opisać za pomocą właściwości bezpieczeństwa (safety) i właściwości żywotności (liveness). Bezpieczeństwo oznacza, że nic złego się nie wydarzy, program nie poda błędnej odpowiedzi. Odporność oznacza, że prędzej czy później wydarzy się coś dobrego, tzn. program w końcu poda poprawną odpowiedź. Zazwyczaj bezpieczeństwo jest ważniejszym wskaźnikiem, błędy najczęściej występują właśnie tutaj. Dlatego dla zaoszczędzenia czasu nie będę mówić o odporności, chociaż to również jest ważne.
Osiągamy bezpieczeństwo, zapisując, po pierwsze, wiele możliwych stanów początkowych. A, po drugie, relacje ze wszystkimi możliwymi następnymi stanami dla każdego stanu. Będziemy zachowywać się jak naukowcy i określimy stany matematycznie. Zbiór stanów początkowych opisuje wzór, na przykład w przypadku algorytmu Euklidesa: (x = M) ∧ (y = N). Dla określonych wartości M i N istnieje tylko jeden stan początkowy. Relacja z następnym stanem opisana jest wzorem, w którym zmienne następnego stanu zapisane są z kreską, a bieżącego stanu — bez kreski. W przypadku algorytmu Euklidesa będziemy mieć do czynienia z dysjunkcją dwóch wzorów, w jednym z nich x jest największą wartością, a w drugim — y:
W pierwszym przypadku nowa wartość y równa jest poprzedniej wartości y, a nową wartość x uzyskujemy, odejmując od większej zmiennej mniejszą. W drugim przypadku robimy odwrotnie.
Wracając do algorytmu Euklidesa, załóżmy ponownie, że M = 12, N = 18. To definiuje jedyny stan początkowy, (x = 12) ∧ (y = 18). Następnie podstawiamy te wartości do powyższego wzoru i otrzymujemy:
Tutaj jedynym możliwym rozwiązaniem jest: x' = 18 - 12 ∧ y' = 12, i otrzymujemy zachowanie: [x = 12, y = 18]. W ten sam sposób 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, w związku z tym nie ma kolejnego stanu. Tak więc mamy pełną specyfikację drugiego kroku — jak widać, to całkiem zwyczajna matematyka, jak u inżynierów i naukowców, a nie dziwaczna, jak w informatyce.
Te dwie formuły można połączyć w jedną formułę logiki temporalnej. Jest ona elegancka i łatwo ją wyjaśnić, ale teraz nie mamy na to czasu. Logika temporalna może być nam potrzebna tylko do właściwości żywotności, dla bezpieczeństwa nie jest potrzebna. Sama logika temporalna nie jest dla mnie atrakcyjna, to nie do końca zwykła matematyka, ale w przypadku żywotności jest to konieczne zło.
W algorytmie Euklidesa dla każdej wartości x i y istnieją unikalne wartości x' i y', które sprawiają, że relacja z następnym stanem jest prawdziwa. Innymi słowy, algorytm Euklidesa jest deterministyczny. Aby modelować algorytm niedeterministyczny, musimy mieć kilka możliwych przyszłych stanów dla aktualnego stanu, a każde nieoznakowane wartości zmiennej musi mieć kilka wartości zmiennej oznaczonej, przy których relacja z następnym stanem jest prawdziwa. To nie jest trudne do zrobienia, ale teraz nie będę podawać przykładów.
Aby stworzyć działające narzędzie, potrzebna jest matematyka formalna. Jak sformułować specyfikację formalną? Potrzebujemy formalnego języka, na przykład, . Specyfikacja algorytmu Euklidesa w tym języku będzie wyglądać następująco:
Symbol znaku równości z trójkątem oznacza, że wartość po lewej stronie znaku jest określona jako równa wartości po prawej stronie znaku. W istocie specyfikacja to definicja, w naszym przypadku dwa definicje. Do specyfikacji w TLA+ należy dodać deklaracje i pewną składnię, jak na slajdzie powyżej. W ASCII będzie to wyglądać tak:
Jak widzimy, nic skomplikowanego. Specyfikację w TLA+ można zweryfikować, tzn. przejść przez wszystkie możliwe zachowania w małym modelu. W naszym przypadku tym modelem będą określone wartości M i N. To bardzo efektywny i prosty sposób weryfikacji, który w całości odbywa się automatycznie. Ponadto można napisać formalne dowody prawdziwości i zweryfikować je mechanicznie, ale wymaga to dużo czasu, dlatego prawie nikt tego nie robi.
Główną wadą TLA+ jest to, że to matematyka, a programiści i informatycy boją się matematyki. Na pierwszy rzut oka może to brzmieć jak żart, ale, niestety, mówię to całkiem serio. Mój kolega właśnie opowiadał mi, jak próbował wyjaśnić TLA+ kilku deweloperom. Gdy tylko na ekranie pojawiły się formuły, ich oczy od razu stały się szklane. Więc jeśli TLA+ przeraża, można użyć , jest to rodzaj zabawkowego języka programowania. Wyrażenie w PlusCal może być dowolnym wyrażeniem TLA+, a więc w zasadzie każdym wyrażeniem matematycznym. Ponadto, w PlusCal istnieje składnia dla niedeterministycznych algorytmów. Dzięki temu, że w PlusCal można zapisać każde wyrażenie TLA+, jest on znacznie bardziej wyrazisty niż jakikolwiek rzeczywisty język programowania. Następnie, PlusCal kompiluje się do łatwej do przeczytania specyfikacji TLA+. Oczywiście nie oznacza to, że skomplikowana specyfikacja PlusCal zamieni się w prostą specyfikację TLA+ — po prostu zgodność między nimi jest oczywista, nie pojawi się dodatkowa złożoność. W końcu tę specyfikację można będzie sprawdzić narzędziami TLA+. W skrócie, PlusCal może pomóc przezwyciężyć fobię matematyczną, jest łatwy do zrozumienia nawet dla programistów i informatyków. W przeszłości przez jakiś czas (około 10 lat) publikowałem w nim algorytmy.
Możliwe, że ktoś zarzuci, że TLA+ i PlusCal to matematyka, a matematyka działa tylko na wymyślonych przykładach. W praktyce jednak potrzebny jest rzeczywisty język z typami, procedurami, obiektami itd. To nieprawda. Oto, co pisze Chris Newcombe, który pracował w Amazonie: „Używaliśmy TLA+ w dziesięciu dużych projektach, a w każdym przypadku jego wykorzystanie znacznie przyczyniło się do rozwoju, ponieważ udało nam się wyłapać niebezpieczne błędy przed wdrożeniem do produkcji oraz ponieważ dał nam zrozumienie i pewność potrzebne do agresywnych optymalizacji wydajności, które nie wpływają na poprawność programu.”. Często można usłyszeć, że przy użyciu formalnych metod otrzymujemy nieefektywny kod — w praktyce jest wręcz przeciwnie. Ponadto panuje przekonanie, że nie można przekonać menedżerów do konieczności formalnych metod, nawet jeśli programiści są przekonani o ich przydatności. A Newcombe pisze: „Menadżerowie teraz wszelkimi sposobami zachęcają do pisania specyfikacji w TLA+, celowo przeznaczając na to czas“. Kiedy menadżerowie widzą, że TLA+ działa, chętnie go wdrażają. Chris Newcomb napisał to około sześciu miesięcy temu (w październiku 2014 roku), a teraz, o ile mi wiadomo, TLA+ jest używane w 14 projektach, a nie w 10. Inny przykład dotyczy projektowania Xbox 360. Do Charlesa Teckera przyszedł stażysta i napisał specyfikację dla systemu pamięci. Dzięki tej specyfikacji znaleziono błąd, który w przeciwnym razie zostałby przeoczony, a przez który każda Xbox 360 zawieszałaby się po czterech godzinach użytkowania. Inżynierowie z IBM potwierdzili, że ich testy nie wykryłyby tego błędu.
Bardziej szczegółowo na temat TLA+ można poczytać w Internecie, a teraz porozmawiajmy o nieformalnych specyfikacjach. Rzadko piszemy programy, które obliczają największy wspólny dzielnik i tym podobne. Znacznie częściej piszemy programy typu narzędzie do formatowania strukturalnego (pretty-printer), które stworzyłem dla TLA+. Po najmniej skomplikowanej obróbce kod w TLA+ wyglądałby następująco:
Jednak w podanym przykładzie użytkownik prawdopodobnie chciał, aby znaki koniunkcji i równości były wyrównane. A więc poprawne formatowanie wyglądałoby raczej tak:
Rozważmy inny przykład:
Tutaj, przeciwnie, wyrównanie znaków równości, dodawania i mnożenia w źródle było przypadkowe, więc najprostsza obróbka jest wystarczająca. Ogólnie rzecz biorąc, nie ma dokładnej matematycznej definicji poprawnego formatowania, ponieważ „poprawne“ w tym przypadku oznacza „takie, jakie chce użytkownik”, a tego nie można matematycznie określić.
Wydawałoby się, że jeśli nie mamy definicji prawdziwości, to specyfikacja jest bezużyteczna. Ale to nieprawda. Jeśli nie wiemy, co dokładnie program ma robić, to nie znaczy, że nie musimy przemyśleć jego działania — wręcz przeciwnie, powinniśmy poświęcić na to jeszcze więcej wysiłku. Specyfikacja jest tutaj szczególnie ważna. Określenie optymalnego programu do formatowania strukturalnego jest niemożliwe, ale to nie znaczy, że nie powinniśmy się za to zabierać w ogóle, a pisanie kodu w formie strumienia świadomości — to nie jest właściwe. Ostatecznie napisałem specyfikację z sześcioma zasadami z definicjami w formie komentarzy w pliku Java. Oto przykład jednej z zasad: token komentarza lewego to LeftComment, który jest zgodny z jego tokenem pokrywającym. Ta zasada jest napisana w, powiedzmy, matematycznym angielskim: LeftComment zgodny, komentarz lewy i token pokrywający — terminy z definicjami. Tak matematycy opisują matematykę: piszą definicje terminów i na ich podstawie — zasady. Korzyść z takiej specyfikacji polega na tym, że zrozumienie i debugowanie sześciu zasad jest znacznie łatwiejsze niż 850 linii kodu. Muszę powiedzieć, że napisanie tych zasad nie było proste, zajęło mi sporo czasu na ich debugowanie. Specjalnie w tym celu napisałem kod, który informował, która zasada jest używana. Dzięki temu, że przetestowałem te sześć zasad na kilku przykładach, nie musiałem debugować 850 linii kodu, a błędy okazały się dość łatwe do znalezienia. W Javie są do tego świetne narzędzia. Gdybym po prostu napisał ten kod, zajęłoby mi to znacznie więcej czasu, a formatowanie byłoby gorszej jakości.
Dlaczego nie mogłem użyć formalnej specyfikacji? Z jednej strony, poprawność wykonania nie jest tutaj zbyt ważna. Strukturalne drukowanie na pewno komuś nie przypadnie do gustu, więc nie musiałem dążyć do poprawnej pracy we wszystkich nietypowych sytuacjach. Jeszcze ważniejsze jest to, że nie miałem odpowiednich narzędzi. Narzędzie do weryfikacji modeli TLA+ tutaj jest bezużyteczne, więc musiałbym ręcznie pisać przykłady.
Podana specyfikacja ma cechy wspólne dla wszystkich specyfikacji. Jest to poziom wyższy niż kod. Można ją zrealizować w dowolnym języku. Do jej pisania nie są potrzebne żadne narzędzia ani metody. Żadny kurs programowania nie pomoże Ci napisać tej specyfikacji. I nie ma narzędzi, które mogłyby uczynić tę specyfikację zbędną, o ile nie piszesz języka specjalnie do tworzenia programów dla strukturalnego drukowania w TLA+. W końcu ta specyfikacja nic nie mówi o tym, jak dokładnie będziemy pisać kod, tylko wskazuje, co ten kod robi. Pisujemy specyfikację, aby pomóc sobie 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:
Dalej, ta specyfikacja to zestaw zasad. Z reguły jest to oznaka słabej specyfikacji. Zrozumienie konsekwencji zestawu reguł jest dość trudne, dlatego musiałem poświęcić dużo czasu na ich debugowanie. Niemniej jednak, w tym przypadku nie znalazłem lepszego sposobu.
Warto powiedzieć kilka słów o programach, które działają nieprzerwanie. Z reguły działają one równolegle, na przykład systemy operacyjne lub systemy rozproszone. Niewielu potrafi je zrozumieć w głowie lub na papierze, a ja do tej grupy nie należę, chociaż kiedyś mi to wychodziło. Dlatego potrzebne są narzędzia, które będą weryfikować naszą pracę — na przykład TLA+ lub PlusCal.
Po co było pisać specyfikację, skoro i tak wiedziałem, co dokładnie kod powinien robić? Tak naprawdę tylko wydawało mi się, że to wiem. Ponadto, mając specyfikację, obca osoba nie musi już zaglądać do kodu, aby zrozumieć, co on robi. Mam zasadę: nie powinno być żadnych ogólnych zasad. Ta zasada ma oczywiście wyjątek — to jedyna ogólna zasada, której przestrzegam: specyfikacja tego, co robi kod, powinna przekazywać ludziom wszystko, co muszą wiedzieć, korzystając z tego kodu.
Czego dokładnie programiści muszą wiedzieć o myśleniu? Przede wszystkim tego samego, co wszyscy: jeśli nie piszesz, tylko ci się wydaje, że myślisz. Ponadto, trzeba myśleć przed kodowaniem, a to oznacza, że trzeba pisać przed kodowaniem. Specyfikacja to to, co piszemy przed rozpoczęciem kodowania. Specyfikacja jest potrzebna dla każdego kodu, który może być używany lub zmieniany przez kogokolwiek. A tym „kogokolwiek” może być sam autor kodu miesiąc po jego napisaniu. Specyfikacja jest potrzebna dla dużych programów i systemów, dla klas, dla metod, a czasami nawet dla skomplikowanych fragmentów pojedynczej metody. Co dokładnie należy napisać o kodzie? Należy opisać, co on robi, czyli to, co może być przydatne każdemu, kto korzysta z tego kodu. Czasami może być również konieczne wskazanie, jak dokładnie kod osiąga swój cel. Jeśli ten sposób omawialiśmy na kursie algorytmów, nazywamy to algorytmem. Jeśli jest to coś bardziej specyficznego i nowego, nazywamy to projektowaniem na wysokim poziomie. Formalne różnice tutaj nie ma: zarówno to, jak i to jest abstrakcyjnym modelem programu.
Jak dokładnie należy pisać specyfikację kodu? Najważniejsze: powinna być na wyższym poziomie niż sam kod. Powinna opisywać stany i zachowania. Powinna być tak rygorystyczna, jak wymaga tego zadanie. Jeśli piszesz specyfikację sposobu realizacji zadania, można ją napisać w pseudokodzie lub z użyciem PlusCal. Należy uczyć się pisania specyfikacji na formalnych specyfikacjach. To da ci niezbędne umiejętności, które pomogą również w tworzeniu specyfikacji nieformalnych. A jak nauczyć się pisać formalne specyfikacje? Kiedy uczyliśmy się programowania, pisaliśmy programy, a następnie je debugowaliśmy. To samo dotyczy tego procesu: należy napisać specyfikację, sprawdzić ją za pomocą narzędzia do weryfikacji modeli i poprawić błędy. TLA+ może nie być najlepszym językiem do formalnych specyfikacji, a dla twoich konkretnych potrzeb prawdopodobnie lepszy będzie inny język. Zaletą TLA+ jest to, że doskonale uczy matematycznego myślenia.
Jak powiązać specyfikację z kodem? Za pomocą komentarzy, które łączą pojęcia matematyczne z ich realizacją. Jeśli pracujesz z grafami, to na poziomie programu będziesz mieć tablice węzłów i tablice połączeń. Dlatego musisz napisać, jak dokładnie graf jest realizowany za pomocą tych struktur programowania.
Należy zauważyć, że nic z powyższego nie odnosi się do samego procesu pisania kodu. Kiedy piszesz kod, czyli wykonujesz trzeci krok, również musisz myśleć i zaplanować program. Jeśli podzadanie okazuje się trudne lub niejasne, trzeba napisać dla niego specyfikację. Ale o samym kodzie tutaj nie mówię. Możesz korzystać z dowolnego języka programowania, dowolnej metodologii, nie o tym tutaj mowa. Ponadto nic z powyższego nie zwalnia z konieczności testowania i debugowania kodu. Nawet jeśli abstrakcyjny model jest poprawnie napisany, w jego realizacji mogą wystąpić błędy.
Pisywanie specyfikacji to dodatkowy etap w procesie pisania kodu. Dzięki niemu wiele błędów można wychwycić mniejszymi siłami – wiemy to z doświadczenia programistów z Amazon. Dzięki specyfikacjom jakość programów wzrasta. Dlaczego więc tak często radzimy sobie bez nich? Ponieważ pisanie jest trudne. A pisanie jest trudne, ponieważ wymaga myślenia, a myślenie też jest trudne. Zawsze łatwiej udawać, że się myśli. Można tu przeprowadzić analogię z bieganiem – im mniej biegasz, tym wolniej biegasz. Musisz trenować swoje mięśnie i ćwiczyć pisanie. Potrzebna jest praktyka.
Specyfikacja może być błędna. Możesz gdzieś popełnić błąd, wymagania mogły się zmienić lub zaszła potrzeba wprowadzenia ulepszeń. Każdy kod, z którego ktoś korzysta, trzeba zmieniać, więc prędzej czy później specyfikacja przestanie odpowiadać programowi. W idealnym przypadku należałoby napisać nową specyfikację i całkowicie przepisać kod. Doskonale wiemy, że nikt tak nie robi. W praktyce łatamy kod i być może aktualizujemy specyfikację. Jeśli to musi się zdarzyć prędzej czy później, to po co w ogóle pisać specyfikacje? Po pierwsze, dla osoby, która będzie poprawiać twój kod, każde zbędne słowo w specyfikacji będzie na wagę złota, a tą osobą możesz być ty sam. Często ganię siebie za niewystarczającą specyfikację, gdy poprawiam swój kod. A piszę więcej specyfikacji niż kodu. Dlatego, gdy poprawiasz kod, zawsze należy aktualizować specyfikację. Po drugie, z każdą poprawką kod staje się gorszy, trudniejszy do czytania i utrzymania. To narastanie entropii. Ale jeśli nie zaczynasz od specyfikacji, to każda napisana linia będzie poprawką, a kod od samego początku będzie nieporęczny i trudny do odczytania.
Jak mówił , żadna bitwa nie została wygrana zgodnie z planem, a żadna bitwa nie została wygrana bez planu. A on wiedział coś o bitwach. Istnieje przekonanie, że pisanie specyfikacji to strata czasu. Czasami tak właśnie jest, a zadanie jest na tyle proste, że nie ma o czym myśleć. Ale zawsze trzeba pamiętać, że gdy radzą ci nie pisać specyfikacji, to znaczy, że radzą ci nie myśleć. I o tym za każdym razem należy pomyśleć. Przemyślenie zadania nie gwarantuje, że nie popełnisz błędów. Jak wiemy, nikt nie wynalazł magicznej różdżki, a programowanie to skomplikowane zajęcie. Ale jeśli nie przemyślisz zadania, to na pewno popełnisz błędy.
Więcej o TLA+ i PlusCal można przeczytać na specjalnej stronie, którą można odwiedzić z mojej strony domowej . Na tym kończę, dziękuję za uwagę.
Przypominam, że to jest tłumaczenie. Kiedy będziecie pisać komentarze — pamiętajcie, że autor ich nie przeczyta. Jeśli naprawdę chcecie porozmawiać z autorem, to będzie on na konferencji Hydra 2019, która odbędzie się w dniach 11-12 lipca 2019 roku w Sankt Petersburgu. Bilety można zakupić. .
Źródło: habr.com
