To je prevodni članek . Pred tem pa kratek uvod. Kako nastanejo zombiji? Vsakdo se je že znašel v situaciji, ko želi prijatelja ali sodelavca dvigniti na svoj nivo, pa mu ne gre. Poleg tega "ne gre" ne toliko za vas kot zanj: na eni strani lestvice je normalna plača, naloge in tako naprej, na drugi pa je treba razmišljati. Razmišljanje je neprijetno in boleče. Hitro obupa in nadaljuje s pisanjem kode, ne da bi sploh uporabil svoje možgane. Zavedate se, koliko truda je potrebno, da premagate oviro naučene nemoči, pa tega preprosto ne storite. Tako nastanejo zombiji, za katere se zdi, da jih je mogoče ozdraviti, a tega, kot kaže, ne bo naredil nihče.
Ko sem to videl (ja, ta isti prijatelj iz učbenikov) in ne daje poročila, ampak sejo vprašanj in odgovorov, sem bil nekoliko previden. Za vsak slučaj, Leslie je svetovno znani znanstvenik, avtor temeljnih del na področju porazdeljenega računalništva, morda ga poznate tudi po črkah La v LaTeXu - “Lamport TeX”. Drugi zaskrbljujoči dejavnik je njegova zahteva: vsak, ki pride, mora (popolnoma brezplačno) vnaprej poslušati nekaj njegovih poročil, se o njih domisliti vsaj eno vprašanje in šele nato priti. Odločil sem se pogledati, kaj Lamport tam oddaja - in super je! To je točno ta stvar, čarobna vezna tabletka za zdravljenje zombijev. Opozarjam vas: besedilo lahko resno opeče tiste, ki obožujejo super agilne metodologije in ne marajo testirati napisanega.
Po habrokatu se pravzaprav začne prevajanje seminarja. Uživajte v branju!
Ne glede na nalogo, ki jo prevzamete, morate vedno iti skozi tri korake:
- odločite se, kateri cilj želite doseči;
- odločite se, kako natančno boste dosegli svoj cilj;
- doseči svoj cilj.
To velja tudi za programiranje. Ko pišemo kodo, potrebujemo:
- odločite se, kaj točno naj program naredi;
- natančno določiti, kako naj opravlja svojo nalogo;
- napišite ustrezno kodo.
Zadnji korak je seveda zelo pomemben, a o tem danes ne bom govoril. Namesto tega bomo razpravljali o prvih dveh. Vsak programer jih izvede pred začetkom dela. Ne sedeš pisati, če se nisi odločil, kaj pišeš: brskalnik ali baza podatkov. Prisotna mora biti določena ideja o cilju. In zagotovo razmislite, kaj točno bo program naredil, in ga ne napišite naključno v upanju, da se bo koda sama nekako spremenila v brskalnik.
Kako točno pride do tega vnaprejšnjega razmišljanja o kodi? Koliko truda bi morali vložiti v to? Vse je odvisno od tega, kako kompleksen problem rešujemo. Recimo, da želimo napisati porazdeljen sistem, odporen na napake. V tem primeru bi morali stvari dobro premisliti, preden se usedemo za kodiranje. Kaj pa, če moramo samo povečati celoštevilsko spremenljivko za 1? Na prvi pogled je tukaj vse nepomembno in razmišljanje ni potrebno, potem pa se spomnimo, da lahko pride do prelivanja. Torej, tudi če želite razumeti, ali je problem preprost ali zapleten, morate najprej razmisliti.
Če vnaprej razmislite o možnih rešitvah problema, se lahko izognete napakam. Toda to zahteva, da je vaše razmišljanje jasno. Da bi to dosegli, morate zapisati svoje misli. Všeč mi je citat Dicka Guindona: "Ko pišeš, ti narava pokaže, kako površno razmišljaš." Če ne pišeš, samo misliš, da razmišljaš. In svoje misli morate zapisati v obliki specifikacij.
Specifikacije imajo številne funkcije, zlasti pri velikih projektih. Vendar bom govoril samo o enem od njih: pomagajo nam jasno razmišljati. Jasno razmišljanje je zelo pomembno in precej težko, zato tukaj potrebujemo kakršno koli pomoč. V katerem jeziku naj pišemo specifikacije? Na splošno je to vedno prvo vprašanje programerjev: v katerem jeziku bomo pisali? Ni enega pravilnega odgovora: problemi, ki jih rešujemo, so preveč raznoliki. Za nekatere ljudi je TLA+ specifikacijski jezik, ki sem ga razvil. Za druge je bolj priročno uporabljati kitajščino. Vse je odvisno od situacije.
Bolj pomembno vprašanje je: kako lahko dosežemo jasnejše mišljenje? Odgovor: Razmišljati moramo kot znanstveniki. To je način razmišljanja, ki je dobro deloval v zadnjih 500 letih. V znanosti gradimo matematične modele realnosti. Astronomija je bila morda prva znanost v ožjem pomenu besede. V matematičnem modelu, ki se uporablja v astronomiji, se nebesna telesa pojavljajo kot točke z maso, položajem in gibalno količino, čeprav so v resnici izjemno zapleteni objekti z gorami in oceani, osekami in tokovi. Ta model, tako kot kateri koli drug, je bil ustvarjen za reševanje določenih težav. Odličen je za določanje, kam usmeriti teleskop, če želite najti planet. Toda če želite napovedati vreme na tem planetu, ta model ne bo deloval.
Matematika nam omogoča določitev lastnosti modela. In znanost kaže, kako so te lastnosti povezane z realnostjo. Pogovorimo se o naši znanosti, informatiki. Realnost, s katero delamo, so računalniški sistemi različnih vrst: procesorji, igralne konzole, računalniki, ki izvajajo programe, itd. Govoril bom o izvajanju programa v računalniku, vendar na splošno vsi ti zaključki veljajo za kateri koli računalniški sistem. V naši znanosti uporabljamo veliko različnih modelov: Turingov stroj, delno urejene množice dogodkov in številne druge.
Kaj je program? To je katera koli koda, ki jo je mogoče obravnavati samostojno. Recimo, da moramo napisati brskalnik. Opravljamo tri naloge: oblikujemo uporabniško predstavitev programa, nato napišemo visokonivojski diagram programa in na koncu napišemo kodo. Ko pišemo kodo, ugotovimo, da moramo napisati oblikovalnik besedila. Tudi tukaj moramo rešiti tri težave: določiti, katero besedilo bo to orodje vrnilo; izberite algoritem za oblikovanje; napisati kodo. Ta naloga ima svojo podnalogo: pravilno vstavljanje vezajev v besede. Tudi to podnalogo rešujemo v treh korakih – kot vidimo, se ti ponavljajo na več ravneh.
Oglejmo si podrobneje prvi korak: katero težavo rešuje program. Tukaj najpogosteje modeliramo program kot funkcijo, ki sprejme nekaj vnosa in da nekaj izhoda. V matematiki je funkcija običajno opisana kot urejen niz parov. Na primer, funkcija kvadriranja naravnih števil je opisana kot niz {<0,0>, <1,1>, <2,4>, <3,9>, …}. Domena definicije takšne funkcije je množica prvih elementov vsakega para, to je naravnih števil. Za definiranje funkcije moramo določiti njeno domeno in formulo.
Toda funkcije v matematiki niso enake funkcijam v programskih jezikih. Matematika je veliko preprostejša. Ker nimam časa za zapletene primere, razmislimo o preprostem: funkcija v 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 M и NČe GCD(M,N) - funkcija, katere domena je niz parov celih števil, vrnjena vrednost pa je največje celo število, deljeno z M и N. Kakšna je realnost v primerjavi s tem modelom? Model deluje s celimi števili, v C ali Javi pa imamo 32-bitnega int. Ta model nam omogoča, da se odločimo, ali je algoritem pravilen GCD, vendar ne bo preprečilo napak pri prelivanju. To bi zahtevalo kompleksnejši model, za katerega pa ni časa.
Pogovorimo se o omejitvah funkcije kot modela. Nekateri programi (kot so operacijski sistemi) ne vrnejo samo določene vrednosti za določene argumente; lahko delujejo neprekinjeno. Poleg tega je funkcija kot model slabo primerna za drugi korak: načrtovanje, kako rešiti problem. Quicksort in bubble sort izračunata isto funkcijo, vendar sta popolnoma različna algoritma. Zato za opis načina doseganja cilja programa uporabljam drug model, recimo mu standardni vedenjski model. Program je v njem predstavljen kot niz vseh veljavnih vedenj, od katerih je vsako zaporedje stanj, stanje pa je dodeljevanje vrednosti spremenljivkam.
Poglejmo, kako bi izgledal drugi korak za evklidski algoritem. Izračunati moramo GCD(M, N). Inicializiramo M kot xIn N kot y, nato večkrat odštejte manjšo od teh spremenljivk od večje, dokler nista enaki. Na primer, če M = 12In N = 18, lahko opišemo naslednje vedenje:
[x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6]
In če M = 0 и N = 0? Ničla je deljiva z vsemi števili, zato v tem primeru ni največjega delitelja. V tej situaciji se moramo vrniti k prvemu koraku in se vprašati: ali res moramo izračunati GCD za nepozitivna števila? Če to ni potrebno, morate samo spremeniti specifikacijo.
Tukaj je na mestu kratka digresija o produktivnosti. Pogosto se meri v številu vrstic kode, napisanih na dan. Toda vaše delo je veliko bolj koristno, če se znebite določenega števila vrstic, saj imate manj prostora za hrošče. In kode se najlažje znebite v prvem koraku. Možno je, da preprosto ne potrebujete vseh zvončkov, ki jih poskušate uvesti. Najhitrejši način za poenostavitev programa in prihranek časa je, da ne počnete stvari, ki jih ne bi smeli početi. Drugi korak ima drugi največji potencial prihranka časa. Če produktivnost merite glede na napisane vrstice, potem vas bo razmišljanje o tem, kako dokončati nalogo manj produktivni, ker lahko isti problem rešite z manj kode. Natančne statistike tukaj ne morem dati, ker nimam možnosti prešteti vrstic, ki jih nisem napisal zaradi časa, ki sem ga porabil za specifikacijo, torej za prvi in drugi korak. In tudi tukaj ne moremo narediti eksperimenta, ker v eksperimentu nimamo pravice dokončati prvega koraka, naloga je določena vnaprej.
V neformalnih specifikacijah je zlahka spregledati številne težave. Nič ni težko napisati strogih specifikacij za funkcije, o tem ne bom razpravljal. Namesto tega bomo govorili o pisanju strogih specifikacij za standardna vedenja. Obstaja izrek, ki pravi, da je mogoče katerikoli niz vedenj opisati z lastnostjo varnosti (varnost) in lastnosti preživetja (živahnost). Varnost pomeni, da se ne bo zgodilo nič slabega, program ne bo dal napačnega odgovora. Preživetje pomeni, da se bo prej ali slej zgodilo nekaj dobrega, tj. program bo prej ali slej dal pravilen odgovor. Varnost je praviloma pomembnejši pokazatelj, tu se najpogosteje pojavljajo napake. Zato, da prihranim čas, ne bom govoril o preživetju, čeprav je to seveda tudi pomembno.
Varnost dosežemo tako, da najprej določimo nabor možnih začetnih stanj. In drugič, razmerja z vsemi možnimi naslednjimi stanji za vsako državo. Obnašajmo se kot znanstveniki in matematično definirajmo stanja. Množica začetnih stanj je opisana s formulo, na primer v primeru evklidskega algoritma: (x = M) ∧ (y = N). Za določene vrednosti M и N obstaja samo eno začetno stanje. Razmerje z naslednjim stanjem opisuje formula, v kateri so spremenljivke naslednjega stanja zapisane s praštevilo, spremenljivke trenutnega stanja pa brez praštevila. V primeru evklidskega algoritma bomo imeli opravka z disjunkcijo dveh formul, v eni od katerih x je največja vrednost, v drugem pa - y:
V prvem primeru je nova vrednost y enaka prejšnji vrednosti y, novo vrednost x pa dobimo tako, da manjšo spremenljivko odštejemo od večje. V drugem primeru naredimo obratno.
Vrnimo se k evklidskemu algoritmu. Predpostavimo še to M = 12, N = 18. To definira eno samo začetno stanje, (x = 12) ∧ (y = 18). Te vrednosti nato vključimo v zgornjo formulo in dobimo:
Tukaj je edina možna rešitev: x' = 18 - 12 ∧ y' = 12in dobimo vedenje: [x = 12, y = 18]. Na enak način lahko opišemo vsa stanja našega vedenja: [x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6].
V zadnjem stanju [x = 6, y = 6] oba dela izraza bosta napačna, zato nima naslednjega stanja. Imamo torej popolno specifikacijo drugega koraka - kot vidimo, je to povsem običajna matematika, kot pri inženirjih in znanstvenikih, in ne čudna, kot v računalništvu.
Ti dve formuli je mogoče združiti v eno formulo časovne logike. Je eleganten in enostaven za razlago, a za to zdaj ni časa. Časovno logiko morda potrebujemo le zaradi lastnosti živahnosti, za varnost pa ni potrebna. Časovne logike kot take ne maram, ni čisto navadna matematika, ampak v primeru živosti nujno zlo.
V evklidskem algoritmu za vsako vrednost x и y obstajajo edinstvene vrednosti x' и y', zaradi česar je razmerje z naslednjim stanjem resnično. Z drugimi besedami, evklidski algoritem je determinističen. Za modeliranje nedeterminističnega algoritma mora imeti trenutno stanje več možnih prihodnjih stanj in vsaka vrednost spremenljivke s praštevilo mora imeti več vrednosti spremenljivke s praosnovo, tako da je razmerje do naslednjega stanja resnično. To ni težko narediti, vendar zdaj ne bom navajal primerov.
Za izdelavo delovnega orodja potrebujete formalno matematiko. Kako narediti specifikacijo formalno? Za to bomo potrebovali formalni jezik, npr. . Specifikacija evklidskega algoritma v tem jeziku bo videti takole:
Simbol enačaja s trikotnikom pomeni, da je vrednost na levi strani znaka določena kot enaka vrednosti na desni strani znaka. V bistvu je specifikacija definicija, v našem primeru dve definiciji. Specifikaciji v TLA+ morate dodati deklaracije in nekaj sintakse, kot na zgornjem diapozitivu. V ASCII bi to izgledalo takole:
Kot lahko vidite, nič zapletenega. Specifikacijo na TLA+ je mogoče preveriti, kar pomeni, da je možno zaobiti vsa možna vedenja v majhnem modelu. V našem primeru bo ta model določene vrednosti M и N. To je zelo učinkovit in preprost način preverjanja, ki je popolnoma samodejen. Poleg tega je mogoče napisati formalne dokaze resnice in jih mehanično preveriti, vendar to vzame veliko časa, zato tega skoraj nihče ne počne.
Glavna pomanjkljivost TLA+ je, da je matematika, programerji in računalničarji pa se matematike bojijo. Na prvi pogled se to sliši kot šala, a na žalost to govorim povsem resno. Moj kolega mi je ravno pripovedoval, kako je poskušal razložiti TLA+ več razvijalcem. Takoj, ko so se formule pojavile na ekranu, so njihove oči takoj steklenile. Torej, če je TLA+ strašljiv, lahko uporabite , je nekakšen programski jezik za igrače. Izraz v PlusCal je lahko kateri koli izraz TLA+, to je v bistvu kateri koli matematični izraz. Poleg tega ima PlusCal sintakso za nedeterministične algoritme. Ker lahko PlusCal napiše kateri koli izraz TLA+, je bistveno bolj izrazit kot kateri koli pravi programski jezik. Nato je PlusCal sestavljen v lahko berljivo specifikacijo TLA+. To seveda ne pomeni, da se bo zapletena specifikacija PlusCal spremenila v preprosto na TLA+ - le da je ujemanje med njima očitno, nobena dodatna zapletenost se ne bo pojavila. Končno je to specifikacijo mogoče preveriti z orodji TLA+. Na splošno lahko PlusCal pomaga premagati fobijo pred matematiko, razumejo ga lahko tudi programerji in računalničarji. V preteklosti sem nekaj časa (približno 10 let) na njem objavljal algoritme.
Morda bo kdo ugovarjal, da sta TLA+ in PlusCal matematika, matematika pa deluje samo z izmišljenimi primeri. V praksi potrebujete pravi jezik s tipi, postopki, objekti itd. To je narobe. Chris Newcomb, ki je delal pri Amazonu, piše: »TLA+ smo uporabili pri desetih velikih projektih in v vsakem primeru je njegova uporaba pomembno vplivala na razvoj, saj smo lahko ujeli nevarne hrošče, preden so prišli v proizvodnjo, in ker nam je dal vpogled in zaupanje, ki smo ga potrebovali, da smo postali agresivni optimizacije delovanja brez vplivanja na resničnost programa". Pogosto lahko slišite, da z uporabo formalnih metod dobimo neučinkovito kodo - v praksi je vse ravno nasprotno. Poleg tega obstaja mnenje, da menedžerjev ni mogoče prepričati o potrebi po formalnih metodah, tudi če so programerji prepričani o njihovi uporabnosti. In Newcomb piše: »Upravitelji si zdaj na vse možne načine prizadevajo, da bi specifikacije napisali v TLA+, in za to posebej dodeljujejo čas«. Torej, ko menedžerji vidijo, da TLA+ deluje, ga sprejmejo. Chris Newcomb je to napisal pred približno šestimi meseci (oktober 2014), zdaj pa, kolikor vem, se TLA+ uporablja v 14 projektih, ne v 10. Drug primer se nanaša na zasnovo XBox 360. K Charlesu Thackerju je prišel pripravnik in napisal specifikacijo za pomnilniški sistem. Zahvaljujoč tej specifikaciji je bila najdena napaka, ki sicer ne bi bila odkrita in bi povzročila sesutje vsakega XBoxa 360 po štirih urah uporabe. Inženirji iz IBM-a so potrdili, da njihovi testi ne bi odkrili te napake.
Več o TLA+ lahko preberete na internetu, zdaj pa se pogovorimo o neformalnih specifikacijah. Redkokdaj moramo pisati programe, ki izračunavajo najmanjši skupni delitelj in podobno. Veliko pogosteje pišemo programe, kot je orodje za lep tiskalnik, ki sem ga napisal za TLA+. Po najenostavnejši obdelavi bi koda TLA+ izgledala takole:
Toda v zgornjem primeru je uporabnik najverjetneje želel, da sta konjunkcija in enačaj poravnana. Tako bi pravilno oblikovanje izgledalo bolj takole:
Razmislite o še enem primeru:
Nasprotno, tukaj je bila poravnava enakih znakov, seštevanje in množenje v izvoru naključna, tako da je najenostavnejša obdelava povsem dovolj. Na splošno ni natančne matematične definicije pravilnega oblikovanja, ker "pravilno" v tem primeru pomeni "kar uporabnik želi", tega pa ni mogoče matematično določiti.
Zdi se, da če nimamo definicije resnice, potem je specifikacija neuporabna. Ampak to ni res. Samo zato, ker ne vemo, kaj naj bi program delal, ne pomeni, da nam ni treba razmišljati o tem, kako naj bi deloval – nasprotno, vanj bi morali vložiti še več truda. Specifikacija je tu še posebej pomembna. Nemogoče je določiti optimalen program za strukturirano tiskanje, vendar to ne pomeni, da se ga sploh ne bi smeli lotiti in pisanje kode kot tok zavesti ne gre za to. Na koncu sem napisal specifikacijo šestih pravil z definicijami v obliki komentarjev v datoteki Java. Tukaj je primer enega od pravil: a left-comment token is LeftComment aligned with its covering token. To pravilo je napisano v, recimo, matematični angleščini: LeftComment aligned, left-comment и covering token — pojmi z definicijami. Matematiki matematiko opisujejo takole: pišejo definicije pojmov in na njihovi podlagi ustvarjajo pravila. Prednost te specifikacije je, da je šest pravil veliko lažje razumeti in odpraviti napake kot 850 vrstic kode. Moram reči, da pisanje teh pravil ni bilo enostavno; odpravljanje napak je trajalo precej časa. Posebej za ta namen sem napisal kodo, ki mi je povedala, katero pravilo je bilo uporabljeno. Ker sem teh šest pravil preizkusil z nekaj primeri, mi ni bilo treba odpravljati napak v 850 vrsticah kode in hrošče je bilo precej enostavno najti. Java ima odlična orodja za to. Če bi samo napisal kodo, bi mi vzelo precej več časa in formatiranje bi bilo slabše kakovosti.
Zakaj ni bilo mogoče uporabiti formalne specifikacije? Po eni strani pravilna izvedba tu ni preveč pomembna. Strukturiran izpis nekaterim zagotovo ne bo zadovoljiv, zato mi ga ni bilo treba zagotoviti, da pravilno deluje v vseh nenavadnih situacijah. Še bolj pomembno pa je dejstvo, da nisem imel ustreznega orodja. Preverjevalnik modelov TLA+ je tukaj neuporaben, zato bi moral primere napisati ročno.
Dana specifikacija ima lastnosti, ki so skupne vsem specifikacijam. Je višja raven od kode. Lahko se izvaja v katerem koli jeziku. Ni orodij ali metod za pisanje. Noben tečaj programiranja vam ne bo pomagal napisati te specifikacije. In ni orodij, zaradi katerih bi bila ta specifikacija nepotrebna, razen če seveda pišete jezik posebej za pisanje strukturiranih programov za tiskanje v TLA+. Končno, ta specifikacija ne pove ničesar o tem, kako točno bomo napisali kodo, navaja le, kaj koda počne. Napišemo specifikacijo, ki nam pomaga razmisliti o problemu, preden začnemo razmišljati o kodi.
Toda ta specifikacija ima tudi značilnosti, ki jo razlikujejo od drugih specifikacij. 95 % drugih specifikacij je veliko krajših in preprostejših:
Poleg tega je ta specifikacija niz pravil. To je običajno znak slabe specifikacije. Razumevanje posledic nabora pravil je precej težko, zato sem moral porabiti veliko časa za njihovo odpravljanje napak. Vendar v tem primeru nisem mogel najti boljšega načina.
Vredno je povedati nekaj besed o programih, ki delujejo neprekinjeno. Običajno delujejo vzporedno, kot so operacijski sistemi ali porazdeljeni sistemi. Zelo malo ljudi jih razume v mislih ali na papirju in jaz nisem eden izmed njih, čeprav mi je nekoč to uspelo. Zato potrebujemo orodja, ki bodo preverjala naše delo - na primer TLA+ ali PlusCal.
Zakaj sem moral napisati specifikacijo, če sem že vedel, kaj naj naredi koda? Pravzaprav sem samo mislil, da vem. Poleg tega z vzpostavljeno specifikacijo zunanjemu uporabniku ni več treba pogledati v kodo, da bi razumel, kaj točno počne. Imam pravilo: splošnih pravil ne sme biti. Seveda obstaja izjema od tega pravila, to je edino splošno pravilo, ki mu sledim: specifikacija o tem, kaj koda počne, mora ljudem povedati vse, kar morajo vedeti, ko uporabljajo to kodo.
Torej, kaj točno morajo programerji vedeti o razmišljanju? Za začetek enako kot za vse: če ne pišeš, potem se ti samo zdi, da razmišljaš. Poleg tega morate razmisliti, preden kodirate, kar pomeni, da morate pisati, preden kodirate. Specifikacija je tisto, kar napišemo, preden začnemo kodirati. Specifikacija je potrebna za vsako kodo, ki jo lahko uporablja ali spreminja kdorkoli. In ta »nekdo« se lahko izkaže za avtorja kode mesec dni po tem, ko je bila napisana. Specifikacija je potrebna za velike programe in sisteme, za razrede, za metode in včasih celo za kompleksne dele ene same metode. Kaj natančno morate napisati o kodi? Morate opisati, kaj počne, to je nekaj, kar je lahko koristno za vsakogar, ki uporablja to kodo. Včasih je morda treba tudi določiti, kako natančno koda doseže svoj cilj. Če smo šli skozi to metodo pri tečaju algoritmov, jo imenujemo algoritem. Če gre za nekaj bolj specializiranega in novega, potem temu rečemo oblikovanje na visoki ravni. Tu ni formalne razlike: oba sta abstraktna modela programa.
Kako natančno morate napisati specifikacijo kode? Glavna stvar: mora biti eno raven višje od same kode. Opisovati mora stanja in vedenja. Moral bi biti tako strog, kot zahteva naloga. Če pišete specifikacijo o tem, kako izvesti nalogo, jo lahko napišete v psevdokodi ali z uporabo PlusCal. Naučiti se morate pisati specifikacije z uporabo formalnih specifikacij. Tako boste pridobili potrebna znanja, ki vam bodo pomagala tudi pri neformalnih. Kako se lahko naučite pisati uradne specifikacije? Ko smo se naučili programirati, smo pisali programe in jih nato razhroščevali. Ista stvar tukaj: napisati morate specifikacijo, jo preveriti s preverjevalnikom modelov in popraviti napake. TLA+ morda ni najboljši jezik za formalno specifikacijo in drug jezik bi bil verjetno bolj primeren za vaše specifične potrebe. Odlična stvar pri TLA+ je, da odlično uči matematično razmišljanje.
Kako povezati specifikacijo in kodo? Uporaba komentarjev, ki povezujejo matematične koncepte in njihovo implementacijo. Če delate z grafi, potem boste na ravni programa imeli nize vozlišč in nize povezav. Zato morate napisati, kako natančno je graf implementiran s temi programskimi strukturami.
Opozoriti je treba, da nič od zgoraj navedenega ne velja za sam proces pisanja kode. Ko pišete kodo, torej izvajate tretji korak, morate tudi razmišljati in razmišljati skozi program. Če se podnaloga izkaže za zapleteno ali neočitno, morate zanjo napisati specifikacijo. Vendar tukaj ne govorim o sami kodi. Uporabite lahko kateri koli programski jezik, katero koli metodologijo, ne gre zanje. Poleg tega nič od zgoraj naštetega ne odpravlja potrebe po testiranju in odpravljanju napak v kodi. Tudi če je abstraktni model napisan pravilno, lahko pride do napak v njegovi implementaciji.
Pisanje specifikacij je dodaten korak v procesu kodiranja. Zahvaljujoč njej je mogoče številne napake ujeti z manj truda - to vemo iz izkušenj programerjev iz Amazona. S specifikacijami postaja kakovost programov višja. Zakaj torej tako pogosto ostanemo brez njih? Ker je pisanje težko. Toda pisanje je težko, ker je za to treba razmišljati, razmišljanje pa je tudi težko. Vedno se je lažje pretvarjati, da razmišljaš. Tu lahko potegnemo analogijo s tekom – manj kot tečeš, počasneje tečeš. Morate trenirati svoje mišice in vaditi pisanje. Potrebna je praksa.
Specifikacija je morda napačna. Morda ste se nekje zmotili ali so se zahteve spremenile ali pa je potrebna izboljšava. Vsako kodo, ki jo kdorkoli uporabi, je treba spremeniti, zato se specifikacija prej ali slej ne bo več ujemala s programom. V idealnem primeru morate v tem primeru napisati novo specifikacijo in popolnoma prepisati kodo. Dobro vemo, da tega nihče ne počne. V praksi kodo popravimo in morda posodobimo specifikacijo. Če se bo to prej ali slej zagotovo zgodilo, zakaj potem sploh pisati specifikacije? Prvič, za osebo, ki bo urejala vašo kodo, bo vsaka dodatna beseda v specifikaciji vredna zlata in ta oseba ste prav lahko vi. Pogosto se zbadam, ker nisem dovolj natančen, ko urejam kodo. In pišem več specifikacij kot kode. Zato je treba specifikacijo vedno posodobiti, ko urejate kodo. Drugič, z vsakim urejanjem je koda slabša, težje jo je brati in vzdrževati. To je povečanje entropije. Če pa ne začnete s specifikacijo, bo vsaka vrstica, ki jo napišete, urejanje, koda pa bo že od začetka obsežna in težko berljiva.
Kot rečeno , nobena bitka ni bila dobljena po načrtu in nobena bitka ni bila dobljena brez načrta. In vedel je nekaj o bitkah. Obstaja mnenje, da je pisanje specifikacij izguba časa. Včasih je to res in naloga je tako preprosta, da o njej nima smisla razmišljati. Vedno pa si morate zapomniti, da ko vam svetujejo, da ne pišete specifikacij, to pomeni, da vam svetujemo, da ne razmišljate. In o tem bi morali razmišljati vsakič. Razmišljanje o nalogi ne zagotavlja, da ne boste delali napak. Kot vemo, nihče ni izumil čarobne paličice, programiranje pa je težka naloga. Če pa naloge ne premislite, boste zagotovo delali napake.
Več o TLA+ in PlusCal si lahko preberete na posebni spletni strani, tja lahko greste z moje domače strani . To je vse zame, hvala za pozornost.
Ne pozabite, da je to prevod. Ko pišete komentarje, ne pozabite, da jih avtor ne bo prebral. Če res želite poklepetati z avtorjem, bo na konferenci Hydra 2019, ki bo potekala 11. in 12. julija 2019 v St. Vstopnice je mogoče kupiti .
Vir: www.habr.com