Ovaj članak je prijevod . Ali prije nje mali uvod. Kako nastaju zombiji? Svatko dođe u situaciju da želi prijatelja ili kolegu podići na svoju razinu, ali ne ide. I ne "ne ide" toliko kod vas koliko kod njega: s jedne strane ljestvice je normalna plaća, zadaci i tako dalje, a s druge potreba za razmišljanjem. Razmišljanje je neugodno i bolno. Brzo odustaje i nastavlja pisati kod bez da imalo uključuje mozak. Zamislite koliko je truda potrebno da se prevlada barijera naučene bespomoćnosti, a vi to jednostavno ne učinite. Tako nastaju zombiji koji se, čini se, mogu izliječiti, no čini se da to nitko neće učiniti.
Kad sam to vidio (da, isti drug iz udžbenika) i ne radi izvješće, nego sesiju pitanja i odgovora, bio sam malo oprezan. Za svaki slučaj, Leslie je svjetski poznati znanstvenik, autor temeljnih djela iz distribuiranog računarstva, a možete ga znati i po slovima La u riječi LaTeX - “Lamport TeX”. Drugi alarmantni faktor je njegov zahtjev: svi koji dolaze moraju (potpuno besplatno) unaprijed poslušati nekoliko njegovih izvještaja, smisliti barem jedno pitanje na njih i tek onda doći. Odlučio sam vidjeti što Lamport tamo emitira – i super je! To je upravo ta stvar, čarobna karika-pilula za liječenje zombija. Upozoravam vas: od teksta mogu osjetno izgorjeti ljubitelji superfleksibilnih metodologija i oni koji ne vole testirati napisano.
Nakon habrokata, zapravo, počinje prijevod seminara. Uživaj čitajući!
Koji god zadatak prihvatili, uvijek trebate proći kroz tri koraka:
- odlučite koji cilj želite postići;
- odlučite kako ćete postići svoj cilj;
- doći do svog cilja.
To se također odnosi i na programiranje. Kada pišemo kod, moramo:
- odlučiti što bi program trebao učiniti;
- odrediti kako treba obavljati svoju zadaću;
- napišite odgovarajući kod.
Posljednji korak je, naravno, vrlo važan, ali neću o tome danas. Umjesto toga, raspravljat ćemo o prva dva. Svaki ih programer izvodi prije početka rada. Ne sjedate da pišete ako niste odlučili pišete li preglednik ili bazu podataka. Određena ideja o cilju mora biti prisutna. I svakako razmislite o tome što će točno program učiniti, a nemojte pisati nekako u nadi da će se kod nekako pretvoriti u preglednik.
Kako se točno događa ovo prethodno razmišljanje koda? Koliko truda trebamo uložiti u ovo? Sve ovisi o tome koliko je složen problem koji rješavamo. Pretpostavimo da želimo napisati distribuirani sustav otporan na pogreške. U ovom slučaju, trebali bismo dobro razmisliti prije nego što sjednemo za kodiranje. Što ako samo trebamo povećati cjelobrojnu varijablu za 1? Na prvi pogled ovdje je sve trivijalno i nema potrebe za razmišljanjem, ali onda se sjetimo da može doći do preljeva. Stoga, čak i da biste razumjeli je li problem jednostavan ili složen, prvo morate razmisliti.
Ako unaprijed razmislite o mogućim rješenjima problema, možete izbjeći pogreške. Ali ovo zahtijeva da vaše razmišljanje bude jasno. Da biste to postigli, morate zapisati svoje misli. Jako mi se sviđa citat Dicka Guindona: "Kad pišete, priroda vam pokazuje koliko aljkavo razmišljate." Ako ne pišete, samo mislite da razmišljate. I trebate zapisati svoje misli u obliku specifikacija.
Specifikacije obavljaju mnoge funkcije, osobito u velikim projektima. Ali govorit ću samo o jednom od njih: pomažu nam da jasno razmišljamo. Jasno razmišljanje je vrlo važno i prilično teško, stoga nam je potrebna svaka pomoć. Na kojem jeziku trebamo pisati specifikacije? Općenito, ovo je uvijek prvo pitanje programera: na kojem jeziku ćemo pisati. Ne postoji jedan točan odgovor na njega: problemi koje rješavamo previše su raznoliki. Za neke je TLA+ specifikacijski jezik koji sam ja razvio. Za druge je prikladnije koristiti kineski. Sve ovisi o situaciji.
Važnije je drugo pitanje: kako postići jasnije mišljenje? Odgovor: Moramo razmišljati kao znanstvenici. Ovo je način razmišljanja koji se dokazao u proteklih 500 godina. U znanosti gradimo matematičke modele stvarnosti. Astronomija je bila možda prva znanost u strogom smislu riječi. U matematičkom modelu koji se koristi u astronomiji, nebeska tijela se pojavljuju kao točke s masom, položajem i količinom gibanja, iako su u stvarnosti iznimno složeni objekti s planinama i oceanima, plimama i osekama. Ovaj model, kao i svaki drugi, stvoren je za rješavanje određenih problema. Izvrstan je za određivanje kamo usmjeriti teleskop ako trebate pronaći planet. Ali ako želite predvidjeti vrijeme na ovoj planeti, ovaj model neće raditi.
Matematika nam omogućuje da odredimo svojstva modela. A znanost pokazuje kako su ta svojstva povezana sa stvarnošću. Razgovarajmo o našoj znanosti, informatici. Stvarnost s kojom radimo su računalni sustavi raznih vrsta: procesori, igraće konzole, računala, izvršni programi i tako dalje. Govorit ću o pokretanju programa na računalu, ali uglavnom svi ovi zaključci vrijede za bilo koji računalni sustav. U našoj znanosti koristimo mnogo različitih modela: Turingov stroj, djelomično uređene skupove događaja i mnoge druge.
Što je program? Ovo je bilo koji kod koji se može razmatrati neovisno. Pretpostavimo da trebamo napisati preglednik. Obavljamo tri zadatka: dizajniramo korisnički pogled na program, zatim pišemo dijagram visoke razine programa i na kraju pišemo kod. Dok pišemo kod, shvaćamo da trebamo napisati formatiranje teksta. Ovdje opet trebamo riješiti tri problema: odrediti koji će tekst ovaj alat vratiti; odaberite algoritam za oblikovanje; napisati kod. Ovaj zadatak ima i svoj podzadatak: pravilno umetanje crtice u riječi. I ovaj podzadatak rješavamo u tri koraka – kao što vidite, oni se ponavljaju na više razina.
Razmotrimo detaljnije prvi korak: koji problem program rješava. Ovdje najčešće modeliramo program kao funkciju koja uzima neki ulaz i proizvodi nešto izlaza. U matematici se funkcija obično opisuje kao uređeni skup parova. Na primjer, funkcija kvadriranja prirodnih brojeva opisuje se kao skup {<0,0>, <1,1>, <2,4>, <3,9>, …}. Domena takve funkcije je skup prvih elemenata svakog para, odnosno prirodnih brojeva. Da bismo definirali funkciju, moramo specificirati njezin opseg i formulu.
Ali funkcije u matematici nisu isto što i funkcije u programskim jezicima. Matematika je puno lakša. Budući da nemam vremena za složene primjere, razmotrimo jedan jednostavan: funkcija u C-u ili statička metoda u Javi koja vraća najveći zajednički djelitelj dvaju cijelih brojeva. U specifikaciji ove metode napisat ćemo: izračunava GCD(M,N) za argumente M и NGdje GCD(M,N) - funkcija čija je domena skup parova cijelih brojeva, a povratna vrijednost je najveći cijeli broj koji je djeljiv s M и N. Kako se ovaj model odnosi na stvarnost? Model radi s cijelim brojevima, dok u C-u ili Javi imamo 32-bitni int. Ovaj model nam omogućuje da odlučimo je li algoritam ispravan GCD, ali to neće spriječiti pogreške prelijevanja. To bi zahtijevalo složeniji model, za koji nema vremena.
Razgovarajmo o ograničenjima funkcije kao modela. Neki programi (kao što su operativni sustavi) ne samo da vraćaju određenu vrijednost za određene argumente, oni mogu raditi neprekidno. Osim toga, funkcija kao model nije prikladna za drugi korak: planiranje kako riješiti problem. Brzo sortiranje i sortiranje u mjehurićima izračunavaju istu funkciju, ali to su potpuno različiti algoritmi. Stoga, da bih opisao kako se postiže cilj programa, koristim drugačiji model, nazovimo ga standardni model ponašanja. Program u njemu predstavljen je kao skup svih dopuštenih ponašanja, od kojih je svako zauzvrat niz stanja, a stanje je dodjeljivanje vrijednosti varijablama.
Pogledajmo kako bi izgledao drugi korak za Euklidov algoritam. Moramo izračunati GCD(M, N). Inicijaliziramo M kao xI N kao y, zatim više puta oduzmite manju od ovih varijabli od veće dok ne budu jednake. Na primjer, ako M = 12I 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 и N = 0? Nula je djeljiva sa svim brojevima, pa u ovom slučaju ne postoji najveći djelitelj. U ovoj situaciji, moramo se vratiti na prvi korak i pitati: trebamo li stvarno izračunati GCD za nepozitivne brojeve? Ako to nije potrebno, samo trebate promijeniti specifikaciju.
Ovdje bismo trebali napraviti malu digresiju o produktivnosti. Često se mjeri u broju linija koda napisanih po danu. Ali vaš rad je puno korisniji ako se riješite određenog broja redaka, jer imate manje mjesta za greške. A najlakši način da se riješite koda je na prvom koraku. Posve je moguće da vam jednostavno ne trebaju sva zvona i zviždaljke koje pokušavate implementirati. Najbrži način da pojednostavite program i uštedite vrijeme je da ne radite stvari koje se ne bi trebale raditi. Drugi korak drugi je potencijal za uštedu vremena. Ako produktivnost mjerite brojem napisanih redaka, razmišljanje o tome kako izvršiti zadatak učinit će vas manje produktivan, jer možete riješiti isti problem s manje koda. Ovdje ne mogu dati točnu statistiku, jer nemam načina da prebrojim redove koje nisam napisao zbog činjenice da sam potrošio vrijeme na specifikaciju, odnosno na prvi i drugi korak. A pokus se ni tu ne može postaviti, jer u pokusu nemamo pravo dovršiti prvi korak, zadatak je unaprijed zadan.
Lako je previdjeti mnoge poteškoće u neformalnim specifikacijama. Nema ništa teško napisati stroge specifikacije za funkcije, o tome neću raspravljati. Umjesto toga, govorit ćemo o pisanju jakih specifikacija za standardna ponašanja. Postoji teorem koji kaže da se svaki skup ponašanja može opisati korištenjem svojstva sigurnosti (sigurnost) i svojstva preživljavanja (živost). Sigurnost znači da se ništa loše neće dogoditi, program neće dati netočan odgovor. Preživljivost znači da će se prije ili kasnije dogoditi nešto dobro, tj. program će prije ili kasnije dati točan odgovor. Sigurnost je u pravilu važniji pokazatelj, tu se najčešće javljaju pogreške. Stoga, da uštedim vrijeme, neću govoriti o preživljavanju, iako je to, naravno, također važno.
Sigurnost postižemo propisivanjem, prvo, skupa mogućih početnih stanja. I drugo, odnosi sa svim mogućim sljedećim stanjima za svako stanje. Ponašajmo se kao znanstvenici i matematički definirajmo stanja. Skup početnih stanja opisuje se formulom, na primjer, u slučaju Euklidovog algoritma: (x = M) ∧ (y = N). Za određene vrijednosti M и N postoji samo jedno početno stanje. Odnos sa sljedećim stanjem opisuje se formulom u kojoj se varijable sljedećeg stanja pišu s primarnim brojem, a varijable trenutnog stanja pišu se bez prabroja. U slučaju Euklidovog algoritma bavit ćemo se disjunkcijom dviju formula od kojih jedna x je najveća vrijednost, au drugom - y:
U prvom slučaju nova vrijednost y jednaka je prethodnoj vrijednosti y, a novu vrijednost x dobivamo oduzimanjem manje varijable od veće. U drugom slučaju radimo suprotno.
Vratimo se Euklidovom algoritmu. Pretpostavimo opet da M = 12, N = 18. Ovo definira jedno početno stanje, (x = 12) ∧ (y = 18). Zatim ubacujemo te vrijednosti u gornju formulu i dobivamo:
Ovo je jedino moguće rješenje: x' = 18 - 12 ∧ y' = 12i dobivamo ponašanje: [x = 12, y = 18]. Slično, 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] oba dijela izraza će biti lažna, tako da nema sljedećeg stanja. Dakle, imamo potpunu specifikaciju drugog koraka - kao što vidite, ovo je sasvim obična matematika, kao kod inženjera i znanstvenika, a ne čudna, kao u informatici.
Ove dvije formule mogu se spojiti u jednu formulu temporalne logike. Elegantna je i lako je objasniti, ali za nju sada nema vremena. Vremenska logika nam može trebati samo za svojstvo živosti, nije potrebna za sigurnost. Ne volim temporalnu logiku kao takvu, nije to sasvim obična matematika, ali u slučaju živosti ona je nužno zlo.
U Euklidovom algoritmu za svaku vrijednost x и y imaju jedinstvene vrijednosti x' и y', koji odnos sa sljedećim stanjem čine istinitim. Drugim riječima, Euklidov algoritam je deterministički. Da bi se modelirao nedeterministički algoritam, trenutno stanje treba imati više mogućih budućih stanja, te da svaka vrijednost varijable bez primarnog broja ima višestruke vrijednosti varijable s primom tako da je odnos prema sljedećem stanju istinit. To je lako učiniti, ali neću sada davati primjere.
Da biste napravili radni alat, potrebna vam je formalna matematika. Kako specifikaciju učiniti formalnom? Da bismo to učinili, potreban nam je formalni jezik, na primjer, . Specifikacija Euklidovog algoritma bi izgledala ovako na ovom jeziku:
Simbol znaka jednakosti s trokutom znači da je vrijednost s lijeve strane znaka definirana kao jednaka vrijednosti s desne strane znaka. U biti, specifikacija je definicija, u našem slučaju dvije definicije. Specifikaciji u TLA+ morate dodati deklaracije i neku sintaksu, kao na slajdu iznad. U ASCII bi to izgledalo ovako:
Kao što vidite, ništa komplicirano. Specifikacija za TLA+ može se testirati, tj. zaobići sva moguća ponašanja u malom modelu. U našem slučaju, ovaj model će biti određene vrijednosti M и N. Ovo je vrlo učinkovita i jednostavna metoda provjere koja je potpuno automatska. Također je moguće napisati formalne dokaze istinitosti i provjeriti ih mehanički, ali to oduzima puno vremena, pa to gotovo nitko ne radi.
Glavni nedostatak TLA+ je što je to matematika, a programeri i informatičari se boje matematike. Na prvi pogled ovo zvuči kao šala, ali, nažalost, mislim potpuno ozbiljno. Kolega mi je upravo pričao kako je nekoliko programera pokušao objasniti TLA+. Čim su se formule pojavile na ekranu, odmah su postale staklene oči. Dakle, ako vas TLA+ plaši, možete koristiti , to je vrsta programskog jezika igračke. Izraz u PlusCal-u može biti bilo koji TLA+ izraz, to jest, uglavnom, bilo koji matematički izraz. Osim toga, PlusCal ima sintaksu za nedeterminističke algoritme. Budući da PlusCal može napisati bilo koji TLA+ izraz, PlusCal je mnogo izražajniji od bilo kojeg pravog programskog jezika. Zatim se PlusCal kompilira u lako čitljivu TLA+ specifikaciju. To, naravno, ne znači da će se složena PlusCal specifikacija pretvoriti u jednostavnu na TLA + - samo je korespondencija između njih očigledna, neće biti dodatne složenosti. Konačno, ovu specifikaciju mogu provjeriti TLA+ alati. Sve u svemu, PlusCal može pomoći u prevladavanju matematičke fobije i lako ga razumiju čak i programeri i informatičari. U prošlosti sam neko vrijeme (oko 10 godina) objavljivao algoritme na njemu.
Možda će netko prigovoriti da su TLA + i PlusCal matematika, a matematika radi samo na izmišljenim primjerima. U praksi vam je potreban pravi jezik s tipovima, procedurama, objektima i tako dalje. To je pogrešno. Evo što piše Chris Newcomb, koji je radio u Amazonu: “Koristili smo TLA+ na deset velikih projekata, au svakom slučaju, korištenje je značajno promijenilo razvoj jer smo uspjeli uhvatiti opasne greške prije nego što smo krenuli s proizvodnjom i jer nam je dao uvid i povjerenje koje smo trebali napraviti agresivne optimizacije performansi bez utjecaja na istinitost programa". Često možete čuti da korištenjem formalnih metoda dobivamo neučinkovit kod - u praksi je sve upravo suprotno. Osim toga, postoji mišljenje da se menadžeri ne mogu uvjeriti u potrebu formalnih metoda, čak i ako su programeri uvjereni u njihovu korisnost. A Newcomb piše: "Menadžeri sada snažno guraju pisanje specifikacija za TLA + i posebno izdvajaju vrijeme za to". Dakle, kada menadžeri vide da TLA+ radi, rado to prihvaćaju. Chris Newcomb je ovo napisao prije otprilike šest mjeseci (listopad 2014.), ali sada, koliko ja znam, TLA+ se koristi u 14 projekata, a ne u 10. Drugi primjer je u dizajnu XBoxa 360. Pripravnik je došao Charlesu Thackeru i napisao specifikaciju za memorijski sustav. Zahvaljujući ovoj specifikaciji, pronađen je bug koji bi inače prošao nezapaženo, a zbog kojeg bi se svaki XBox 360 srušio nakon četiri sata korištenja. IBM-ovi inženjeri potvrdili su da njihovi testovi ne bi pronašli ovu grešku.
Više o TLA + možete pročitati na Internetu, ali sada razgovarajmo o neformalnim specifikacijama. Rijetko moramo pisati programe koji izračunavaju najmanji zajednički djelitelj i slično. Puno češće pišemo programe poput alata za lijepi pisač koji sam napisao za TLA+. Nakon najjednostavnije obrade, TLA + kod bi izgledao ovako:
Ali u gornjem primjeru, korisnik je najvjerojatnije želio da se veznici i jednakosti poravnaju. Dakle, ispravno oblikovanje bi više izgledalo ovako:
Razmotrimo još jedan primjer:
Ovdje je, naprotiv, poravnanje znakova jednakosti, zbrajanja i množenja u izvoru bilo slučajno, pa je najjednostavnija obrada sasvim dovoljna. Općenito, ne postoji točna matematička definicija ispravnog oblikovanja, jer "ispravno" u ovom slučaju znači "ono što korisnik želi", a to se ne može matematički odrediti.
Čini se da ako nemamo definiciju istine, onda je specifikacija beskorisna. Ali nije. Samo zato što ne znamo što bi program trebao raditi ne znači da ne trebamo razmišljati o tome kako funkcionira — naprotiv, moramo uložiti još više truda u to. Specifikacija je ovdje posebno važna. Nemoguće je odrediti optimalan program za strukturirani ispis, ali to ne znači da ga se uopće ne trebamo prihvatiti, a pisanje koda kao toka svijesti nije dobra stvar. Na kraju sam napisao specifikaciju od šest pravila s definicijama u obliku komentara u java datoteci. Evo primjera jednog od pravila: a left-comment token is LeftComment aligned with its covering token. Ovo pravilo je napisano na, da tako kažemo, matematičkom engleskom jeziku: LeftComment aligned, left-comment и covering token - pojmovi s definicijama. Ovako matematičari opisuju matematiku: pišu definicije pojmova i na temelju njih pravila. Prednost takve specifikacije je da je šest pravila puno lakše razumjeti i otkloniti pogreške nego 850 redaka koda. Moram reći da pisanje ovih pravila nije bilo lako, trebalo je dosta vremena da se isprave pogreške. Posebno u tu svrhu napisao sam kod koji je javljao koje je pravilo korišteno. Zahvaljujući činjenici da sam ovih šest pravila testirao na nekoliko primjera, nisam morao debugirati 850 redaka koda, a pokazalo se da je bugove prilično lako pronaći. Java ima izvrsne alate za to. Da sam samo napisao kod, trebalo bi mi puno više vremena, a formatiranje bi bilo lošije kvalitete.
Zašto se nije mogla koristiti formalna specifikacija? S jedne strane, ispravna izvedba ovdje nije previše važna. Strukturalni ispisi sigurno se nikome neće svidjeti, tako da nisam morao raditi kako treba u svim čudnim situacijama. Još važnije je to što nisam imao adekvatan alat. TLA+ provjera modela ovdje je beskorisna, pa bih morao ručno pisati primjere.
Gornja specifikacija ima značajke zajedničke svim specifikacijama. Viša je razina od koda. Može se implementirati na bilo kojem jeziku. Svi alati ili metode beskorisni su za pisanje. Nikakav tečaj programiranja vam neće pomoći da napišete ovu specifikaciju. I nema alata koji bi ovu specifikaciju mogli učiniti nepotrebnom, osim ako, naravno, ne pišete jezik posebno za pisanje programa za strukturirani ispis u TLA+. Konačno, ova specifikacija ne govori ništa o tome kako ćemo točno napisati kod, ona samo navodi što ovaj kod radi. Pišemo specifikaciju da nam pomogne da razmislimo o problemu prije nego počnemo razmišljati o kodu.
Ali ova specifikacija također ima značajke koje je razlikuju od ostalih specifikacija. 95% ostalih specifikacija je znatno kraće i jednostavnije:
Nadalje, ova specifikacija je skup pravila. U pravilu, to je znak loše specifikacije. Razumijevanje posljedica skupa pravila prilično je teško, zbog čega sam morao potrošiti puno vremena na njihovo otklanjanje pogrešaka. Međutim, u ovom slučaju nisam mogao pronaći bolji način.
Vrijedi reći nekoliko riječi o programima koji se izvode kontinuirano. U pravilu rade paralelno, na primjer, operativni sustavi ili distribuirani sustavi. Vrlo malo ljudi ih može razumjeti mentalno ili na papiru, a ja nisam jedan od njih, iako sam jednom to mogao. Stoga su nam potrebni alati koji će provjeriti naš rad - na primjer, TLA + ili PlusCal.
Zašto je bilo potrebno napisati specifikaciju ako sam već znao što točno kod treba raditi? Zapravo, samo sam mislio da to znam. Osim toga, uz specifikaciju, autsajder više ne mora ulaziti u kod kako bi razumio što točno radi. Imam pravilo: ne bi trebalo biti općih pravila. Postoji iznimka od ovog pravila, naravno, to je jedino opće pravilo koje slijedim: specifikacija onoga što kod radi treba reći ljudima sve što trebaju znati kada koriste kod.
Pa što točno programeri trebaju znati o razmišljanju? Za početak, isto kao i svi ostali: ako ne pišete, onda vam se samo čini da razmišljate. Također, morate razmišljati prije nego što kodirate, što znači da morate pisati prije nego što kodirate. Specifikacija je ono što napišemo prije nego počnemo kodirati. Specifikacija je potrebna za bilo koji kôd koji svatko može koristiti ili modificirati. A taj "netko" može biti sam autor koda mjesec dana nakon što je napisan. Specifikacija je potrebna za velike programe i sustave, za klase, za metode, a ponekad čak i za složene dijelove jedne metode. Što točno treba napisati o kodu? Morate opisati što radi, odnosno što može biti korisno bilo kojoj osobi koja koristi ovaj kod. Ponekad je također potrebno navesti kako kôd ostvaruje svoju svrhu. Ako smo ovu metodu prošli u tečaju algoritama, onda je nazivamo algoritmom. Ako je nešto posebnije i novo, onda to nazivamo dizajnom na visokoj razini. Ovdje nema formalne razlike: oba su apstraktni model programa.
Kako biste točno trebali napisati specifikaciju koda? Glavna stvar: trebao bi biti jednu razinu viši od samog koda. Treba opisivati stanja i ponašanja. Trebao bi biti onoliko strog koliko zadatak zahtijeva. Ako pišete specifikaciju za implementaciju zadatka, možete je napisati u pseudokodu ili s PlusCal-om. Morate naučiti kako pisati specifikacije na formalnim specifikacijama. To će vam dati potrebne vještine koje će vam pomoći i kod neformalnih. Kako naučiti pisati formalne specifikacije? Kad smo učili programirati, pisali smo programe i zatim ispravljali pogreške u njima. Ovdje je isto: napišite specifikaciju, provjerite je alatom za provjeru modela i popravite greške. TLA+ možda nije najbolji jezik za formalnu specifikaciju, a drugi jezik će vjerojatno biti bolji za vaše specifične potrebe. Prednost TLA+ je u tome što vrlo dobro podučava matematičko razmišljanje.
Kako povezati specifikaciju i kod? Uz pomoć komentara koji povezuju matematičke pojmove i njihovu implementaciju. Ako radite s grafovima, tada ćete na razini programa imati nizove čvorova i nizove veza. Stoga morate točno napisati kako je graf implementiran ovim programskim strukturama.
Treba napomenuti da se ništa od navedenog ne odnosi na stvarni proces pisanja koda. Kada napišete kod, odnosno izvedete treći korak, također trebate razmišljati i promišljati program. Ako se ispostavi da je podzadatak složen ili neočit, trebate napisati specifikaciju za njega. Ali ovdje ne govorim o samom kodu. Možete koristiti bilo koji programski jezik, bilo koju metodologiju, ne radi se o njima. Također, ništa od navedenog ne eliminira potrebu testiranja i otklanjanja pogrešaka koda. Čak i ako je apstraktni model ispravno napisan, može biti grešaka u njegovoj implementaciji.
Pisanje specifikacija dodatni je korak u procesu kodiranja. Zahvaljujući njemu, mnoge se pogreške mogu uhvatiti s manje truda - znamo to iz iskustva programera iz Amazona. Sa specifikacijama kvaliteta programa postaje veća. Pa zašto onda tako često idemo bez njih? Jer pisanje je teško. A pisati je teško, jer za to treba misliti, a razmišljati je također teško. Uvijek je lakše glumiti ono što mislite. Ovdje možete povući analogiju s trčanjem – što manje trčite, trčite sporije. Morate trenirati mišiće i vježbati pisanje. Treba vježbati.
Specifikacija može biti netočna. Možda ste negdje pogriješili, ili su se zahtjevi promijenili, ili je možda potrebno poboljšanje. Svaki kôd koji bilo tko koristi mora se promijeniti, tako da prije ili kasnije specifikacija više neće odgovarati programu. U idealnom slučaju, u ovom slučaju morate napisati novu specifikaciju i potpuno prepisati kod. Dobro znamo da to nitko ne radi. U praksi, zakrpamo kod i eventualno ažuriramo specifikaciju. Ako će se to dogoditi prije ili kasnije, zašto onda uopće pisati specifikacije? Prvo, za osobu koja će uređivati vaš kod, svaka dodatna riječ u specifikaciji bit će zlata vrijedna, a ta osoba možete biti vi sami. Često se korim jer nisam dobio dovoljno specifikacija kada uređujem svoj kod. I pišem više specifikacija nego koda. Stoga, kada uređujete kod, specifikaciju uvijek treba ažurirati. Drugo, sa svakom revizijom kod postaje sve gori, postaje ga sve teže čitati i održavati. Ovo je povećanje entropije. Ali ako ne počnete sa specifikacijom, svaki redak koji napišete bit će uređivanje, a kod će biti nezgrapan i težak za čitanje od samog početka.
Kao što je rečeno , nijedna bitka nije dobivena planom, i nijedna bitka nije dobivena bez plana. I znao je ponešto o bitkama. Postoji mišljenje da je pisanje specifikacija gubljenje vremena. Ponekad je to istina, a zadatak je toliko jednostavan da o njemu nema što razmišljati. Ali uvijek biste trebali zapamtiti da kada vam je rečeno da ne pišete specifikacije, rečeno vam je da ne razmišljate. I o tome treba razmišljati svaki put. Razmišljanje o zadatku ne jamči da nećete pogriješiti. Kao što znamo, nitko nije izmislio čarobni štapić, a programiranje je težak zadatak. Ali ako ne razmislite o problemu, zajamčeno je da ćete pogriješiti.
Više o TLA + i PlusCal možete pročitati na posebnoj web stranici, tamo možete otići s moje početne stranice . To je sve za mene, hvala na pažnji.
Imajte na umu da je ovo prijevod. Kada pišete komentare, imajte na umu da ih autor neće čitati. Ako baš želite popričati s autorom, on će biti na konferenciji Hydra 2019 koja će se održati 11. i 12. srpnja 2019. u Sankt Peterburgu. Ulaznice se mogu kupiti .
Izvor: www.habr.com