Ovaj članak je prijevod . Ali prije nje malo upoznavanja. Kako nastaju zombiji? Svako je došao u situaciju da želi prijatelja ili kolegu da podigne na njihov nivo, ali ne ide. I ne toliko kod vas koliko kod njega „ne ide“: na jednoj strani vaga je normalna plata, zadaci i tako dalje, a na drugoj potreba za razmišljanjem. Razmišljanje je neprijatno i bolno. Brzo odustaje i nastavlja pisati kod, a da uopće ne uključuje mozak. Zamišljate koliko je truda potrebno da se savlada barijera naučene bespomoćnosti, a jednostavno to ne radite. Tako nastaju zombiji koji se, čini se, mogu izliječiti, ali čini se da to niko neće učiniti.
Kad sam to vidio (da, isti drug iz udžbenika) i ne pravi izveštaj, već sesiju pitanja i odgovora, bio sam malo oprezan. Za svaki slučaj, Leslie je svjetski poznati naučnik, autor fundamentalnih radova u distribuiranom računarstvu, a možete ga upoznati i po slovima La u riječi LaTeX – “Lamport TeX”. Drugi alarmantni faktor je njegov zahtjev: svi koji dolaze moraju (apsolutno besplatno) unaprijed saslušati nekoliko njegovih izvještaja, postaviti barem jedno pitanje o njima, pa tek onda doći. Odlučio sam da vidim šta Lamport tamo emituje - i super je! To je upravo ta stvar, čarobna pilula za liječenje zombija. Upozoravam: od teksta, ljubitelji superfleksibilnih metodologija i oni koji ne vole da testiraju napisano mogu posebno da izgore.
Nakon habrokata, naime, počinje prevođenje seminara. Uživajte u čitanju!
Koji god zadatak da preuzmete, uvijek morate 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.
Ovo se odnosi i na programiranje. Kada pišemo kod, potrebno je da:
- odlučiti šta program treba da radi;
- odrediti kako treba da obavlja svoj zadatak;
- napišite odgovarajući kod.
Poslednji korak je, naravno, veoma važan, ali neću o tome danas. Umjesto toga, razgovaraćemo o prva dva. Svaki programer ih izvodi prije početka rada. Ne sedite da pišete osim ako niste odlučili da li pišete pretraživač ili bazu podataka. Određena ideja o cilju mora biti prisutna. I definitivno razmislite šta će tačno program raditi, a ne pišite nekako u nadi da će se kod nekako pretvoriti u pretraživač.
Kako tačno dolazi do ovog kodnog prethodnog razmišljanja? Koliko truda treba da uložimo u ovo? Sve zavisi od toga koliko složen problem rešavamo. Pretpostavimo da želimo da napišemo distribuirani sistem otporan na greške. U ovom slučaju, trebali bismo dobro razmisliti o stvarima prije nego što sjednemo da kodiramo. Šta ako samo trebamo povećati cjelobrojnu varijablu za 1? Ovdje je na prvi pogled sve trivijalno i nije potrebno razmišljanje, ali onda se sjetimo da može doći do prelivanja. Stoga, čak i da biste razumjeli da li je problem jednostavan ili složen, prvo morate razmisliti.
Ako unaprijed razmislite o mogućim rješenjima problema, možete izbjeći greške. Ali ovo zahtijeva da vaše razmišljanje bude jasno. Da biste to postigli, morate zapisati svoje misli. Zaista mi se sviđa citat Dicka Guindona: “Kada pišete, priroda vam pokazuje koliko je vaše razmišljanje aljkavo.” Ako ne pišete, samo mislite da mislite. I morate zapisati svoje misli u obliku specifikacija.
Specifikacije obavljaju mnoge funkcije, posebno u velikim projektima. Ali govoriću samo o jednom od njih: pomažu nam da jasno razmišljamo. Razmišljanje jasno je veoma važno i prilično teško, pa nam je ovdje potrebna bilo kakva pomoć. Na kom jeziku da pišemo specifikacije? Generalno, ovo je uvek prvo pitanje za programere: na kom jeziku ćemo pisati. Ne postoji jedan tačan odgovor na to: problemi koje rješavamo su previše raznoliki. Za neke je TLA+ jezik specifikacije koji sam ja razvio. Za druge je zgodnije koristiti kineski. Sve zavisi od situacije.
Važnije je drugo pitanje: kako postići jasnije razmišljanje? Odgovor: Moramo razmišljati kao naučnici. Ovo je način razmišljanja koji se dokazao u proteklih 500 godina. U nauci gradimo matematičke modele stvarnosti. Astronomija je možda bila prva nauka u strogom smislu te riječi. U matematičkom modelu koji se koristi u astronomiji, nebeska tijela se pojavljuju kao tačke s masom, položajem i zamahom, iako su u stvarnosti izuzetno složeni objekti s planinama i okeanima, plimama i plimama. Ovaj model, kao i svaki drugi, stvoren je za rješavanje određenih problema. Odličan je za određivanje kamo usmjeriti teleskop ako trebate pronaći planetu. Ali ako želite predvidjeti vrijeme na ovoj planeti, ovaj model neće raditi.
Matematika nam omogućava da odredimo svojstva modela. A nauka pokazuje kako su ta svojstva povezana sa stvarnošću. Hajde da pričamo o našoj nauci, informatici. Realnost sa kojom radimo su računarski sistemi raznih vrsta: procesori, konzole za igre, računari, izvršni programi, itd. Govoriću o pokretanju programa na računaru, ali uglavnom, svi ovi zaključci važe za svaki računarski sistem. U našoj nauci koristimo mnogo različitih modela: Turingovu mašinu, djelimično uređene skupove događaja i mnoge druge.
Šta je program? Ovo je svaki kod koji se može posmatrati nezavisno. Pretpostavimo da treba da napišemo pretraživač. Izvodimo tri zadatka: dizajniramo korisnički pogled na program, zatim pišemo dijagram visokog nivoa programa i na kraju pišemo kod. Dok pišemo kod, shvaćamo da trebamo napisati formater teksta. Ovdje ponovo trebamo riješiti tri problema: odrediti koji tekst će ovaj alat vratiti; odaberite algoritam za formatiranje; napisati kod. Ovaj zadatak ima svoj podzadatak: pravilno umetnuti crticu u riječi. I ovaj podzadatak rješavamo u tri koraka - kao što vidite, ponavljaju se na više nivoa.
Razmotrimo detaljnije prvi korak: koji problem rješava program. Ovdje najčešće modeliramo program kao funkciju koja uzima neki ulaz i proizvodi neki izlaz. U matematici se funkcija obično opisuje kao uređeni skup parova. Na primjer, funkcija kvadriranja prirodnih brojeva je opisana kao skup {<0,0>, <1,1>, <2,4>, <3,9>, …}. Domen takve funkcije je skup prvih elemenata svakog para, odnosno prirodnih brojeva. Da bismo definirali funkciju, moramo specificirati njen opseg i formulu.
Ali funkcije u matematici nisu isto što i funkcije u programskim jezicima. Matematika je mnogo lakša. Pošto nemam vremena za složene primjere, razmotrimo jedan jednostavan: funkciju u C-u ili statičku metodu u Javi koja vraća najveći zajednički djelitelj dva cijela broja. U specifikaciji ove metode napisaćemo: izračunava GCD(M,N) za argumente M и Ngde GCD(M,N) - funkcija čija je domena skup parova cijelih brojeva, a povratna vrijednost je najveći cijeli broj koji je djeljiv sa M и N. Kako se ovaj model odnosi na stvarnost? Model radi na cijelim brojevima, dok u C ili Javi imamo 32-bitni int. Ovaj model nam omogućava da odlučimo da li je algoritam ispravan GCD, ali to neće spriječiti greške prelijevanja. To bi zahtijevalo složeniji model, za koji nema vremena.
Hajde da razgovaramo o ograničenjima funkcije kao modela. Neki programi (kao što su operativni sistemi) ne vraćaju samo određenu vrijednost za određene argumente, već mogu raditi kontinuirano. Osim toga, funkcija kao model nije dobro prikladna za drugi korak: planiranje kako riješiti problem. Brzo sortiranje i mjehurić sortiranje 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 je predstavljen kao skup svih dozvoljenih ponašanja, od kojih je svako, zauzvrat, niz stanja, a stanje je dodjela vrijednosti varijablama.
Hajde da vidimo kako bi izgledao drugi korak za Euklid algoritam. Moramo da izračunamo GCD(M, N). Inicijaliziramo M kako xi N kako y, zatim uzastopno oduzimajte 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]
I ako M = 0 и N = 0? Nula je djeljiva sa svim brojevima, tako da u ovom slučaju nema najvećeg djelitelja. U ovoj situaciji, moramo se vratiti na prvi korak i pitati: da li zaista trebamo 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 brojem redova koda napisanih dnevno. Ali vaš rad je mnogo korisniji ako se riješite određenog broja linija, jer imate manje mjesta za greške. A najlakši način da se riješite koda je u prvom koraku. Sasvim 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 ne bi trebalo raditi. Drugi korak je drugi potencijal za uštedu vremena. Ako mjerite produktivnost u smislu napisanih redaka, onda će vas razmišljanje o tome kako izvršiti zadatak natjerati manje produktivan, jer isti problem možete riješiti s manje koda. Ovdje ne mogu dati tačnu statistiku, jer nemam načina da izbrojim broj redova koje nisam napisao zbog činjenice da sam potrošio vrijeme na specifikaciju, odnosno na prvi i drugi korak. A eksperiment se ni ovdje ne može postaviti, jer u eksperimentu nemamo pravo završiti prvi korak, zadatak je unaprijed određen.
Lako je previdjeti mnoge poteškoće u neformalnim specifikacijama. Nema ništa teško u pisanju strogih specifikacija za funkcije, o tome neću raspravljati. Umjesto toga, razgovaraćemo o pisanju jakih specifikacija za standardna ponašanja. Postoji teorema koja kaže da se bilo koji skup ponašanja može opisati korištenjem sigurnosnog svojstva (sigurnost) i svojstva preživljavanja (živost). Sigurnost znači da se ništa loše neće dogoditi, program neće dati netačan odgovor. Preživljivost znači da će se prije ili kasnije nešto dobro dogoditi, odnosno program će prije ili kasnije dati tačan odgovor. Sigurnost je po pravilu važniji pokazatelj, tu se najčešće javljaju greš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 svaku državu. Ponašajmo se kao naučnici i matematički definišimo 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 zapisuju s prostim brojem, a varijable trenutnog stanja bez prostog broja. U slučaju Euklidovog algoritma bavit ćemo se disjunkcijom dvije formule, u jednoj od kojih x je najveća vrijednost, au drugom - y:
U prvom slučaju, nova vrijednost y jednaka je prethodnoj vrijednosti y, a novu vrijednost x dobijamo oduzimanjem manje varijable od veće varijable. U drugom slučaju radimo suprotno.
Vratimo se Euklidovom algoritmu. Pretpostavimo opet to M = 12, N = 18. Ovo definiše jedno početno stanje, (x = 12) ∧ (y = 18). Zatim te vrijednosti ubacimo u gornju formulu i dobijemo:
Evo jedinog mogućeg rješenja: x' = 18 - 12 ∧ y' = 12i dobijamo 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 poslednjem stanju [x = 6, y = 6] oba dijela izraza će biti lažna, tako da nema sljedeće stanje. Dakle, imamo potpunu specifikaciju drugog koraka - kao što vidite, ovo je sasvim obična matematika, kao kod inženjera i naučnika, a ne čudna, kao u informatici.
Ove dvije formule mogu se kombinirati u jednu formulu temporalne logike. Elegantna je i laka za objašnjenje, ali za nju sada nema vremena. Možda nam je potrebna vremenska logika samo za svojstvo živosti, nije potrebna za sigurnost. Ne volim vremensku logiku kao takvu, nije baš obična matematika, ali u slučaju živosti je nužno zlo.
U Euklidovom algoritmu, za svaku vrijednost x и y imaju jedinstvene vrijednosti x' и y', što čini relaciju sa sljedećim stanjem istinitim. Drugim riječima, Euklidov algoritam je deterministički. Da bi se modelirao nedeterministički algoritam, trenutno stanje treba da ima više mogućih budućih stanja i da svaka neprimirana vrijednost varijable ima višestruke vrijednosti varijable, tako da je odnos prema sljedećem stanju istinit. To je lako učiniti, ali neću sada navoditi 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, npr. . Specifikacija Euklidovog algoritma bi na ovom jeziku izgledala ovako:
Simbol znaka jednakosti sa trouglom znači 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. U specifikaciju u TLA+, morate dodati deklaracije i neku sintaksu, kao na gornjoj slici. U ASCII-u bi to izgledalo ovako:
Kao što vidite, ništa komplikovano. Specifikacija za TLA+ se može 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 efikasna i jednostavna metoda verifikacije koja je potpuno automatska. Moguće je i pisati formalne dokaze istinitosti i mehanički ih provjeriti, ali to oduzima dosta vremena, tako da to gotovo niko ne radi.
Glavni nedostatak TLA+ je to što je matematika, a programeri i informatičari se boje matematike. Na prvi pogled ovo zvuči kao šala, ali, nažalost, mislim ozbiljno. Moj kolega mi je upravo pričao kako je pokušao objasniti TLA+ nekoliko programera. Čim su se formule pojavile na ekranu, odmah su postale staklene oči. Dakle, ako vas TLA+ plaši, možete koristiti , to je neka vrsta programskog jezika igračke. Izraz u PlusCal-u može biti bilo koji TLA+ izraz, odnosno, 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, ova specifikacija se može provjeriti pomoću TLA+ alata. Sve u svemu, PlusCal može pomoći u prevladavanju fobije od matematike i lak je za razumijevanje čak i programerima i kompjuterskim naučnicima. U prošlosti sam na njemu objavljivao algoritme neko vrijeme (oko 10 godina).
Možda će neko prigovoriti da su TLA + i PlusCal matematika, a matematika radi samo na izmišljenim primjerima. U praksi vam je potreban pravi jezik sa tipovima, procedurama, objektima i tako dalje. Ovo je pogrešno. Evo šta piše Chris Newcomb, koji je radio u Amazonu: „Koristili smo TLA+ na deset velikih projekata, i u svakom slučaju je napravio značajnu razliku u razvoju jer smo bili u mogućnosti da uhvatimo opasne greške prije nego što smo započeli proizvodnju i zato što nam je dao uvid i samopouzdanje koji su nam bili potrebni za agresivne performanse. optimizacije bez uticaja na istinitost programa". Često možete čuti da kada se koriste formalne metode dobijamo neefikasan 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 se sada jako trude da napišu specifikacije za TLA+, i posebno odvoje vrijeme za ovo“. Dakle, kada menadžeri vide da TLA+ radi, rado to prihvataju. Chris Newcomb je ovo napisao prije otprilike šest mjeseci (oktobar 2014.), ali sada, koliko ja znam, TLA+ se koristi u 14 projekata, a ne u 10. Drugi primjer je u dizajnu XBoxa 360. Stažist je došao kod Charlesa Thackera i napisao specifikaciju za memorijski sistem. Zahvaljujući ovoj specifikaciji pronađena je greška koja bi inače prošla nezapaženo, a zbog koje bi svaki XBox 360 pao nakon četiri sata korištenja. IBM-ovi inženjeri su potvrdili da njihovi testovi ne bi pronašli ovu grešku.
Više o TLA + možete pročitati na Internetu, ali sada hajde da pričamo o neformalnim specifikacijama. Rijetko moramo pisati programe koji izračunavaju najmanji zajednički djelitelj i slično. Mnogo češće pišemo programe poput alata za lijepi štampač koji sam napisao za TLA+. Nakon najjednostavnije obrade, TLA + kod bi izgledao ovako:
Ali u gornjem primjeru, korisnik je najvjerovatnije želio da se konjunkcija i znak jednakosti poravnaju. Dakle, ispravno formatiranje bi izgledalo više ovako:
Razmotrimo još jedan primer:
Ovdje je, naprotiv, poravnanje predznaka jednakosti, sabiranja i množenja u izvoru bilo nasumično, pa je najjednostavnija obrada sasvim dovoljna. Općenito, ne postoji tač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 šta program treba da radi ne znači da ne treba da razmišljamo o tome kako funkcioniše – naprotiv, moramo da uložimo još više truda u to. Ovdje je posebno važna specifikacija. Nemoguće je odrediti optimalan program za strukturirano štampanje, ali to ne znači da ga uopće ne treba uzimati, a pisanje koda kao toka svijesti nije dobra stvar. Na kraju sam napisao specifikaciju od šest pravila sa definicijama u obliku komentara u java fajlu. 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: LeftComment aligned, left-comment и covering token - pojmovi sa definicijama. Ovako matematičari opisuju matematiku: pišu definicije pojmova i, na osnovu njih, pravila. Prednost takve specifikacije je što je šest pravila mnogo lakše razumjeti i otkloniti greške od 850 linija koda. Moram reći da pisanje ovih pravila nije bilo lako, trebalo je dosta vremena za njihovo otklanjanje grešaka. Posebno u tu svrhu napisao sam kod koji je prijavio koje je pravilo korišteno. Zahvaljujući činjenici da sam testirao ovih šest pravila na nekoliko primjera, nisam morao otklanjati greške u 850 linija koda, a pokazalo se da je greške prilično lako pronaći. Java ima odlične alate za ovo. Da sam samo napisao kod, trebalo bi mi mnogo duže, a formatiranje bi bilo lošijeg kvaliteta.
Zašto se nije mogla koristiti formalna specifikacija? S jedne strane, ispravno izvođenje ovdje nije previše važno. Strukturalni ispisi se sigurno neće svidjeti nikome, tako da nisam morao da ga natjeram da radi kako treba u svim čudnim situacijama. Još važnija je činjenica da nisam imao adekvatne alate. Provjera TLA+ modela ovdje je beskorisna, pa bih morao ručno pisati primjere.
Gore navedena specifikacija ima karakteristike zajedničke svim specifikacijama. To je viši nivo od koda. Može se implementirati na bilo kojem jeziku. Bilo koji alat ili metode su beskorisni za pisanje. Nijedan kurs programiranja vam neće pomoći da napišete ovu specifikaciju. I ne postoje alati koji bi ovu specifikaciju mogli učiniti nepotrebnom, osim ako, naravno, ne pišete jezik posebno za pisanje strukturiranih programa za štampanje u TLA+. Konačno, ova specifikacija ne govori ništa o tome kako ćemo tačno napisati kod, već samo navodi šta 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 karakteristike koje je razlikuju od ostalih specifikacija. 95% ostalih specifikacija je znatno kraće i jednostavnije:
Nadalje, ova specifikacija je skup pravila. Po pravilu, ovo je znak loše specifikacije. Razumevanje posledica skupa pravila je prilično teško, zbog čega sam morao da potrošim dosta vremena na njihovo otklanjanje grešaka. Međutim, u ovom slučaju nisam mogao pronaći bolji način.
Vrijedi reći nekoliko riječi o programima koji rade kontinuirano. U pravilu rade paralelno, na primjer, operativni sistemi ili distribuirani sistemi. Vrlo malo ljudi ih može razumjeti mentalno ili na papiru, a ja nisam jedan od njih, iako sam to nekada mogao. Stoga su nam potrebni alati koji će provjeriti naš rad - na primjer, TLA + ili PlusCal.
Zašto je bilo potrebno pisati specifikaciju ako sam već znao šta tačno kod treba da radi? U stvari, samo sam mislio da znam. Osim toga, sa specifikacijom, autsajder više ne mora ulaziti u kod da bi shvatio šta tačno radi. Imam pravilo: ne bi trebalo da postoje opšta pravila. Postoji izuzetak od ovog pravila, naravno, to je jedino opšte pravilo koje se pridržavam: specifikacija onoga što kod radi treba da kaže ljudima sve što treba da znaju kada koriste kod.
Dakle, šta tačno programeri treba da znaju o razmišljanju? Za početak, isto kao i svi ostali: ako ne pišeš, onda ti se samo čini da razmišljaš. Također, morate razmišljati prije nego što kodirate, što znači da morate pisati prije nego što kodirate. Specifikacija je ono što pišemo prije nego što počnemo s kodiranjem. Specifikacija je potrebna za svaki kod koji bilo ko može koristiti ili modificirati. A taj "neko" je možda i sam autor koda mesec dana nakon što je napisan. Specifikacija je potrebna za velike programe i sisteme, za klase, za metode, a ponekad čak i za složene dijelove jedne metode. Šta tačno treba napisati o kodu? Morate opisati šta radi, odnosno šta može biti korisno bilo kojoj osobi koja koristi ovaj kod. Ponekad će takođe biti potrebno navesti kako kod ostvaruje svoju svrhu. Ako smo kroz ovu metodu prošli kroz algoritame, onda je nazivamo algoritamom. Ako je to nešto posebnije i novo, onda to nazivamo dizajnom na visokom nivou. Ovdje nema formalne razlike: oba su apstraktni model programa.
Kako tačno treba napisati specifikaciju koda? Glavna stvar: trebao bi biti jedan nivo viši od samog koda. Trebalo bi da opisuje stanja i ponašanja. Trebalo bi da bude strogo onoliko koliko zadatak zahtijeva. Ako pišete specifikaciju o tome kako će se zadatak implementirati, možete je napisati u pseudokodu ili uz PlusCal. Morate naučiti kako napisati specifikacije na formalnim specifikacijama. Ovo će vam dati potrebne vještine koje će vam pomoći i sa neformalnim. Kako naučiti pisati formalne specifikacije? Kada smo naučili programirati, napisali smo programe i potom ih otklonili. Ovdje je isto: napišite specifikaciju, provjerite je pomoću provjere modela i popravite greške. TLA+ možda nije najbolji jezik za formalnu specifikaciju, a neki drugi jezik će vjerovatno 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 koncepte i njihovu implementaciju. Ako radite sa grafovima, tada ćete na nivou programa imati nizove čvorova i nizove veza. Stoga, morate točno napisati kako se graf implementira od strane ovih programskih struktura.
Treba napomenuti da se ništa od gore navedenog ne odnosi na stvarni proces pisanja koda. Kada pišete kod, odnosno izvodite treći korak, također morate razmišljati i razmišljati kroz program. Ako se pokaže da je podzadatak složen ili neočigledan, morate 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đe, ništa od gore navedenog ne eliminiše potrebu za testiranjem i otklanjanjem grešaka koda. Čak i ako je apstraktni model ispravno napisan, mogu postojati greške u njegovoj implementaciji.
Pisanje specifikacija je dodatni korak u procesu kodiranja. Zahvaljujući njemu, mnoge greške se mogu uhvatiti uz manje truda - to znamo iz iskustva programera iz Amazona. Sa specifikacijama, kvalitet programa postaje veći. Pa zašto onda tako često idemo bez njih? Jer pisanje je teško. A pisati je teško, jer za ovo treba razmišljati, a i razmišljanje je teško. Uvek je lakše pretvarati se šta misliš. Ovdje možete povući analogiju s trčanjem – što manje trčite, to sporije trčite. Morate trenirati mišiće i vježbati pisanje. Treba praksa.
Specifikacija može biti netačna. Možda ste negdje pogriješili, ili su se zahtjevi možda promijenili, ili je možda potrebno poboljšati. Svaki kod koji bilo ko koristi mora se promijeniti, tako da prije ili kasnije specifikacija više neće odgovarati programu. U idealnom slučaju, u ovom slučaju, trebate napisati novu specifikaciju i potpuno prepisati kod. Znamo dobro da to niko ne radi. U praksi, zakrpimo 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 grdim što 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 se pogoršava, postaje sve teži za čitanje i održavanje. Ovo je povećanje entropije. Ali ako ne počnete sa specifikacijom, onda će svaki red koji napišete biti izmjena, a kod će biti glomazan i teško čitljiv od samog početka.
Kao što je rečeno , nijedna bitka nije dobijena po planu, niti jedna bitka nije dobijena 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 nema o čemu razmišljati. Ali uvijek treba imati na umu da kada vam se kaže da ne pišete specifikacije, rečeno vam je da ne razmišljate. I svaki put treba razmišljati o tome. Razmišljanje o zadatku ne garantuje da nećete pogrešiti. Kao što znamo, niko nije izmislio čarobni štapić, a programiranje je težak zadatak. Ali ako ne razmislite o problemu, zagarantovano ćete pogriješiti.
Više o TLA + i PlusCal-u 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 zaista želite da razgovarate sa autorom, onda će on biti na konferenciji Hydra 2019, koja će se održati od 11. do 12. jula 2019. u Sankt Peterburgu. Ulaznice se mogu kupiti .
izvor: www.habr.com