Ovo je prijevod članka . No prethodi mu malo uvoda. Kako nastaju zombiji? Svi smo se našli u situaciji kada želimo podići prijatelja ili kolegu na svoju razinu, a ne ide. A zapravo, „ne ide“ ne toliko zbog tebe, koliko zbog njega: na jednoj strani su normalna plaća, zadaci i tako dalje, a na drugoj - potreba za razmišljanjem. Razmišljanje je neugodno i bolno. Brzo odustaje i nastavlja pisati kod bez uključivanja mozga. Možeš zamisliti koliko snage treba uložiti da se prebrodi barijera naučene bespomoćnosti, i jednostavno to ne činiš. Tako nastaju zombiji, koje, čini se, možemo izliječiti, ali nitko se zapravo time neće baviti.
Kada sam vidio da (da, da, onaj isti iz udžbenika) i radi ne predavanje, već sesiju pitanja i odgovora, malo sam se zabrinuo. U svakom slučaju, Leslie je svjetski poznati znanstvenik, autor temeljnih radova u distribuiranim računalnim sustavima, a možda ga znate i po slovima La u riječi LaTeX - „Lamport TeX“. Drugi zastrašujući faktor je njegov zahtjev: svi koji dođu moraju (potpuno besplatno) unaprijed odslušati neka od njegovih predavanja, smisliti barem jedno pitanje i tek tada doći. Odlučio sam vidjeti što Lamport iznosi - i to je divno! To je točno ta stvar, čarobna poveznica-tableta za izlečenje zombije. Upozoravam: teksta će se itekako zapaliti kod ljubitelja superflexibilnih metodologija i onih koji ne vole testirati ono što su napisali.
Nakon hubrokata, zapravo, počinje prijevod seminara. Ugodno čitanje!
Bez obzira na to koju zadatak preuzmete, uvijek morate proći kroz tri koraka:
- odrediti koji cilj želite postići;
- odlučiti kako ćete točno postići svoj cilj;
- doći do svog cilja.
To se odnosi i na programiranje. Kada pišemo kod, potrebno je:
- odlučiti što točno program treba raditi;
- utvrditi kako točno treba izvršiti svoj zadatak;
- napisati odgovarajući kod.
Zadnji korak je, naravno, vrlo važan, ali o tome danas neću govoriti. Umjesto toga, razgovarat ćemo o prva dva. Svaki programer ih provodi prije nego što započne s radom. Ne sjedite pisati ako niste odlučili što točno pišete: preglednik ili bazu podataka. Određeni uvid u cilj mora biti prisutan. I svakako razmišljate o tome što će program raditi, a ne pišete nasumično u nadi da će se kod nekako pretvoriti u preglednik.
Kako točno izgleda ovo prethodno razmišljanje o kodu? Koliko truda trebamo uložiti u to? Sve ovisi o tome koliki problem rješavamo. Recimo da želimo napisati otpornu distribuiranu sustav. U tom slučaju, trebamo dobro razmisliti prije nego što sjednemo za kod. A što ako jednostavno trebamo povećati cijeli broj varijable za 1? Na prvi pogled, ovdje je sve trivijalno i ne trebaju nam razmišljanja, ali se onda sjetimo da može doći do preopterećenja. Dakle, čak i da bismo shvatili je li problem jednostavan ili složen — prvo moramo razmisliti.
Ako unaprijed razmislite o mogućim rješenjima problema, možete izbjeći greške. No da bi to bilo moguće, vaše razmišljanje mora biti jasno. Da biste to postigli, trebate zapisivati svoje misli. Jako mi se sviđa citat Dicka Gindona: "Kada pišete, priroda vam pokazuje koliko su vaši misli neuredne." Ako ne pišete, samo vam se čini da razmišljate. A svoje misli trebate zapisivati u obliku specifikacija.
Specifikacije obavljaju mnoge funkcije, posebno u velikim projektima. No, govorim samo o jednoj od njih: pomažu nam da jasno razmišljamo. Jasno razmišljanje je vrlo važno i prilično teško, pa nam ovdje treba svaka pomoć. Na kojem jeziku trebamo pisati specifikacije? To je uvijek prvo pitanje za programere: na kojem jeziku ćemo pisati. Ne postoji jedan ispravni odgovor na to: problemi koje rješavamo su previše raznoliki. Za neke je korisna TLA+ — jezik specifikacija koji sam razvio. Za druge je prikladnije koristiti kineski. Sve ovisi o situaciji.
Postoji važnije pitanje: kako postići jasnije razmišljanje? Odgovor: trebamo razmišljati kao znanstvenici. Ovo je način razmišljanja koji se pokazao učinkovitom posljednjih 500 godina. U znanosti gradimo matematičke modele stvarnosti. Astronomija je, vjerojatno, bila prva znanost u pravom smislu te riječi. U matematičkom modelu koji se koristi u astronomiji, nebeska tijela pojavljuju se kao točke s masom, pozicijom i impulsa, iako su u stvarnosti izuzetno složeni objekti s planinama i oceanima, plimama i osekom. Ovaj model, kao i svaki drugi, stvoren je za rješavanje određenih zadataka. Odlično je prilagođen za određivanje kamo treba usmjeriti teleskop ako trebate pronaći planet. No, ako želite predvidjeti vrijeme na tom planetu, ovaj model neće biti od pomoći.
Matematika nam omogućuje da odredimo svojstva modela. A znanost pokazuje kako se ta svojstva odnose na stvarnost. Razgovarajmo o našoj znanosti, računalnim znanostima. Stvarnost s kojom radimo su računalni sustavi raznih vrsta: procesori, igraće konzole, računala koja izvršavaju programe i tako dalje. Govorit ću o izvršenju programa na računalu, ali, u suštini, svi ovi zaključci primjenjivi su na bilo koji računalni sustav. U našoj znanosti koristimo mnoge različite modele: Turingov stroj, djelomično uređene skupove događaja i mnoge druge.
Što je program? To je bilo koji kod koji se može smatrati samostalnim. Pretpostavimo da trebamo napisati preglednik. Provodimo tri zadatka: dizajniramo prikaz programa za korisnika, zatim pišemo visoko razinu sheme programa, i na kraju, pišemo kod. Tijekom pisanja koda shvaćamo da trebamo napisati alat za formatiranje teksta. Ovdje opet trebamo riješiti tri zadatka: odrediti koji će tekst ovaj alat vraćati; odabrati algoritam za formatiranje; napisati kod. Ovaj zadatak ima svoju podzadatak: pravilno umetati crticu u riječi. Ovu podzadatak također rješavamo u tri koraka — kao što vidimo, oni se ponavljaju na mnogim razinama.
Pogledajmo detaljnije prvi korak: koju zadatak rješava program. Ovdje najčešće modeliramo program kao funkciju koja prima neke ulazne podatke i isporučuje određene izlazne podatke. U matematici, funkcija se obično opisuje kao uređeni skup parova. Na primjer, funkcija kvadriranja za prirodne brojeve opisuje se kao skup {, , , , ...}. Domena takve funkcije su prvi elementi svakog para, odnosno prirodni brojevi. Da bismo definirali funkciju, trebamo navesti njenu domenu i formulu.
No, funkcije u matematici nisu isto što i funkcije u programskim jezicima. Matematika je znatno jednostavnija. Budući da nemam vremena za složene primjere, razmotrit ćemo jednostavan: funkcija u jeziku C ili statička metoda u Javi koja vraća najveći zajednički djelitelj dva cijela broja. U specifikaciji te metode napisat ćemo: izračunava GCD(M,N) za argumente M i N, gdje GCD(M,N) — funkcija čija je domena skup parova cijelih brojeva, a povratna vrijednost je najveći cijeli broj koji dijeli M i N. Kako se ovaj model odnosi na stvarnost? Model operira s cijelim brojevima, dok u C ili Javi imamo 32-bitni int. Ovaj model nam omogućuje da odredimo je li algoritam ispravan GCD, ali neće spriječiti greške preljeva. Za to bi bio potreban složeniji model, na kojem sada nema vremena.
Razgovarajmo o ograničenjima funkcije kao modela. Rad nekih programa (na primjer, operativnih sustava) nije samo vraćanje određenih vrijednosti za određene argumente, oni se mogu izvršavati kontinuirano. Osim toga, funkcija kao model nije pogodna za drugi korak: planiranje načina rješavanja zadatka. Brza i mehurasto sortiranje izračunavaju istu funkciju, ali to su potpuno različiti algoritmi. Stoga ću za opis načina postizanja cilja programa koristiti drugi model, nazovimo ga standardni model ponašanja. Program je u njemu predstavljen kao skup svih dozvoljenih ponašanja, od kojih je svako, zauzvrat, niz stanja, a stanje je dodjeljivanje vrijednosti varijablama.
Pogledajmo kako će izgledati drugi korak za Euklidov algoritam. Trebamo izračunati GCD(M, N). Inicijaliziramo M kao x, već N kao y, a zatim kontinuirano oduzimamo manju od ovih varijabli od veće dok ne postanu jednake. Na primjer, ako M = 12, već N = 18, možemo opisati sljedeće ponašanje:
[x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6]
A ako M = 0 i N = 0? Ноль делится на все числа, поэтому наибольшего делителя в этом случае нет. В этой ситуации нам нужно вернуться к первому шагу и спросить: действительно ли нам нужно вычислять НОД для неположительных чисел? Если в этом нет необходимости, то нужно просто изменить спецификацию.
Ovdje se mora napraviti malo odstupanje o produktivnosti. Često se mjeri brojem napisanim redaka koda dnevno. No, vaš rad je znatno korisniji ako se riješite određenog broja redaka, jer imate manje prostora za greške. I najlakše je riješiti se koda upravo u prvom koraku. Sasvim je moguće da vam jednostavno nisu potrebni svi ti dodaci koje pokušavate implementirati. Najbrži način za pojednostavljenje programa i uštedu vremena je ne raditi stvari koje ne vrijedi raditi. Drugi korak je na drugom mestu po potencijalu za uštedu vremena. Ako mjerite produktivnost brojem napisanih redaka, razmišljanje o načinu izvršenja zadatka učinit će vas manje produktivnima, budući da možete riješiti isti zadatak manjim obimom koda. Točne statistike ovdje ne mogu navesti, jer nemam način da izračunam onaj broj redaka koje nisam napisao zahvaljujući tome što sam potrošio vreme na specifikaciju, odnosno na prvi i drugi korak. I eksperiment ovdje ne možemo provesti, jer u eksperimentu nemamo pravo izvršiti prvi korak, zadatak je unaprijed definiran.
U neformalnim specifikacijama lako je zaboraviti na mnoge poteškoće. Nema ništa komplicirano u pisanju strogih specifikacija za funkcije, neću o tome raspravljati. Umjesto toga, razgovarat ćemo o pisanju strogih specifikacija za standardne modele ponašanja. Postoji teorema koja kaže da se bilo koji skup ponašanja može opisati svojstvom sigurnosti (safety) i svojstvom živosti (liveness). Sigurnost znači da ništa loše neće dogoditi, program neće dati netočan odgovor. Otpornost znači da će рано ili kasnije dogoditi nešto dobro, tj. program će рано ili касније dati točan odgovor. Općenito, sigurnost je važnija mjera, a greške se obično javljaju upravo ovdje. Stoga, kako bih uštedio vrijeme, neću govoriti o otpornosti, iako je ona, naravno, također važna.
Sigurnost postižemo opisivanjem, prvo, mnogih mogućih početnih stanja. I, drugo, odnosa sa svim mogućim sljedećim stanjima za svako stanje. Ponašat ćemo se kao znanstvenici i definirati stanja matematički. Skup početnih stanja opisuje se formulom, na primjer, u slučaju Euklidovog algoritma: (x = M) ∧ (y = N). Za određene vrijednosti M i N postoji samo jedno početno stanje. Odnos sa sljedećim stanjem opisuje se formulom u kojoj se varijable sljedećeg stanja zapisuju s crticom, a trenutnog stanja bez crte. U slučaju Euklidovog algoritma, imat ćemo posla s disjunkcijom dviju formula, od kojih jedna x je najveća vrijednost, a druga — y:
U prvom slučaju nova vrijednost y jednaka je prijašnjoj vrijednosti y, a novu vrijednost x dobivamo oduzimanjem manje varijable od veće. U drugom slučaju činimo obrnuto.
Vratimo se Euklidovom algoritmu. Pretpostavimo ponovno da M = 12, N = 18. To određuje jedinstveno početno stanje, (x = 12) ∧ (y = 18). Zatim ove vrijednosti zamjenjujemo u gornju formulu i dobivamo:
Ovdje je jedina moguća solucija: x' = 18 - 12 ∧ y' = 12, i dobivamo ponašanje: [x = 12, y = 18]. Na sličan način možemo opisati sva stanja u našem ponašanju: [x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6].
U posljednjem stanju [x = 6, y = 6] obje strane izraza bit će neistinite, stoga sljedećeg stanja nema. Dakle, imamo potpunu specifikaciju drugog koraka — kao što vidimo, to je sasvim obična matematika, kao kod inženjera i znanstvenika, a ne čudna, kao u računalnim znanostima.
Te dvije formule mogu se spojiti u jednu formulu temporalne logike. Ona je elegantna i lako je objasniti, ali trenutno nema vremena za to. Temporalna logika može nam biti potrebna samo za svojstvo živosti, za sigurnost nije potrebna. Sama temporalna logika nije omiljena, nije posve obična matematika, ali u slučaju živosti ona je nužno zlo.
U Euklidovom algoritmu za svaku vrijednost x i y postoje jedinstvene vrijednosti x' i y', koje čine odnos s sljedećim stanjem istinitim. Drugim riječima, Euklidov algoritam je deterministički. Da bismo simulirali nedeterministički algoritam, potrebno je da trenutno stanje ima više mogućih budućih stanja, i da svaka vrijednost varijable bez crte ima nekoliko vrijednosti varijable s crtom, pri čemu odnos s sljedećim stanjem postaje istinit. To nije teško učiniti, ali sada neću davati primjere.
Da bismo napravili funkcionalni alat, potrebna je formalna matematika. Kako učiniti specifikaciju formalnom? Za to će nam trebati formalni jezik, na primjer, . Specifikacija Euklidovog algoritma na tom jeziku izgledat će ovako:
Simbol znaka jednakosti s trokutom označava da je vrijednost lijevo od znaka definirana kao jednaka vrijednosti desno od znaka. U suštini, specifikacija je definicija, u našem slučaju dvije definicije. Kako bi specifikacija u TLA+ bila potpuna, potrebno je dodati deklaracije i određenu sintaksu, kao što je prikazano na slajdu iznad. U ASCII obliku to će izgledati ovako:
Kao što vidimo, nije ništa komplicirano. Specifikaciju u TLA+ moguće je provjeriti, tj. obuhvatiti sve moguće ponašanja u malom modelu. U našem slučaju, taj model bit će određene vrijednosti M i N. To je vrlo učinkovit i jednostavan način provjere koji se u potpunosti izvodi automatski. Osim toga, moguće je napisati formalne dokaze istinitosti i provjeriti ih mehanički, ali za to je potrebno puno vremena, pa gotovo nitko to ne radi.
Glavni nedostatak TLA+ je u tome što je to matematika, a programeri i računalni znanstvenici se boje matematike. Na prvi pogled to zvuči kao šala, ali, nažalost, govorim to sasvim ozbiljno. Moj kolega mi je upravo pričao o tome kako je pokušao objasniti TLA+ nekoliko programerima. Čim su se na ekranu pojavile formule, odmah su dobili staklene oči. Tako da, ako TLA+ zastrašuje, može se koristiti , to je svojevrsni igračka programski jezik. Izraz u PlusCal može biti bilo koji izraz TLA+, odnosno, u suštini, bilo koji matematički izraz. Štoviše, PlusCal ima sintaksu za nedeterminističke algoritme. Budući da se u PlusCal može zapisati bilo koji izraz TLA+, on je značajno izražajniji od bilo kojeg stvarnog programskog jezika. Nadalje, PlusCal se prevodi u lako čitljivu specifikaciju TLA+. To ne znači, naravno, da će složena specifikacija PlusCal postati jednostavna u TLA+ — samo je očigledna podudarnost između njih, neće se javiti dodatna složenost. Na kraju, tu specifikaciju može provjeriti alati TLA+. Ukratko, PlusCal može pomoći u prevladavanju fobije od matematike, lako ga je razumjeti čak i programerima i računalnim znanstvenicima. U prošlosti sam neko vrijeme (oko 10 godina) objavljivao algoritme na njemu.
Možda će netko prigovoriti da su TLA+ i PlusCal — to matematika, a matematika radi samo na izmišljenim primjerima. U praksi je potrebn je pravi jezik s tipovima, procedurama, objektima i tako dalje. To nije točno. Evo što piše Chris Newcomb, koji je radio u Amazonu: «Koristili smo TLA+ u deset velikih projekata, i u svakom slučaju njegovo korištenje je znatno doprinijelo razvoju, jer smo mogli uhvatiti opasne greške prije nego što su otišle u produkciju, i zato što nam je pružilo razumijevanje i povjerenje potrebno za agresivne optimizacije performansi, koje ne utječu na istinitost programa». Često se može čuti da pri korištenju formalnih metoda dobivamo neučinkovit kod — u praksi je ipak sve potpuno obrnut. Osim toga, postoji uvjerenje da je nemoguće uvjeriti menadžere u potrebu za formalnim metodama, čak i kada programeri vjeruju u njihovu korisnost. A Newcomb piše: „Menadžeri sada sve više potiču da pišemo specifikacije na TLA+, i posebno odvajaju vreme za to“. Tako da kada menadžeri vide da TLA+ funkcioniše, rado ga prihvataju. Kris Njukomb je to napisao pre nekih šest meseci (u oktobru 2014. godine), a sada, koliko znam, TLA+ se koristi u 14 projekata, a ne 10. Drugi primer se odnosi na projektovanje XBox 360. Čarlzu Tekeru se obratio pripravnik i napisao specifikaciju za sistem memorije. Zahvaljujući toj specifikaciji pronađen je bag koji inače ne bi bio primećen, a zbog kojeg bi svaka XBox 360 padala nakon četiri sata korišćenja. Inženjeri iz IBM-a su potvrdili da njihovi testovi ne bi otkrili ovaj bag.
O TLA+ možete pročitati više na internetu, a sada hajde da pričamo o neformalnim specifikacijama. Retko pišemo programe koji izračunavaju najveći zajednički delilac i tome slično. Značajno češće pišemo programe poput alata za strukturalno formatiranje (pretty-printer), koji sam napisao za TLA+. Nakon najjednostavnijeg obrade, kod na TLA+ bi izgledao ovako:
Ali u navedenom primeru, korisnik je verovatno želeo da simboli konjukcije i jednakosti budu poravnati. Tako da bi ispravno formatiranje verovatno izgledalo ovako:
Razmotrimo drugi primer:
Ovde, naprotiv, poravnanje simbola jednakosti, sabiranja i množenja u izvoru je bilo slučajno, tako da je najjednostavnija obrada sasvim dovoljna. U suštini, ne postoji tačna matematička definicija ispravnog formatiranja, jer „ispravno“ u ovom slučaju znači „onako kako želi korisnik“, a to se matematički ne može odrediti.
Na prvi pogled, ako nemamo definiciju istinitosti, specifikacija je beskorisna. No, to nije tačno. Ako ne znamo šta program tačno treba da uradi, to ne znači da ne trebamo razmišljati o njegovom radu - naprotiv, trebamo uložiti još više truda u to. Specifikacija je ovde posebno važna. Nije moguće odrediti optimalan program za strukturalno formatiranje, ali to ne znači da se ne bi trebali time baviti uopšte; pisanje koda kao tok svesti nije rešenje. Na kraju sam napisao specifikaciju od šest pravila s definicijama u obliku komentara u Java datoteci. Evo primjera jednog od pravila: token lijevog komentara je LeftComment usklađen s njegovim pokrivnim tokenom. Ovo pravilo je napisano na, recimo, matematičkom engleskom: LeftComment usklađen, lijevi komentar i pokrivni token — termini s definicijama. Tako matematičari opisuju matematiku: pišu definicije termina i na temelju njih — pravila. Korist od takve specifikacije je u tome što je razumjeti i debagirati šest pravila znatno lakše nego 850 redaka koda. Treba reći da nije bilo lako napisati ova pravila, potrošeno je prilično mnogo vremena na njihovu debagiranje. Posebno za tu svrhu napisao sam kod koji je javio koje se točno pravilo koristi. Zahvaljujući tome što sam provjerio tih šest pravila na nekoliko primjera, nisam morao debagirati 850 redaka koda, a greške je bilo prilično lako pronaći. U Javi postoje odlični alati za to. Da sam samo napisao kod, puno bi više vremena otišlo, a formatiranje bi bilo lošije.
Zašto nije bilo moguće koristiti formalnu specifikaciju? S jedne strane, ispravnost izvršenja ovdje nije suviše važna. Strukturni ispis sigurno neće odgovarati nekome, tako da nisam trebao postići ispravnost u svim neobičnim situacijama. Još važnije je to što nisam imao adekvatne alate. Alat za provjeru modela TLA+ ovdje je beskoristan, pa bih morao ručno pisati primjere.
Priložena specifikacija ima osobine zajedničke svim specifikacijama. Ona je na višoj razini od koda. Može se implementirati na bilo kojem jeziku. Za njezino pisanje beskorisni su bilo kakvi alati ili metode. Nijedan tečaj programiranja vam neće pomoći da napišete ovu specifikaciju. I ne postoje alati koji bi učinili ovu specifikaciju suvišnom, osim ako ne pišete jezik posebno za pisanje programa strukturnog ispisa na TLA+. Na kraju, ova specifikacija ne govori ništa o tome kako ćemo pisati kod, već samo ukazuje na ono što taj kod radi. Pišemo specifikaciju kako bismo nam pomogli razmisliti o problemu prije nego što počnemo razmišljati o kodu.
Ali ova specifikacija ima i osobine koje je razlikuju od drugih specifikacija. 95% drugih specifikacija značajno je kraće i jednostavnije:
Dalje, ova specifikacija predstavlja skup pravila. Općenito, to je znak loše specifikacije. Razumjeti posljedice niza pravila prilično je teško, i upravo zato sam morao potrošiti puno vremena na njihovo ispravljanje. Ipak, u ovom slučaju nisam mogao pronaći bolji način.
Treba reći nekoliko riječi o programima koji rade neprekidno. Općenito, oni rade paralelno, na primjer, operativni sustavi ili distribuirani sustavi. Malo tko može razumjeti njihovu funkciju u mislima ili na papiru, a ja ne pripadam toj grupi, iako sam to nekada mogao. Stoga su potrebni alati koji će provjeriti naš rad — na primjer, TLA+ ili PlusCal.
Zašto je bilo potrebno napisati specifikaciju ako sam već znao što kôd treba raditi? U stvari, samo mi se činilo da to znam. Osim toga, uz prisustvo specifikacije, vanjskim osobama više nije potrebno zavirivati u kôd da bi shvatile što on radi. Imam pravilo: ne smije biti općih pravila. Ovo pravilo, naravno, ima iznimku, to je jedino opće pravilo kojem slijedim: specifikacija onoga što kôd radi mora ljudima reći sve što trebaju znati pri korištenju tog koda.
Dakle, što programeri trebaju znati o razmišljanju? Prvo, isto što i svi drugi: ako ne pišeš, samo ti se čini da razmišljaš. Osim toga, treba razmisliti prije nego što kodiraš, a to znači da trebaš pisati prije nego što kodiraš. Specifikacija je ono što pišemo prije nego što počnemo kodirati. Specifikacija je potrebna za svaki kod koji može koristiti ili mijenjati bilo tko. A taj „bilo tko“ može biti i sam autor koda mjesec dana nakon što ga je napisao. Specifikacija je potrebna za velike programe i sustave, za klase, za metode, a ponekad čak i za složene dijelove pojedine metode. Što točno treba pisati o kodu? Treba opisati što kod radi, odnosno ono što može biti korisno svakome tko koristi taj kod. Ponekad može biti potrebno i navesti kako točno kod postiže svoj cilj. Ako smo taj način prolazili na tečaju o algoritmima, nazivamo to algoritmom. Ako je to nešto specijalizirano i novo, nazivamo to visok nivo dizajna. Formalne razlike ovdje nema: i jedno i drugo je apstraktni model programa.
Kako bi trebala izgledati specifikacija koda? Najvažnije: ona treba biti na razini iznad samog koda. Treba opisivati stanja i ponašanja. Treba biti toliko stroga koliko to zadatak zahtijeva. Ako pišete specifikaciju načina realizacije zadatka, možete je napisati u pseudokodu ili uz pomoć PlusCal. Učiti pisati specifikacije treba na formalnim specifikacijama. To će vam dati potrebne vještine, koje pomažu i s neformalnim. A kako naučiti pisati formalne specifikacije? Kada smo učili programirati, pisali smo programe, a zatim ih otklanjali. I ovdje je isto: treba napisati specifikaciju, provjeriti je pomoću alata za provjeru modela i ispraviti pogreške. TLA+ možda nije najbolji jezik za formalne specifikacije, i vjerojatno će za vaše specifične potrebe bolje odgovarati drugi jezik. Prednost TLA+ je u tome što odlično podučava matematičkom razmišljanju.
Kako povezati specifikaciju i kod? Pomoću komentara koji povezuju matematičke pojmove i njihovu implementaciju. Ako radite s grafovima, tada ćete na razini programa imati nizove čvorova i nizove povezanosti. Stoga trebate napisati kako se graf konkretno implementira tim programskim strukturama.
Treba napomenuti da ništa od rečenog ne odnosi se na sam proces pisanja koda. Kada pišete kod, odnosno kada izvršavate treći korak, također morate razmišljati i planirati program. Ako se podzadacija pokaže složenom ili nejasnom, potrebno je napisati specifikaciju za nju. No ovdje ne govorim o samom kodu. Možete koristiti bilo koji programski jezik, bilo koju metodologiju, to nije tema. Osim toga, ništa od rečenog ne oslobađa vas obveze testiranja i otklanjanja grešaka u kodu. Čak i ako je apstraktni model ispravno napisan, u njegovoj implementaciji mogu postojati greške.
Pisanje specifikacija je dodatna faza u procesu pisanja koda. Zahvaljujući tome, mnoge greške može se otkriti s manje truda — to znamo iz iskustva programera iz Amazona. Uz specifikacije, kvaliteta programa postaje viša. Pa zašto onda tako često prolazimo bez njih? Zato što je pisanje teško. A teško je pisati jer za to treba razmišljati, a razmišljati je također teško. Uvijek je lakše praviti se da razmišljate. Ovdje se može povući analogija s trčanjem — što manje trčite, to sporije trčite. Trebate trenirati svoje mišiće i vježbati u pisanju. Potrebna je praksa.
Specifikacija može biti netočna. Mogli ste negdje napraviti pogrešku, ili su se zahtjevi mogli promijeniti, ili je bilo potrebno napraviti poboljšanje. Svaki kod koji netko koristi treba promijeniti, stoga će prije ili kasnije specifikacija prestati odgovarati programu. U idealnom slučaju, u ovom bi slučaju trebalo napisati novu specifikaciju i potpuno prepisati kod. Dobro znamo da to nitko ne radi. U praksi krpamo kod i možda ažuriramo specifikaciju. Ako se to neizbježno događa prije ili kasnije, zašto uopće pisati specifikacije? Prvo, za osobu koja će uređivati vaš kod, svaka suvišna riječ u specifikaciji bit će zlata vrijedna, a ta osoba možete biti i vi sami. Često se kritiziram zbog nedovoljne specifikacije kada uređujem svoj kod. I pišem više specifikacija nego koda. Stoga, kada uređujete kod, specifikaciju uvijek treba ažurirati. Kad god nešto promijenite, kod postaje lošiji, sve ga je teže čitati i održavati. To je nakupljanje entropije. Ali ako ne započnete sa specifikacijom, svaka napisana linija bit će ispravka, a kod će od samog početka biti glomazan i teško čitljiv.
Kako je rekao , nitko nije dobio bitku prema planu, i nitko nije dobio bitku bez plana. A on je znao nešto o bitkama. Postoji mišljenje da je pisanje specifikacija besplodna potraga. Ponekad je to zaista tako i zadatak je toliko jednostavan da nema potrebe razmišljati o njemu. No uvijek se treba sjetiti da kada vam savjetuju da ne pišete specifikacije, zapravo vam savjetuju da ne razmišljate. I o tome treba svaki put razmisliti. Razmišljanje o zadatku ne jamči da nećete napraviti pogreške. Kao što znamo, nitko nije izmislio čarobni štapić, a programiranje je složena aktivnost. Ali ako ne promišljate zadatak, sigurno ćete napraviti pogreške.
Više o TLA+ i PlusCal možete pročitati na posebnoj stranici, gdje možete otići s moje početne stranice . To je sve za sada, hvala na pažnji.
Podsjećam vas da je ovo prijevod. Kada budete pisali komentare, imajte na umu da autor neće to pročitati. Ako stvarno želite razgovarati s autorom, bit će na konferenciji Hydra 2019, koja će se održati 11-12. srpnja 2019. godine u Saint Petersburgu. Ulaznice se mogu kupiti .
Izvor: habr.com
