To je članek-prevod . Pred njim pa je kratek uvod. Kako nastajajo zombiji? Vsakdo se je kdaj znašel v situaciji, ko želi popeljati prijatelja ali sodelavca na svojo raven, a mu to ne uspe. Pri tem 'ne uspe' ni toliko tvoja krivda, kot njegova: na eni strani tehtnice je normalna plača, naloge itd., na drugi pa potreba po razmišljanju. Razmišljanje je neprijetno in boleče. Hitro se preda in nadaljuje s pisanjem kode, ne da bi vključil možgane. Si predstavljaš, koliko truda je potrebno, da prebrodiš oviro naučene brezmoči, in tega preprosto ne storiš. Tako nastajajo zombiji, ki jih lahko zdravimo, a nihče se s tem ne bo ukvarjal.
Ko sem videl, da (da-da, tisti znani tovariš iz učbenikov) in ne bo imel predavanja, temveč sejo vprašanj in odgovorov, sem bil malo previden. Da za vsak slučaj pojasnim, Leslie je svetovno znan znanstvenik, avtor temeljnih del na področju porazdeljenega računalništva, ter ga morda poznate po črkah La v besedi LaTeX - 'Lamport TeX'. Drug zaskrbljujoč dejavnik je njegova zahteva: vsakdo, ki pride, mora (popolnoma brezplačno) vnaprej prisluhniti dvema njegovima predavanjema, postaviti vsaj eno vprašanje in le potem priti na sejo. Odločil sem se, da pogledam, kaj tam Lamport govori - in to je čudovito! To je točno to, čarobna povezava-tableta za zdravljenje zombijev. Opozorim: besedilo lahko precej razjezi ljubitelje superfleksibilnih metodologij in tiste, ki ne marajo testirati napisanega.
Po hibridnem pogovoru se začne prevod seminarja. Prijetno branje!
Ne glede na to, katero nalogo se lotite, vedno morate preiti tri korake:
- določiti, kakšnega cilja želite doseči;
- odločiti se, kako boste dosegli svoj cilj;
- priti do svojega cilja.
To velja tudi za programiranje. Ko pišemo kodo, moramo:
- določiti, kaj naj bi program počel;
- opredeliti, kako naj bi izpolnil svojo nalogo;
- napiši ustrezno kodo.
Zadnji korak je, seveda, zelo pomemben, vendar o njem danes ne bom govoril. Namesto tega bomo razpravljali o prvih dveh. Ti sta opravila vsak programer, preden začne delati. Ne sedite pisati, če niste odločili, kaj točno pišete: brskalnik ali bazo podatkov. Določena predstava o cilju mora nujno biti prisotna. In seveda premislite, kaj točno bo program počel, ne da bi samo pisali na slepo v upanju, da se bo koda nekako spremenila v brskalnik.
Kako natančno poteka to predhodno razmišljanje o kodi? Koliko truda moramo temu nameniti? Vse je odvisno od tega, kako zapleten problem rešujemo. Recimo, da želimo napisati odpornost na napake distribucijskega sistema. V tem primeru moramo vse temeljito premisliti, preden se lotimo kode. A če moramo samo povečati celo število za 1? Na prvi pogled je vse banally preprosto in tu ni potrebe po razmišljanju, toda nato se spomnimo, da lahko pride do prelivanja. Zato je tudi za razumevanje, ali je problem preprost ali zapleten — najprej treba razmisliti.
Če predhodno premislite možne rešitve problema, se lahko izognete napakam. A za to je potrebno, da je vaše razmišljanje jasno. Da bi to dosegli, morate zapisovati svoje misli. Zelo mi je všeč citat Dika Gindona: „Ko pišete, narava vam pokaže, kako zanemarjeno je vaše razmišljanje.“ Če ne pišete, se vam le zdi, da mislite. In misli je treba zapisovati v obliki specifikacij.
Specifikacije opravljajo številne funkcije, še posebej pri večjih projektih. A govoril bom le o eni izmed njih: pomagajo nam jasno razmišljati. Jasno razmišljanje je zelo pomembno in dokaj težko, zato potrebujemo vsako oporo. V katerem jeziku naj pišemo specifikacije? To je pravzaprav vedno prvo vprašanje za programerje: v katerem jeziku bomo pisali. Ni enega pravilnega odgovora na to: problemi, ki jih rešujemo, so preveč raznoliki. Za nekatere je koristen TLA+ — to je jezik specifikacij, ki sem ga razvil. Za druge je bolj praktično uporabljati kitajski. Vse je odvisno od situacije.
Pomembnejše vprašanje je: kako doseči jasnejše mišljenje? Odgovor: razmišljati moramo kot znanstveniki. To je način razmišljanja, ki se je izkazal za zelo učinkovit v zadnjih 500 letih. V znanosti gradimo matematične modele resničnosti. Astronomija je bila verjetno prva znanost v svojem strogo pomenu. V matematičnem modelu, ki se uporablja v astronomiji, se nebesna telesa pojavijo kot točke z maso, položajem in gibanjem, medtem ko so v resnici zelo zapleteni objekti z gorami in oceani, plimovanjem in osekom. Ta model, tako kot vsak drug, je ustvarjen za reševanje določenih nalog. Odlično se obnese, da določimo, kam usmeriti teleskop, če želimo najti planet. Toda če želite napovedati vreme na tem planetu, ta model ne bo primern.
Matematika nam omogoča, da določimo lastnosti modela. In znanost pokaže, kako te lastnosti ustrezajo resničnosti. Pogovorimo se o naši znanosti, računalništvu. Resničnost, s katero delamo, so računalniški sistemi najrazličnejših vrst: procesorji, igralne konzole, računalniki, ki izvajajo programe in tako naprej. Govoril bom o izvajanju programa na računalniku, vendar so te ugotovitve na splošno uporabne za vsak računalniški sistem. V naši znanosti uporabljamo številne različne modele: Turingova naprava, delno urejene množice dogodkov in mnoge druge.
Kaj je program? To je vsak koda, ki jo lahko obravnavamo samostojno. Recimo, da moramo napisati brskalnik. Izvajamo tri naloge: načrtujemo predstavitev programa za uporabnika, nato napišemo visoko raven sheme programa in na koncu napišemo kodo. Med pisanjem kode se zavedamo, da moramo napisati sredstvo za oblikovanje besedila. Tukaj moramo ponovno rešiti tri naloge: določiti, kateri besedilo bo to sredstvo vrnilo; izbrati algoritem za oblikovanje; napisati kodo. Ta naloga ima svojo podnalogo: pravilno vstavljanje pomožnih črk v besede. To podnalogo prav tako rešujemo v treh korakih — kot vidimo, se ti ponovno pojavljajo na mnogih ravneh.
Poglejmo podrobneje prvi korak: kakšno nalogo rešuje program. Tukaj program običajno modeliramo kot funkcijo, ki prejme določene vhodne podatke in vrne določene izhodne podatke. V matematiki je funkcija običajno opisana kot urejen množični par. Na primer, funkcija kvadriranja naravnih števil je opisana kot množica {, , , , …}. Območje opredelitve te funkcije je množica prvih elementov vsakega para, torej naravna števila. Da bi opredelili funkcijo, moramo navesti njeno območje opredelitve in formulo.
A vendar funkcije v matem umetnosti niso enake funkcijam v programskih jezikih. Matematika je precej preprostejša. Ker nimam časa za zapletene primere, poglejmo preprost: funkcija v jeziku C ali statična metoda v Javi, ki vrne največji skupni delitelj dveh celih števil. V specifikaciji te metode bomo zapisali: izračuna GCD(M,N) za argumente У in N, gde GCD(M,N) — funkcija, katere območje opredelitve je množica parov celih števil, vrnjena vrednost pa je največje celo število, ki deli У in N. Kako se ta model povezuje z realnostjo? Model deluje s celimi številkami, medtem ko imamo v C ali Javi 32-bitno int. Ta model nam omogoča, da ugotovimo, ali je algoritem GCD, vendar ne preprečuje napak zaradi prelivanja. Za to bi potrebovali bolj zapleten model, za katerega ni časa.
Pogovorimo se o omejitvah funkcije kot modela. Delo nekaterih programov (na primer operacijskih sistemov) ni omejeno na vrnitev določenega rezultata za določene argumente, lahko delujejo neprekinjeno. Poleg tega funkcija kot model slabo ustreza drugemu koraku: načrtovanju načina reševanja naloge. Hitro razvrščanje in mehurčno razvrščanje izračunata isto funkcijo, vendar sta to popolnoma različni algoritemski postopki. Zato za opis načina doseganja cilja programa uporabljam drug model, poimenovan standardni vedenjski model. V njem je program predstavljen kot množica vseh dopustnih vedenj, od katerih je vsako zaporedje stanj, stanje pa je dodelitev vrednosti spremenljivkam.
Poglejmo, kako bo izgledal drugi korak algoritma Evklid. Moramo izračunati GCD(M, N). Inicializirali bomo У kako x, a N kako y, nato pa od večje vrednosti odštejemo manjšo, dokler se ne izenačita. Na primer, če M = 12, a N = 18, lahko opišemo naslednje vedenje:
[x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6]
In če je M = 0 in N = 0? Ноль делится на все числа, поэтому наибольшего делителя в этом случае нет. В этой ситуации нам нужно вернуться к первому шагу и спросить: действительно ли нам нужно вычислять НОД для неположительных чисел? Если в этом нет необходимости, то нужно просто изменить спецификацию.
Tukaj je treba narediti majhen odklon od produktivnosti. Ta se pogosto meri s številom napisanih vrstic kode na dan. Vendar je vaše delo bistveno bolj koristno, če ste se znebili določenega števila vrstic, ker imate manj prostora za napake. Najlažje se znebiti kode prav v prvem koraku. Zelo možno je, da preprosto ne potrebujete vseh tistih funkcionalnosti, ki jih skušate uresničiti. Najhitrejši način za poenostavitev programa in prihranitev časa je, da ne izvajate stvari, ki jih ni treba izvajati. Drugi korak je drugi po potencialu za prihranek časa. Če produktivnost merite v številu napisanih vrstic, potem vam bo razmišljanje o tem, kako izvesti nalogo, naredilo manj produktivne, saj boste isto nalogo lahko rešili z manjšim obsegom kode. Natančne statistike tukaj ne morem posredovati, ker nimam načina, da preštejem to število vrstic, ki jih nisem napisal, ker sem porabil čas za specifikacijo, torej na prvih dveh korakih. In eksperiment tudi tukaj ni mogoč, ker v eksperimentu ne smemo izvesti prvega koraka, naloga je vnaprej določena.
Pri neformalnih specifikacijah je lahko enostavno spregledati številne težave. Nič zapletenega ni pri pisanju strogo določenih specifikacij za funkcije, o tem ne bom razpravljal. Namesto tega se bomo pogovarjali o pisanju strogih specifikacij za standardne vedenjske modele. Obstaja teorema, ki pravi, da je možno katerokoli množico vedenj opisati s svojstvom varnosti (safety) in lastnostjo oživljanja (liveness). Varnost pomeni, da se ne bo zgodilo nič slabega, program ne bo dal napačnega odgovora. Živahnost pomeni, da se рано ali позно zgodi nekaj dobrega, tj. program bo рано ali позно dal pravilen odgovor. Kot pravilo je varnost pomembnejši kazalnik, napake se največkrat pojavijo prav tukaj. Zato, da prihranimo čas, ne bom govoril o živahnosti, čeprav je ta seveda prav tako pomembna.
Dosegamo varnost s tem, da najprej napišemo številna možna izhodiščna stanja. In drugič, odnose z vsemi mogočimi naslednjimi stanjami za vsako stanje. Obnašali se bomo kot znanstveniki in stanja definirali matematično. Skupina izhodiščnih stanj je opisana s formulo, na primer, v primeru Evklidovega algoritma: (x = M) ∧ (y = N). Za določene vrednosti У in N obstaja samo eno izhodiščno stanje. Odnose z naslednjim stanjem opisujemo s formulo, v kateri so spremenljivke naslednjega stanja zapisane s poševnico, trenutnega stanja pa brez. V primeru Evklidovega algoritma se bomo ukvarjali z disjunkcijo dveh formul, od katerih je ena x največja vrednost, druga pa y:
V prvem primeru je nova vrednost y enaka prejšnji vrednosti y, nova vrednost x pa dobimo tako, da od večje spremenljivke odštejemo manjšo. V drugem primeru naredimo obratno.
Vrnimo se k Evklidovemu algoritmu. Spet domnevajmo, da M = 12, N = 18. To določa edino izhodiščno stanje, (x = 12) ∧ (y = 18). Nato te vrednosti vstavimo v zgoraj omenjeno formulo in dobimo:
Tu je edina mogoča rešitev: x' = 18 - 12 ∧ y' = 12, in dobimo obnašanje: [x = 12, y = 18]. Tudi tako lahko opišemo vsa stanja v našem obnašanju: [x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6].
V zadnjem stanju [x = 6, y = 6] bosta obe deli izraza lažni, kar pomeni, da naslednjega stanja ni. Tako imamo popolno specifikacijo drugega koraka — kot vidimo, je to povsem običajna matematika, kot pri inženirjih in znanstvenikih, in ne nenavadna, kot v računalniških znanostih.
Ti dve formuli można združit' v eno formulo temporalne logike. Elegantna je in preveriti jo ni težko, vendar za to trenutno ni časa. Temporalna logika nam lahko pride prav samo za lastnost živosti, za varnost ni potrebna. Sama temporalna logika ni všeč, ni povsem običajna matematika, a v primeru živosti je nujno zlo.
V Evklidovem algoritmu za vsak vrednost x in y obstajajo edinstvene vrednosti x' in y', ki naredijo razmerje s naslednjim stanjem resnično. Drugače povedano, Evklidov algoritem je determinističen. Da bi modelirali nedeterminističen algoritem, mora imeti trenutno stanje več mogočih prihodnjih stanj, in vsak vrednost spremenljivke brez nagiba mora imeti več vrednosti spremenljivke z nagibom, pri katerih je razmerje z naslednjim stanjem resnično. To ni težko narediti, vendar zdaj ne bom podajal primerov.
Da bi izdelali delovno orodje, potrebujemo formalno matematiko. Kako narediti specifikacijo formalno? Za to bomo potrebovali formalen jezik, na primer, . Specifikacija Evklidovega algoritma bo v tem jeziku izgledala takole:
Simbol znaka enakosti s trikotnikom pomeni, da je vrednost levo od znaka definirana kot enaka vrednosti desno od znaka. V bistvu je specifikacija definicija, v našem primeru dve definiciji. K specifikaciji v TLA+ je treba dodati deklaracije in nekakšno sintakso, kot je na sliki zgoraj. V ASCII bi to izgledalo tako:
Kot vidimo, ni nič zapletenega. Specifikacijo v TLA+ lahko preverimo, tj. obhodimo vseh mogočih vedenj v majhnem modelu. V našem primeru bo ta model določene vrednosti У in N. To je zelo učinkovit in preprost način preverjanja, ki se v celoti izvede avtomatsko. Poleg tega je mogoče napisati formalne dokaze o resničnosti in jih preveriti mehanično, vendar to zahteva veliko časa, zato tega skoraj nihče ne počne.
Glavni nedostatak TLA+ je taj što je to matematika, a programeri i računalni naučnici se plaše matematike. Na prvi pogled ovo zvuči kao šala, ali, nažalost, govorim to sasvim ozbiljno. Moj kolega mi je nedavno pričao kako je pokušao objasniti TLA+ nekoliko programerima. Čim su na ekranu ugledali formule, odmah su dobili staklasti pogled. Dakle, ako TLA+ deluje zastrašujuće, može se koristiti , to je neka vrsta igračke programski jezik. Izraz u PlusCal može biti bilo koji izraz TLA+, odnosno, u suštini, bilo koji matematički izraz. Pored toga, PlusCal ima sintaksu za nedeterminističke algoritme. S obzirom na to da se u PlusCal može zabeležiti bilo koji izraz TLA+, on je znatno izražajniji od bilo kog stvarnog programskog jezika. Nadalje, PlusCal se kompilira u lako čitljivu specifikaciju TLA+. To ne znači, naravno, da će se složena specifikacija PlusCal pretvoriti u jednostavnu na TLA+ — prosto je očigledno da postoji podudarnost između njih, neće biti dodatne složenosti. Na kraju, ovu specifikaciju će biti moguće proveriti alatima TLA+. U suštini, PlusCal može pomoći u prevazilaženju fobije od matematike, lako ga mogu razumeti čak i programeri i računalni naučnici. Nekoliko godina sam objavljivao algoritme napisane u njemu.
Možda će neko prigovoriti da su TLA+ i PlusCal matematika, a da matematika funkcioniše samo na izmišljenim primerima. U praksi je potreban pravi jezik sa tipovima, procedurama, objektima i tako dalje. To nije tačno. Evo šta kaže Kris Njukomb, koji je radio u Amazonu: „Koristili smo TLA+ u deset velikih projekata, i u svakom slučaju je njegovo korišćenje značajno doprinelo razvoju, jer smo uspeli da uhvatimo opasne greške pre nego što su se pojavile u proizvodnji, i jer nam je to dalo razumevanje i samopouzdanje potrebno za agresivne optimizacije performansi koje ne utiču na istinitost programa“. Često se može čuti da korišćenjem formalnih metoda dobijamo neefikasan kod — u praksi je upravo obrnuto. Pored toga, postoji mišljenje da menadžere nije moguće uveriti u potrebu formalnih metoda, čak i kada su programeri uvereni u njihovu korisnost. A Njukomb piše: „Menadžeri sada sve više podstiču da se pišu specifikacije na TLA+, i posebno izdvajaju vreme za to“. Tako da kada menadžeri vide da TLA+ funkcioniše, rado ga prihvataju. Kris Njukomb je to napisao pre otprilike šest meseci (u oktobru 2014. godine), a sada, koliko ja znam, TLA+ se koristi u 14 projekata, a ne 10. Drugi primer se odnosi na projektovanje XBox 360. Čarls Tekker je dobio stagista koji je napisao specifikaciju za sistem memorije. Zahvaljujući ovoj specifikaciji otkrivena je greška koja inače ne bi bila primećena, a zbog koje bi svaka XBox 360 padala posle četiri sata korišćenja. Inženjeri iz IBM-a su potvrdili da njihovi testovi ne bi otkrili tu grešku.
Detaljnije o TLA+ možete pročitati na internetu, a sada hajde da pričamo o neformalnim specifikacijama. Retko pišemo programe koji izračunavaju najveći zajednički delilac i slično. Često pišemo programe poput alata za formatiranje (pretty-printer), koji sam napisao za TLA+. Nakon najjednostavnijeg formatiranja, kod na TLA+ bi izgledao ovako:
Ali u datom primeru korisnik je verovatno želeo da su znaci konjunkcije i jednakosti poravnati. Tako da je ispravno formatiranje verovatno ovako:
Razmotrimo drugi primer:
Ovde, naprotiv, poravnanje znakova jednakosti, sabiranja i množenja u izvoru je bilo nasumično, pa je najjednostavnije formatiranje sasvim dovoljno. U suštini, ne postoji tačna matematička definicija ispravnog formatiranja, jer „ispravno“ u ovom slučaju znači „onako kako korisnik želi“, a to se matematički ne može definisati.
Naizgled, ako nemamo definiciju istinitosti, onda je specifikacija beskorisna. Ali to nije tako. Ako ne znamo šta tačno program treba da uradi, to ne znači da ne treba da razmišljamo o njegovom radu — naprotiv, trebamo uložiti još više truda u to. Specifikacija je ovde posebno važna. Teško je odrediti optimalan program za formatiranje, ali to ne znači da se ne bi trebali njome baviti. Pisanje koda kao tok svesti nije rešenje. Na kraju sam napisao specifikaciju od šest pravila sa definicijama u obliku komentara v datoteki Java. Tukaj je primer enega od pravil: token za levo pripombo je LeftComment, usklajen s svojim pokrivnim tokenom. To pravilo je napisano v, recimo, matematičnem angleščini: LeftComment usklajen, levo-komentar in pokrovni token — termini z definicijami. To je način, kako matematik opisuje matematiko: piše definicije terminov in na podlagi njih — pravila. Korist te specifikacije je, da je razumevanje in odpravljanje napak pri šestih pravilih bistveno lažje kot pri 850 vrsticah kode. Moram reči, da pisanje teh pravil ni bilo enostavno, precej časa je bilo potrebnega za njihovo odpravljanje napak. Posebej za to sem napisal kodo, ki je poročala, katero pravilo se uporablja. Ker sem ta šest pravil preveril na več primerih, mi ni bilo treba odpravljati 850 vrstic kode, napake pa so bile precej enostavne za odkriti. V Javi obstajajo odlična orodja za to. Če bi samo napisal kodo, bi mi vzelo znatno več časa, in oblikovanje bi bilo slabše.
Zakaj ne bi bilo mogoče uporabiti formalne specifikacije? Po eni strani, pravilnost izvedbe tu ni tako pomembna. Strukturno tiskanje bo zagotovo nekomu neprijetno, tako da mi ni bilo treba doseči pravilnega delovanja v vseh nenavadnih situacijah. Še pomembnejše je, da nisem imel ustreznih orodij. Orodje za preverjanje modelov TLA+ je tukaj brez pomena, tako da bi moral ročno pisati primere.
Z navedeno specifikacijo so nekatere značilnosti skupne vsem specifikacijam. Je višje ravni od kode. Uvesti jo je mogoče v katerem koli jeziku. Pri njenem pisanju so kakršna koli orodja ali metode brez pomena. Noben programerski tečaj vam ne more pomagati pri pisanju te specifikacije. In ne obstajajo orodja, ki bi lahko naredila to specifikacijo odvečno, razen če ne pišete jezika posebej za pisanje programov za strukturno tiskanje v TLA+. Na koncu, ta specifikacija ne govori nič o tem, kako bomo točno napisali kodo, zgolj navaja, kaj ta koda počne. Specifikacijo pišemo, da si pomagamo premisliti problem, preden začnemo razmišljati o kodi.
Ampak ta specifikacija ima tudi posebnosti, ki jo ločijo od drugih specifikacij. 95% drugih specifikacij je bistveno krajših in preprostejših:
Zatem ta specifikacija je niz pravil. Na splošno je to znak slabe specifikacije. Razumeti posledice niza pravil je precej težko, zato sem porabil veliko časa za njihovo odpravljanje. Kljub temu v tem primeru nisem našel boljšega načina.
Ustrezno je nekaj besed o programih, ki delujejo neprekinjeno. Na splošno delujejo vzporedno, na primer operacijski sistemi ali distribuirani sistemi. Zanje se lahko v mislih ali na papirju zelo malo ljudi znajde, in jaz ne spadam med njih, čeprav sem nekoč znal. Zato so potrebna orodja, ki bodo preverila naše delo — na primer TLA+ ali PlusCal.
Zakaj je bilo treba napisati specifikacijo, če sem že vedel, kaj naj bi koda počela? V resnici se mi je samo zdelo, da to vem. Poleg tega ob prisotnosti specifikacije ni treba, da nekdo drug poseže v kodo, da bi razumel, kaj dejansko počne. Imam pravilo: ne sme biti nobenih splošnih pravil. To pravilo ima seveda izjemo, to je edino splošno pravilo, ki ga upoštevam: specifikacija tega, kar koda počne, mora ljudem sporočiti vse, kar morajo vedeti pri uporabi te kode.
Kaj natančno morajo programerji vedeti o razmišljanju? Najprej to, kar velja za vse: če ne pišeš, imaš le občutek, da razmišljaš. Poleg tega je treba razmišljati, preden začneš kodirati, kar pomeni, da je treba pisati, preden kodiraš. Specifikacija je tisto, kar napišemo pred začetkom kodiranja. Specifikacija je potrebna za vsak kodo, ki jo lahko uporabi ali spremeni kdorkoli. In ta 'kdorkoli' je lahko sam avtor kode čez mesec dni po njenem pisanju. Specifikacija je potrebna za velike programe in sisteme, razrede, metode in včasih celo za zapleteni odsek posamezne metode. Kaj točno je treba pisati o kodi? Treba je opisati, kaj počne, torej tisto, kar bi bilo lahko koristno katerikoli osebi, ki uporablja to kodo. Včasih je morda potrebno tudi navesti, kako točno koda doseže svoj cilj. Če smo to metodo obravnavali v tečaju algoritmov, ji pravimo algoritem. Če pa gre za nekaj bolj specifičnega in novega, ji pravimo visoko nivojsko oblikovanje. Formalne razlike tu ni: oboje je abstraktni model programa.
Kako natančno bi morali napisati specifikacijo kode? Glavno: mora biti na nivoju nad samo kodo. Opisovati mora stanje in vedenje. Mora biti tako stroga, kot to naloga zahteva. Če pišete specifikacijo načina realizacije naloge, jo lahko napišete v psevdokodu ali s pomočjo PlusCal. Učiti se pisati specifikacije je treba na formalnih specifikacijah. To vam bo dalo potrebne veščine, ki bodo uporabne tudi pri neformalnih. Kako pa se naučiti pisati formalne specifikacije? Ko smo se učili programiranja, smo pisali programe in jih nato odpravljali. Enako velja tukaj: treba je napisati specifikacijo, jo preveriti s pomočjo orodja za preverjanje modelov in popraviti napake. TLA+ morda ni najboljši jezik za formalne specifikacije in za vaše specifične potrebe bo verjetno bolje ustrezal drug jezik. Prednost TLA+ je v tem, da odlično uči matematičnemu razmišljanju.
Kako povezati specifikacijo in kodo? S pomočjo komentarjev, ki povezujejo matematične pojme in njihovo implementacijo. Če delate z grafi, boste na ravni programa imeli tabele vozlišč in tabele povezav. Zato morate napisati, kako se graf dejansko uresničuje s temi programskimi strukturami.
Treba je opaziti, da se nič od zgoraj navedenega ne nanaša na sam proces pisanja kode. Ko pišete kodo, torej izvajate tretji korak, morate tudi razmišljati in premisliti o programu. Če se podnaloga izkaže za zapleteno ali nejasno, morate zanj napisati specifikacijo. O sami kodi tukaj ne govorim. Uporabljate lahko kateri koli programski jezik, katero koli metodologijo, to ni tema. Poleg tega nič od zgoraj navedenega ne oprošča potrebe po testiranju in odpravljanju napak v kodi. Tudi če je abstraktni model pravilno napisan, so lahko v njegovi implementaciji napake.
Pisanje specifikacij je dodatna faza v procesu pisanja kode. Zahvaljujoč temu je mogoče mnoge napake odkriti z manjšimi napori — to poznamo iz izkušenj programerjev iz Amazona. S specifikacijami se kakovost programov zviša. Zakaj torej tako pogosto preživimo brez njih? Ker je pisanje težko. In pisanje je težko, ker je treba razmišljati, razmišljanje pa je tudi težko. Vedno je lažje delati, kot da razmišljaš. Tukaj lahko potegnemo analogijo z tekom — čim manj tečete, tem počasneje tečete. Potrebno je trenirati svoje mišice in vaditi pisanje. Potrebna je praksa.
Specifikacija može biti netočna. Mogli ste negdje napraviti grešku, ili su se zahtjevi možda promijenili, ili je bilo potrebno napraviti poboljšanje. Svaki kod koji netko koristi mora se mijenjati, stoga će ranije ili kasnije specifikacija prestati odgovarati programu. U idealnom slučaju, u tom slučaju, trebate napisati novu specifikaciju i potpuno prepisati kod. Dobro znamo da to nitko ne čini. U praksi zakrpamo kod i možda ažuriramo specifikaciju. Ako to obavezno jednom dođe, zašto uopće pisati specifikacije? Prvo, za osobu koja će uređivati vaš kod, svaka suvišna riječ u specifikaciji bit će dragocjena, a ta osoba možete biti i vi sami. Često se prekoravam zbog nedostatne specifikacije kada uređujem svoj kod. A ja pišem više specifikacija nego koda. Stoga, kada uređujete kod, specifikaciju uvijek treba ažurirati. Drugo, s svakim uređivanjem kod postaje gori, sve je teže čitati i održavati. To je porast entropije. Ali ako ne krenete od specifikacije, svaka napisano linija bit će izmjena, i kod će od samog početka biti glomazan i teško čitljiv.
Kao što je rekao , niti jedna bitka nije dobijena prema planu, i niti jedna bitka nije dobijena bez plana. A on je znao nešto o bitkama. Postoji mišljenje da je pisanje specifikacija beskorisno gubljenje vremena. Ponekad je to zaista tako, i zadatak je toliko jednostavan da se o njemu ne treba razmišljati. No, uvijek treba imati na umu da kada vam savjetuju da ne pišete specifikacije, to znači da vam savjetuju da ne razmišljate. I o tome svakako treba razmisliti. Promišljanje zadatka ne jamči da nećete napraviti greške. Kao što znamo, nitko nije izumio čarobni štapić, a programiranje je složen posao. No, ako ne razmišljate o zadatku, sigurno ćete napraviti greške.
Detaljnije o TLA+ i PlusCal možete pročitati na posebnoj stranici, može se doći s moje početne stranice . Na tome sam završio, hvala na pažnji.
Opozarjam, da je to prevod. Ko boste pisali komentarje, se spomnite, da avtor teh ne bo prebral. Če res želite komunicirati z avtorjem, bo prisoten na konferenci Hydra 2019, ki bo potekala 11. in 12. julija 2019 v Sankt Peterburgu. Vstopnice so na voljo za nakup. .
Izvor: habr.com
