Tento článok je prekladom . Ale pred ňou malý úvod. Ako sa tvoria zombie? Každý sa dostal do situácie, kedy chce potiahnuť kamaráta alebo kolegu na svoju úroveň, no nejde to. A nie je to ani tak u vás, ako u neho, že „to nejde“: na jednej strane stupnice je normálny plat, úlohy atď., Na druhej strane potreba premýšľať. Myslenie je nepríjemné a bolestivé. Rýchlo to vzdáva a pokračuje v písaní kódu bez toho, aby vôbec zapol mozog. Predstavujete si, koľko úsilia stojí prekonať bariéru naučenej bezmocnosti, a jednoducho to neurobíte. Takto vznikajú zombie, ktoré sa, zdá sa, dajú vyliečiť, no zdá sa, že to nikto neurobí.
Keď som to videl (áno, ten istý súdruh z učebníc) a nerobí správu, ale reláciu otázok a odpovedí, bol som trochu opatrný. Len pre každý prípad, Leslie je svetoznámy vedec, autor zásadných diel v oblasti distribuovaných počítačov a môžete ho poznať aj podľa písmen La v slove LaTeX - „Lamport TeX“. Druhým alarmujúcim faktorom je jeho požiadavka: každý, kto príde, si musí (úplne zadarmo) vopred vypočuť pár jeho reportáží, vymyslieť na ne aspoň jednu otázku a až potom prísť. Rozhodol som sa pozrieť, čo tam Lamport vysielal – a je to skvelé! Je to presne tá vec, magická tabletka na vyliečenie zombíkov. Varujem vás: z textu môžu výrazne vyhorieť milovníci superflexibilných metodík a tí, ktorí neradi testujú napísané.
Po habrokate sa v skutočnosti začína preklad seminára. Užívať si čítanie!
Bez ohľadu na to, akú úlohu prijmete, vždy musíte prejsť tromi krokmi:
- rozhodnite sa, aký cieľ chcete dosiahnuť;
- rozhodnite sa, ako dosiahnete svoj cieľ;
- prísť k svojmu cieľu.
To platí aj pre programovanie. Keď píšeme kód, potrebujeme:
- rozhodnúť, čo by mal program robiť;
- určiť, ako má vykonávať svoju úlohu;
- napíšte zodpovedajúci kód.
Posledný krok je, samozrejme, veľmi dôležitý, ale o ňom dnes nebudem hovoriť. Namiesto toho budeme diskutovať o prvých dvoch. Každý programátor ich vykonáva pred začatím práce. Nesadnete si k písaniu, pokiaľ ste sa nerozhodli, či píšete prehliadač alebo databázu. Musí byť prítomná určitá predstava o cieli. A určite premýšľate o tom, čo presne program urobí, a nepíšte nejako v nádeji, že sa kód nejako zmení na prehliadač.
Ako presne prebieha toto predbežné premyslenie kódu? Koľko úsilia by sme tomu mali venovať? Všetko závisí od toho, aký zložitý problém riešime. Predpokladajme, že chceme napísať distribuovaný systém odolný voči chybám. V tomto prípade by sme si mali veci dôkladne premyslieť, kým si sadneme ku kódovaniu. Čo ak potrebujeme zvýšiť celočíselnou premennú o 1? Na prvý pohľad je tu všetko triviálne a nie je potrebné premýšľať, ale potom si uvedomíme, že môže dôjsť k preplneniu. Preto aj na to, aby ste pochopili, či je problém jednoduchý alebo zložitý, musíte najprv premýšľať.
Ak si vopred premyslíte možné riešenia problému, môžete sa vyhnúť chybám. To si však vyžaduje, aby vaše myslenie bolo jasné. Aby ste to dosiahli, musíte si zapísať svoje myšlienky. Veľmi sa mi páči citát Dicka Guindona: "Keď píšeš, príroda ti ukazuje, aké nedbalé je tvoje myslenie." Ak nepíšete, myslíte si len, že premýšľate. A svoje myšlienky si musíte zapísať vo forme špecifikácií.
Špecifikácie plnia mnoho funkcií, najmä vo veľkých projektoch. Ale budem hovoriť len o jednom z nich: pomáhajú nám jasne myslieť. Jasné myslenie je veľmi dôležité a dosť ťažké, takže tu potrebujeme akúkoľvek pomoc. V akom jazyku by sme mali písať špecifikácie? Vo všeobecnosti je to vždy prvá otázka pre programátorov: v akom jazyku budeme písať. Neexistuje na to jediná správna odpoveď: problémy, ktoré riešime, sú príliš rôznorodé. Pre niektorých je TLA+ jazyk špecifikácie, ktorý som vyvinul. Pre ostatných je vhodnejšie použiť čínštinu. Všetko závisí od situácie.
Dôležitejšia je ďalšia otázka: ako dosiahnuť jasnejšie myslenie? Odpoveď: Musíme myslieť ako vedci. Toto je spôsob myslenia, ktorý sa osvedčil za posledných 500 rokov. Vo vede vytvárame matematické modely reality. Astronómia bola možno prvou vedou v užšom zmysle slova. V matematickom modeli používanom v astronómii sa nebeské telesá javia ako body s hmotnosťou, polohou a hybnosťou, hoci v skutočnosti ide o mimoriadne zložité objekty s horami a oceánmi, prílivmi a odlivmi. Tento model, ako každý iný, bol vytvorený na riešenie určitých problémov. Je to skvelé na určenie, kam nasmerovať ďalekohľad, ak potrebujete nájsť planétu. Ale ak chcete predpovedať počasie na tejto planéte, tento model nebude fungovať.
Matematika nám umožňuje určiť vlastnosti modelu. A veda ukazuje, ako tieto vlastnosti súvisia s realitou. Hovorme o našej vede, informatike. Realitou, s ktorou pracujeme, sú výpočtové systémy rôzneho druhu: procesory, herné konzoly, počítače, spúšťacie programy a pod. Budem hovoriť o spustení programu na počítači, ale vo všeobecnosti všetky tieto závery platia pre akýkoľvek počítačový systém. V našej vede používame mnoho rôznych modelov: Turingov stroj, čiastočne usporiadané súbory udalostí a mnoho ďalších.
čo je program? Toto je akýkoľvek kód, ktorý možno zvážiť nezávisle. Predpokladajme, že potrebujeme napísať prehliadač. Vykonávame tri úlohy: navrhneme užívateľský pohľad na program, potom napíšeme diagram na vysokej úrovni programu a nakoniec napíšeme kód. Pri písaní kódu si uvedomujeme, že musíme napísať textový formátovač. Tu musíme opäť vyriešiť tri problémy: určiť, aký text tento nástroj vráti; vyberte algoritmus pre formátovanie; napísať kód. Táto úloha má svoju podúlohu: správne vložiť do slov spojovník. Aj túto podúlohu riešime v troch krokoch – ako vidíte, opakujú sa na mnohých úrovniach.
Pozrime sa podrobnejšie na prvý krok: aký problém program rieši. Tu najčastejšie modelujeme program ako funkciu, ktorá odoberá nejaký vstup a produkuje nejaký výstup. V matematike sa funkcia zvyčajne popisuje ako usporiadaná množina párov. Napríklad funkcia kvadratúry pre prirodzené čísla je opísaná ako množina {<0,0>, <1,1>, <2,4>, <3,9>, …}. Definičný obor takejto funkcie je množina prvých prvkov každého páru, teda prirodzených čísel. Aby sme definovali funkciu, musíme špecifikovať jej rozsah a vzorec.
Ale funkcie v matematike nie sú to isté ako funkcie v programovacích jazykoch. Matematika je oveľa jednoduchšia. Keďže nemám čas na zložité príklady, pouvažujme nad jednoduchým: funkciou v C alebo statickou metódou v Jave, ktorá vracia najväčšieho spoločného deliteľa dvoch celých čísel. V špecifikácii tejto metódy budeme písať: počíta GCD(M,N) za argumenty M и NKde GCD(M,N) - funkcia, ktorej doménou je množina párov celých čísel a návratová hodnota je najväčšie celé číslo, ktoré je deliteľné číslom M и N. Ako tento model súvisí s realitou? Model funguje na celých číslach, zatiaľ čo v C alebo Jave máme 32-bit int. Tento model nám umožňuje rozhodnúť, či je algoritmus správny GCD, ale nezabráni to chybám pri pretečení. To by si vyžadovalo zložitejší model, na ktorý nie je čas.
Povedzme si o obmedzeniach funkcie ako modelu. Niektoré programy (napríklad operačné systémy) nevracajú len určitú hodnotu pre určité argumenty, ale môžu bežať nepretržite. Okrem toho funkcia ako model nie je vhodná pre druhý krok: plánovanie riešenia problému. Rýchle triedenie a triedenie bublín počítajú rovnakú funkciu, ale sú to úplne odlišné algoritmy. Preto, aby som opísal, ako sa dosiahne cieľ programu, používam iný model, nazvime ho štandardný behaviorálny model. Program v ňom je reprezentovaný ako súbor všetkých prípustných správaní, z ktorých každé je zase sekvenciou stavov a stavom je priradenie hodnôt k premenným.
Pozrime sa, ako by vyzeral druhý krok pre Euclidov algoritmus. Musíme počítať GCD(M, N). Inicializujeme M ako xA N ako y, potom opakovane odčítajte menšiu z týchto premenných od väčšej, kým sa nebudú rovnať. Napríklad ak M = 12A N = 18, môžeme opísať nasledujúce správanie:
[x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6]
A ak M = 0 и N = 0? Nula je deliteľná všetkými číslami, takže v tomto prípade neexistuje najväčší deliteľ. V tejto situácii sa musíme vrátiť k prvému kroku a spýtať sa: naozaj potrebujeme vypočítať GCD pre nekladné čísla? Ak to nie je potrebné, stačí zmeniť špecifikáciu.
Tu by sme mali urobiť malú odbočku o produktivite. Často sa meria v počte riadkov kódu napísaných za deň. Ale vaša práca je oveľa užitočnejšia, ak sa zbavíte určitého počtu riadkov, pretože máte menej miesta pre chyby. A najjednoduchší spôsob, ako sa zbaviť kódu, je v prvom kroku. Je celkom možné, že jednoducho nepotrebujete všetky zvončeky a píšťalky, ktoré sa snažíte implementovať. Najrýchlejší spôsob, ako zjednodušiť program a ušetriť čas, je nerobiť veci, ktoré by sa robiť nemali. Druhým krokom je druhý najväčší potenciál úspory času. Ak meriate produktivitu na základe napísaných riadkov, prinúti vás premýšľať o tom, ako splniť úlohu menej produktívne, pretože rovnaký problém môžete vyriešiť s menším množstvom kódu. Nemôžem tu uviesť presnú štatistiku, pretože nemám ako spočítať počet riadkov, ktoré som nenapísal, pretože som strávil čas na špecifikácii, teda na prvom a druhom kroku. A ani tu sa experiment nedá nastaviť, pretože v experimente nemáme právo dokončiť prvý krok, úloha je vopred určená.
Je ľahké prehliadnuť mnohé ťažkosti v neformálnych špecifikáciách. Napísať striktné špecifikácie pre funkcie nie je nič zložité, nebudem to rozoberať. Namiesto toho budeme hovoriť o napísaní silných špecifikácií pre štandardné správanie. Existuje teorém, ktorý hovorí, že pomocou vlastnosti zabezpečenia možno opísať akúkoľvek množinu správania (bezpečnosť) a vlastnosti prežitia (živosť). Bezpečnosť znamená, že sa nič zlé nestane, program nedá nesprávnu odpoveď. Prežitie znamená, že skôr či neskôr sa niečo dobré stane, t. j. program skôr či neskôr dá správnu odpoveď. Bezpečnosť je spravidla dôležitejším ukazovateľom, najčastejšie sa tu vyskytujú chyby. Preto pre úsporu času nebudem hovoriť o prežití, aj keď je, samozrejme, tiež dôležitá.
Bezpečnosť dosiahneme tak, že najprv predpíšeme množinu možných počiatočných stavov. A po druhé, vzťahy so všetkými možnými ďalšími stavmi pre každý štát. Správajme sa ako vedci a definujme stavy matematicky. Množina počiatočných stavov je opísaná vzorcom, napríklad v prípade Euklidovho algoritmu: (x = M) ∧ (y = N). Pre určité hodnoty M и N existuje len jeden počiatočný stav. Vzťah s nasledujúcim stavom je opísaný vzorcom, v ktorom sa premenné nasledujúceho stavu zapisujú s prvočíslom a premenné aktuálneho stavu sa zapisujú bez prvočísla. V prípade Euklidovho algoritmu sa budeme zaoberať disjunkciou dvoch vzorcov, z ktorých jeden x je najväčšia hodnota a v druhej - y:
V prvom prípade sa nová hodnota y rovná predchádzajúcej hodnote y a novú hodnotu x získame odčítaním menšej premennej od väčšej. V druhom prípade robíme opak.
Vráťme sa k Euklidovmu algoritmu. Predpokladajme, že znova M = 12, N = 18. Toto definuje jediný počiatočný stav, (x = 12) ∧ (y = 18). Tieto hodnoty potom zapojíme do vyššie uvedeného vzorca a získame:
Tu je jediné možné riešenie: x' = 18 - 12 ∧ y' = 12a dostaneme správanie: [x = 12, y = 18]. Podobne môžeme opísať všetky stavy nášho správania: [x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6].
V poslednom stave [x = 6, y = 6] obe časti výrazu budú nepravdivé, takže nemá žiadny ďalší stav. Takže máme kompletnú špecifikáciu druhého kroku - ako vidíte, je to celkom obyčajná matematika ako u inžinierov a vedcov a nie divná, ako v informatike.
Tieto dva vzorce možno spojiť do jedného vzorca časovej logiky. Je elegantná a ľahko sa vysvetľuje, ale teraz na ňu nie je čas. Časovú logiku môžeme potrebovať len pre živosť, nie je potrebná pre bezpečnosť. Časovú logiku ako takú nemám rád, nie je to celkom obyčajná matematika, ale v prípade živosti je to nutné zlo.
V Euklidovom algoritme pre každú hodnotu x и y majú jedinečné hodnoty x' и y', ktoré robia vzťah s nasledujúcim stavom pravdivým. Inými slovami, Euklidov algoritmus je deterministický. Na modelovanie nedeterministického algoritmu je potrebné, aby aktuálny stav mal viacero možných budúcich stavov a aby každá hodnota premennej s primárnou základňou mala viacero hodnôt primárnej premennej, takže vzťah k ďalšiemu stavu je pravdivý. Je to jednoduché, ale teraz nebudem uvádzať príklady.
Na výrobu pracovného nástroja potrebujete formálnu matematiku. Ako urobiť špecifikáciu formálnou? Na to potrebujeme formálny jazyk, napr. . Špecifikácia Euklidovho algoritmu by v tomto jazyku vyzerala takto:
Symbol rovnosti s trojuholníkom znamená, že hodnota naľavo od znamienka je definovaná ako rovná hodnote napravo od znamienka. V podstate je špecifikácia definícia, v našom prípade dve definície. K špecifikácii v TLA+ je potrebné pridať deklarácie a nejakú syntax, ako na snímke vyššie. V ASCII by to vyzeralo takto:
Ako vidíte, nič zložité. Špecifikáciu pre TLA+ je možné otestovať, t.j. obísť všetky možné správanie v malom modeli. V našom prípade bude tento model určitými hodnotami M и N. Ide o veľmi efektívny a jednoduchý spôsob overovania, ktorý je úplne automatický. Je tiež možné písať formálne pravdivé dôkazy a kontrolovať ich mechanicky, ale to si vyžaduje veľa času, takže to takmer nikto nerobí.
Hlavnou nevýhodou TLA+ je, že je to matematika a programátori a informatici sa matematiky boja. Na prvý pohľad to znie ako vtip, ale, žiaľ, myslím to úplne vážne. Môj kolega mi práve hovoril, ako sa snažil vysvetliť TLA+ niekoľkým vývojárom. Len čo sa vzorce objavili na obrazovke, okamžite sa z nich stali sklenené oči. Takže ak vás TLA+ vydesí, môžete použiť , je to taký hračkársky programovací jazyk. Výraz v PlusCal môže byť akýkoľvek TLA+ výraz, teda celkovo akýkoľvek matematický výraz. PlusCal má navyše syntax pre nedeterministické algoritmy. Pretože PlusCal dokáže napísať akýkoľvek TLA+ výraz, PlusCal je oveľa výraznejší než akýkoľvek skutočný programovací jazyk. Ďalej je PlusCal skompilovaný do ľahko čitateľnej špecifikácie TLA+. To, samozrejme, neznamená, že sa komplexná špecifikácia PlusCal zmení na jednoduchú na TLA + - len korešpondencia medzi nimi je zrejmá, nedôjde k žiadnej ďalšej zložitosti. Nakoniec je možné túto špecifikáciu overiť pomocou nástrojov TLA+. Celkovo môže PlusCal pomôcť prekonať matematickú fóbiu a je ľahko pochopiteľný aj pre programátorov a počítačových vedcov. V minulosti som na ňom nejaký čas (asi 10 rokov) publikoval algoritmy.
Možno niekto namietne, že TLA + a PlusCal je matematika a matematika funguje len na vymyslených príkladoch. V praxi potrebujete skutočný jazyk s typmi, procedúrami, objektmi atď. Toto je nesprávne. Tu je to, čo Chris Newcomb, ktorý pracoval v Amazone, píše: „Použili sme TLA+ na desiatich veľkých projektoch a v každom prípade jeho používanie prinieslo významný rozdiel vo vývoji, pretože sme boli schopní zachytiť nebezpečné chyby ešte pred spustením výroby a pretože nám to poskytlo prehľad a istotu, ktorú sme potrebovali robiť agresívne optimalizácie výkonu bez ovplyvnenia pravdivosti programu“. Často môžete počuť, že pri používaní formálnych metód dostávame neefektívny kód – v praxi je všetko presne naopak. Okrem toho existuje názor, že manažérov nemožno presvedčiť o potrebe formálnych metód, aj keď sú programátori presvedčení o ich užitočnosti. A Newcomb píše: „Manažéri teraz tvrdo tlačia na písanie špecifikácií pre TLA + a špecificky na to prideľujú čas“. Takže keď manažéri vidia, že TLA+ funguje, radi to prijmú. Chris Newcomb to napísal asi pred šiestimi mesiacmi (október 2014), ale teraz, pokiaľ viem, sa TLA+ používa v 14 projektoch, nie v 10. Ďalší príklad sa týka dizajnu XBox 360. Za Charlesom Thackerom prišiel stážista a napísal špecifikáciu pre pamäťový systém. Vďaka tejto špecifikácii sa našla chyba, ktorá by inak zostala nepovšimnutá a kvôli ktorej by každý XBox 360 po štyroch hodinách používania spadol. Inžinieri IBM potvrdili, že ich testy by túto chybu nenašli.
Viac o TLA + si môžete prečítať na internete, ale teraz si povieme niečo o neformálnych špecifikáciách. Málokedy musíme písať programy, ktoré vypočítajú najmenšieho spoločného deliteľa a podobne. Oveľa častejšie píšeme programy, ako je nástroj pre peknú tlačiareň, ktorý som napísal pre TLA+. Po najjednoduchšom spracovaní by kód TLA + vyzeral takto:
Vo vyššie uvedenom príklade však používateľ s najväčšou pravdepodobnosťou chcel, aby boli spojka a rovná sa zarovnané. Takže správne formátovanie by vyzeralo asi takto:
Zvážte ďalší príklad:
Tu bolo naopak zarovnanie znamienok rovnosti, sčítania a násobenia v zdroji náhodné, takže úplne stačí najjednoduchšie spracovanie. Vo všeobecnosti neexistuje presná matematická definícia správneho formátovania, pretože „správne“ v tomto prípade znamená „to, čo používateľ chce“, a to sa nedá matematicky určiť.
Zdalo by sa, že ak nemáme definíciu pravdy, potom je špecifikácia zbytočná. Ale nie je. To, že nevieme, čo má program robiť, neznamená, že nemusíme premýšľať o tom, ako funguje – práve naopak, musíme do toho vynaložiť ešte viac úsilia. Tu je dôležitá najmä špecifikácia. Určiť optimálny program pre štruktúrovanú tlač je nemožné, to však neznamená, že by sme to vôbec nemali brať a písať kód ako prúd vedomia nie je dobrá vec. Na záver som napísal špecifikáciu šiestich pravidiel s definíciami vo forme komentárov v súbore java. Tu je príklad jedného z pravidiel: a left-comment token is LeftComment aligned with its covering token. Toto pravidlo je napísané, povedzme, matematickou angličtinou: LeftComment aligned, left-comment и covering token - pojmy s definíciami. Matematici takto popisujú matematiku: píšu definície pojmov a na základe nich aj pravidlá. Výhodou takejto špecifikácie je, že šesť pravidiel je oveľa jednoduchšie pochopiť a ladiť ako 850 riadkov kódu. Musím povedať, že napísanie týchto pravidiel nebolo jednoduché, ich odladenie zabralo pomerne veľa času. Špeciálne na tento účel som napísal kód, ktorý hlásil, ktoré pravidlo bolo použité. Vďaka tomu, že som týchto šesť pravidiel otestoval na niekoľkých príkladoch, nemusel som ladiť 850 riadkov kódu a ukázalo sa, že chyby sa dajú celkom ľahko nájsť. Java má na to skvelé nástroje. Keby som len napísal kód, trvalo by mi to oveľa dlhšie a formátovanie by bolo horšej kvality.
Prečo by sa nemohla použiť formálna špecifikácia? Na jednej strane tu nie je príliš dôležité správne prevedenie. Štrukturálne výtlačky určite nikoho nepotešia, takže som ich nemusel správne upravovať vo všetkých zvláštnych situáciách. Ešte dôležitejší je fakt, že som nemal adekvátne nástroje. Kontrola modelov TLA+ je tu zbytočná, takže príklady by som musel písať ručne.
Vyššie uvedená špecifikácia má vlastnosti spoločné pre všetky špecifikácie. Je to vyššia úroveň ako kód. Môže byť implementovaný v akomkoľvek jazyku. Akékoľvek nástroje alebo metódy sú na jeho písanie zbytočné. Žiadny kurz programovania vám nepomôže napísať túto špecifikáciu. A neexistujú žiadne nástroje, ktoré by mohli urobiť túto špecifikáciu zbytočnou, pokiaľ, samozrejme, nepíšete jazyk špeciálne na písanie štruktúrovaných tlačových programov v TLA+. Nakoniec, táto špecifikácia nehovorí nič o tom, ako presne napíšeme kód, iba hovorí, čo tento kód robí. Špecifikáciu píšeme, aby nám pomohla premyslieť si problém skôr, ako začneme premýšľať o kóde.
Ale táto špecifikácia má aj vlastnosti, ktoré ju odlišujú od ostatných špecifikácií. 95 % ostatných špecifikácií je výrazne kratších a jednoduchších:
Ďalej je táto špecifikácia súborom pravidiel. Spravidla je to znak zlej špecifikácie. Pochopiť dôsledky súboru pravidiel je dosť ťažké, a preto som musel stráviť veľa času ich ladením. V tomto prípade som však nenašiel lepší spôsob.
Stojí za to povedať pár slov o programoch, ktoré bežia nepretržite. Spravidla pracujú paralelne, napríklad operačné systémy alebo distribuované systémy. Len veľmi málo ľudí im rozumie mentálne alebo na papieri a ja medzi nich nepatrím, hoci som to kedysi dokázal. Preto potrebujeme nástroje, ktoré budú kontrolovať našu prácu – napríklad TLA+ alebo PlusCal.
Prečo bolo potrebné napísať špecifikáciu, keď som už vedel, čo presne má kód robiť? V skutočnosti som si myslel, že to viem. Navyše, so špecifikáciou sa outsider už nemusí dostať do kódu, aby pochopil, čo presne robí. Mám pravidlo: nemali by existovať žiadne všeobecné pravidlá. Z tohto pravidla samozrejme existuje výnimka, je to jediné všeobecné pravidlo, ktorým sa riadim: špecifikácia toho, čo kód robí, by mala ľuďom povedať všetko, čo potrebujú vedieť pri používaní kódu.
Čo presne teda potrebujú programátori vedieť o myslení? Na začiatok to isté ako všetci ostatní: ak nepíšete, potom sa vám len zdá, že premýšľate. Pred kódovaním musíte tiež premýšľať, čo znamená, že musíte písať skôr, ako kódujete. Špecifikácia je to, čo napíšeme predtým, ako začneme kódovať. Pre každý kód, ktorý môže ktokoľvek použiť alebo upraviť, je potrebná špecifikácia. A tento „niekto“ môže byť sám autorom kódu mesiac po jeho napísaní. Špecifikácia je potrebná pre veľké programy a systémy, pre triedy, pre metódy a niekedy aj pre zložité časti jednej metódy. Čo presne by sa malo o kóde napísať? Musíte opísať, čo robí, to znamená, čo môže byť užitočné pre každého, kto používa tento kód. Niekedy môže byť potrebné špecifikovať, ako kód plní svoj účel. Ak sme touto metódou prešli v priebehu algoritmov, nazývame ju algoritmus. Ak je to niečo špeciálnejšie a nové, potom to nazývame dizajn na vysokej úrovni. Nie je tu žiadny formálny rozdiel: oba sú abstraktným modelom programu.
Ako presne by ste mali napísať špecifikáciu kódu? Hlavná vec: mala by byť o úroveň vyššie ako samotný kód. Mal by popisovať stavy a správanie. Mal by byť taký prísny, ako si to úloha vyžaduje. Ak píšete špecifikáciu toho, ako sa má úloha implementovať, môžete ju napísať v pseudokóde alebo pomocou PlusCal. Musíte sa naučiť, ako písať špecifikácie na formálnych špecifikáciách. Získate tak potrebné zručnosti, ktoré vám pomôžu aj pri neformálnych. Ako sa naučíte písať formálne špecifikácie? Keď sme sa naučili programovať, napísali sme programy a potom ich ladili. Tu je to rovnaké: napíšte špecifikáciu, skontrolujte ju pomocou kontroly modelov a opravte chyby. TLA+ nemusí byť najlepší jazyk pre formálnu špecifikáciu a iný jazyk bude pravdepodobne lepší pre vaše špecifické potreby. Výhodou TLA+ je, že veľmi dobre učí matematické myslenie.
Ako prepojiť špecifikáciu a kód? Pomocou komentárov, ktoré spájajú matematické pojmy a ich implementáciu. Ak pracujete s grafmi, tak na úrovni programu budete mať polia uzlov a polia odkazov. Preto musíte presne napísať, ako je graf implementovaný týmito programovacími štruktúrami.
Treba poznamenať, že nič z vyššie uvedeného neplatí pre samotný proces písania kódu. Keď píšete kód, to znamená, že vykonávate tretí krok, musíte tiež premýšľať a premýšľať nad programom. Ak sa ukáže, že čiastková úloha je zložitá alebo nie je zrejmá, musíte pre ňu napísať špecifikáciu. Ale nehovorím tu o samotnom kóde. Môžete použiť akýkoľvek programovací jazyk, akúkoľvek metodiku, nie je to o nich. Nič z vyššie uvedeného tiež nevylučuje potrebu testovania a ladenia kódu. Aj keď je abstraktný model napísaný správne, v jeho implementácii sa môžu vyskytnúť chyby.
Zápis špecifikácií je ďalším krokom v procese kódovania. Vďaka nemu sa dajú mnohé chyby zachytiť s menšou námahou – poznáme to zo skúseností programátorov z Amazonu. So špecifikáciami sa kvalita programov zvyšuje. Prečo teda tak často chodíme bez nich? Pretože písanie je ťažké. A písanie je ťažké, pretože na to musíte myslieť a myslenie je tiež ťažké. Vždy je ľahšie predstierať, čo si myslíte. Tu môžete nakresliť analógiu s behom – čím menej bežíte, tým pomalšie. Musíte trénovať svaly a trénovať písanie. Treba prax.
Špecifikácia môže byť nesprávna. Možno ste niekde urobili chybu alebo sa požiadavky zmenili, prípadne je potrebné vykonať zlepšenie. Každý kód, ktorý ktokoľvek používa, musí byť zmenený, takže skôr či neskôr už nebude špecifikácia zodpovedať programu. V ideálnom prípade musíte v tomto prípade napísať novú špecifikáciu a úplne prepísať kód. Dobre vieme, že to nikto nerobí. V praxi opravujeme kód a prípadne aktualizujeme špecifikáciu. Ak sa to skôr či neskôr stane, tak prečo vôbec písať špecifikácie? Po prvé, pre osobu, ktorá bude upravovať váš kód, bude mať každé slovo navyše v špecifikácii cenu zlata a touto osobou môžete byť vy sami. Často sa nadávam, že pri úprave kódu nemám dostatočnú špecifikáciu. A píšem viac špecifikácií ako kódu. Preto pri úprave kódu je vždy potrebné aktualizovať špecifikáciu. Po druhé, s každou revíziou sa kód zhoršuje, je čoraz náročnejší na čítanie a údržbu. Ide o zvýšenie entropie. Ak však nezačnete špecifikáciou, potom každý riadok, ktorý napíšete, bude úpravou a kód bude od začiatku nepraktický a ťažko čitateľný.
Ako bolo povedané , žiadna bitka nebola vyhratá podľa plánu a žiadna bitka nebola vyhratá bez plánu. A vedel niečo o bitkách. Existuje názor, že písanie špecifikácií je strata času. Niekedy je to pravda a úloha je taká jednoduchá, že nie je o čom premýšľať. Vždy by ste si však mali pamätať, že keď vám niekto povie, aby ste nepísali špecifikácie, povedali vám, aby ste nepremýšľali. A mali by ste na to myslieť zakaždým. Premyslenie úlohy nezaručuje, že neurobíte chyby. Ako vieme, nikto nevynašiel čarovný prútik a programovanie je náročná úloha. Ak si však problém nepremyslíte, zaručene urobíte chyby.
Viac o TLA + a PlusCal si môžete prečítať na špeciálnej webovej stránke, môžete tam prejsť z mojej domovskej stránky . To je z mojej strany všetko, ďakujem za pozornosť.
Upozorňujeme, že ide o preklad. Keď píšete komentáre, nezabudnite, že ich autor nebude čítať. Ak si naozaj chcete s autorom pokecať, potom bude na konferencii Hydra 2019, ktorá sa bude konať 11. – 12. júla 2019 v Petrohrade. Lístky je možné zakúpiť .
Zdroj: hab.com