Toto je preklad článku . Ale predtým krátky úvod. Ako sa vytvárajú zombies? Každý sa ocitol v situácii, keď chce pozdvihnúť svojho priateľa alebo kolegu na svoju úroveň, ale nedarí sa mu to. A je to „nedarí sa“ nie tak veľmi kvôli tebe, ako kvôli nemu: na jednej strane váh je normálny plat, úlohy a tak ďalej, na druhej strane – potreba premýšľať. Premýšľať je nepríjemné a bolestivé. Rýchlo sa vzdáva a pokračuje v písaní kódu, úplne bez zapojenia mozgu. Predstavuješ si, koľko síl je potrebné vynaložiť na preklenutie bariéry naučenej bezmocnosti, a jednoducho to neurobíš. Takto sa vytvárajú zombies, ktorých sa možno zdá, že je možné uzdraviť, ale akosi sa nikomu nechce to robiť.
Keď som videl, že (áno, áno, ten istý spoločník z učebníc) a nebude robiť prednášku, ale sedenie s otázkami a odpoveďami, trochu som sa znepokojil. Pre istotu, Leslie je svetoznámy vedec, autor základných prác v distribuovaných výpočtoch, a možno ho poznáte aj z písmen La v slove LaTeX – "Lamport TeX". Druhým znepokojujúcim faktorom je jeho požiadavka: každý, kto príde, by mal (úplne zadarmo) vopred vypočuť pár jeho prednášok, vymyslieť na ne aspoň jednu otázku a až potom prísť. Rozhodol som sa pozrieť, čo Lesli hovorí – a je to úžasné! Je to presne to, čarovný odkaz-tabletka na vyliečenie zombizmu. Varujem: z textu môže poriadne zhoriť milovníkom nadmerne flexibilných metodológií a nemilovníkom testovania napísaného.
Po hromadnej diskusii vlastne začína preklad seminára. Prajem príjemné čítanie!
Nezáleží na tom, akú úlohu si vyberiete, vždy musíte prejsť tromi krokmi:
- určiť, akého cieľa chcete dosiahnuť;
- rozhodnúť, ako presne budete dosahovať svoj cieľ;
- dosiahnuť svoj cieľ.
To sa týka aj programovania. Keď píšeme kód, musíme:
- rozhodnúť, čo presne by mal program robiť;
- určiť, ako presne by mal vykonávať svoju úlohu;
- napísať zodpovedajúci kód.
Posledný krok je samozrejme veľmi dôležitý, ale o ňom dnes nebude reč. Namiesto toho budeme diskutovať o prvých dvoch. Tieto kroky vykonáva každý programátor skôr, než začne pracovať. Nesadnite si písať, pokiaľ ste sa nerozhodli, čo vlastne píšete: prehliadač alebo databázu. Určité predstavenie o cieli musí byť prítomné. A určite premýšľate o tom, čo presne program bude robiť, a nie píšete len tak s nádejou, že kód sa nejako premení na prehliadač.
Ako presne prebieha toto predbežné premýšľanie o kóde? Koľko úsilia by sme na to mali vynaložiť? Všetko závisí od toho, aký zložitý problém riešime. Predpokladajme, že chceme napísať odolný distribuovaný systém. V takom prípade by sme sa mali riadne zamyslieť, skôr než si sadneme za kód. A ak potrebujeme len zvýšiť celočíselnú premennú o 1? Na prvý pohľad je to triviálne a nevyžaduje žiadne úvahy, ale potom si uvedomíme, že môže nastať pretečenie. Preto, aj na to, aby sme pochopili, či ide o jednoduchý alebo zložitý problém — najprv musíme premýšľať.
Ak si dopredu premyslíte možné riešenia problému, môžete sa vyhnúť chybám. Ale na to, aby ste to dosiahli, musí byť vaše myslenie jasné. Aby ste to dosiahli, musíte si zaznamenať svoje myšlienky. Veľmi sa mi páči citát Dicka Gindona: „Keď píšete, príroda vám ukáže, aké neporiadne je vaše myslenie“. Ak nepíšete, len si myslíte, že premýšľate. A zapisovať si myšlienky by ste mali vo forme špecifikácií.
Špecifikácie plnia množstvo funkcií, najmä vo veľkých projektoch. Ale budem hovoriť len o jednej z nich: pomáhajú nám jasne myslieť. Jasne myslieť 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? To je vo všeobecnosti vždy prvá otázka pre programátorov: v akom jazyku budeme písať. Neexistuje správna odpoveď: problémy, ktoré riešime, sú príliš rozmanité. Pre niektorých je užitočné TLA+ — je to jazyk špecifikácií, ktorý som vytvoril. Pre iných je pohodlnejšie používať čínsky. Všetko závisí od situácie.
Dôležitejšia otázka znie: ako dosiahnuť jasnejšie myslenie? Odpoveď: musíme myslieť ako vedci. Tento spôsob myslenia sa osvedčil počas posledných 500 rokov. V vede budujeme matematické modely reality. Astronómia bola pravdepodobne prvou vedou v prísnom zmysle tohto slova. V matematickom modeli používanom v astronómii sa nebeské telá predstavujú ako body s hmotnosťou, polohou a momentom, hoci v skutočnosti sú to extrémne zložité objekty s horami a oceánmi, prílivmi a odlivmi. Tento model, rovnako ako každý iný, je vytvorený na riešenie určitého problému. Skvele sa hodí na to, aby sme určili, kam nasmerovať teleskop, ak potrebujeme 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 sa tieto vlastnosti vzťahujú na realitu. Poďme hovoriť o našej vede, informatike. Realita, s ktorou pracujeme, sú výpočtové systémy najrôznejších druhov: procesory, herné konzoly, počítače, ktoré vykonávajú programy, a tak ďalej. Budem hovoriť o vykonávaní programu na počítači, ale vo veľkej miere sú všetky tieto poznatky použiteľné pre akýkoľvek výpočtový systém. V našej vede používame množstvo rôznych modelov: Turingove stroje, čiastočne usporiadané množiny udalostí a mnohé iné.
Čo je to program? Je to akýkoľvek kód, ktorý môžeme považovať za samostatný. Predpokladajme, že potrebujeme napísať prehliadač. Splníme tri úlohy: navrhneme zobrazenie programu pre používateľa, potom napíšeme vysokú úroveň schémy programu a nakoniec napíšeme kód. Počas písania kódu si uvedomujeme, že potrebujeme napísať nástroj na formátovanie textu. Tu opäť musíme vyriešiť tri úlohy: určiť, aký text tento nástroj bude vracať; zvoliť algoritmus na formátovanie; napísať kód. Táto úloha má svoju podúlohu: správne vkladať spojovníky do slov. Túto podúlohu tiež riešime v troch krokoch – ako vidíme, opakujú sa na mnohých úrovniach.
Pozrime sa podrobnejšie na prvý krok: akú úlohu rieši program. Tu najčastejšie modelujeme program ako funkciu, ktorá prijíma niektoré vstupné údaje a poskytuje niektoré výstupné údaje. V matematike sa funkcia zvyčajne opisuje ako usporiadaná množina párov. Napríklad, funkcia umocnenia na druhú pre prirodzené čísla sa opisuje ako množina {, , , , …}. Oblasť definície takejto funkcie je množina prvých prvkov každého páru, teda prirodzené čísla. Na to, aby sme definovali funkciu, musíme uviesť jej oblasť definície a vzorec.
Ale funkcie v matematike nie sú to isté ako funkcie v programovacích jazykoch. Matematika je oveľa jednoduchšia. Keďže na komplikované príklady nemám čas, pozrime sa na jednoduchý: funkcia v jazyku C alebo statická metóda v Jave, ktorá vracia najväčší spoločný deliteľ dvoch celých čísel. V špecifikácii tejto metódy napíšeme: vypočíta GCD(M,N) pre argumenty M a N, kde GCD(M,N) — funkcia, ktorej oblasť definície je množina párov celých čísel a návratová hodnota je najväčšie celé číslo, ktoré delí M a N. Ako táto miera súvisí s realitou? Miera operuje s celými číslami, a v C alebo Jave máme 32-bitový int. Tento model nám umožňuje určiť, či je algoritmus správny GCD, ale nebráni pretečeniu. Na to by bolo potrebné zložitější model, na ktorý nie je čas.
Porozprávajme sa o obmedzeniach funkcie ako modelu. Práca niektorých programov (napríklad operačných systémov) sa nezameriava len na to, aby vrátila určitú hodnotu pre určité argumenty, môžu fungovať nepretržite. Okrem toho, funkcia ako model nie je dobre vhodná pre druhý krok: plánovanie spôsobu riešenia úlohy. Rýchly triediaci algoritmus a triedenie bublinkami počítajú tú istú funkciu, ale to sú úplne rôzne algoritmy. Preto na opísanie spôsobu dosiahnutia cieľa programu používam iný model, nazvime ho štandardný behaviorálny model. Program v ňom je zobrazený ako množina všetkých prípustných správaní, pričom každé z týchto správaní je zase sekvenciou stavov a stav je priradenie hodnôt premenným.
Pozrime sa, ako bude vyzerať druhý krok algoritmu Euklida. Musíme vypočítať GCD(M, N). Iniciujeme M ako x, a N ako y, potom opakovane odčítame menšiu z týchto premenných od väčšej, kým sa nestanú rovnými. Napríklad, ak M = 12, a 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 a N = 0? Ноль делится на все числа, поэтому наибольшего делителя в этом случае нет. В этой ситуации нам нужно вернуться к первому шагу и спросить: действительно ли нам нужно вычислять НОД для неположительных чисел? Если в этом нет необходимости, то нужно просто изменить спецификацию.
Tu je vhodné urobiť krátku odbočku o produktivite. Často sa meria počtom riadkov kódu napísaných za deň. Ale vaša práca je výrazne cennejšia, ak ste sa zbavili určitého počtu riadkov, pretože máte menej priestoru na chyby. A zbavovať sa kódu je najjednoduchšie práve v prvom kroku. Je celkom možné, že nepotrebujete všetky tie vylepšenia, ktoré sa snažíte implementovať. Najrýchlejší spôsob, ako zjednodušiť program a ušetriť čas, je nerobiť veci, ktoré sa nemusia robiť. Druhý krok je druhý v poradí z hľadiska potenciálu na úsporu času. Ak meriate produktivitu v počte napísaných riadkov, premýšľanie o spôsoboch, ako vykonať úlohu, vás urobí menej produktívnymi, pretože tú istú úlohu môžete vyriešiť menším objemom kódu. Presnú štatistiku tu poskytnúť nemôžem, pretože nemám spôsob, ako počítať počet riadkov, ktoré som nenapísal, pretože som strávil čas špecifikáciou, teda prvým a druhým krokom. A experiment tu tiež nemôžem vykonať, pretože v experimente nemôžeme vykonať prvý krok, úloha je určená vopred.
V neformálnych špecifikáciách je ľahké prehliadnuť mnohé ťažkosti. Nie je nič zložité na písaní prísnych špecifikácií pre funkcie, o tom sa nebudeme baviť. Namiesto toho sa porozprávame o písaní prísnych špecifikácií pre štandardné behaviorálne modely. Existuje veta, ktorá hovorí, že akúkoľvek množinu správania je možné opísať pomocou vlastnosti bezpečnosti (safety) a vlastnosti životnosti (liveness). Bezpečnosť znamená, že sa nič zlé nestane, program nevydá nesprávnu odpoveď. Odolnosť znamená, že skôr či neskôr nastane niečo dobré, t. j. program skôr či neskôr poskytne správnu odpoveď. Vo všeobecnosti je bezpečnosť dôležitejším ukazovateľom, chyby sa väčšinou vyskytujú práve tu. Preto, aby som ušetril čas, nebudem hovoriť o odolnosti, aj keď je samozrejme tiež dôležitá.
Dosahujeme bezpečnosti tým, že vypisujeme, po prvé, množstvo možných počiatočných stavov. A po druhé, vzťahy so všetkými možnými nasledujúcimi stavmi pre každý stav. Budeme sa správať ako vedci a definovať stavy matematicky. Sada počiatočných stavov je popísaná formulou, napríklad v prípade Euklidovho algoritmu: (x = M) ∧ (y = N). Pre určité hodnoty M a N existuje iba jeden počiatočný stav. Vzťah s nasledujúcim stavom je opísaný formulou, v ktorej sú premenné nasledujúceho stavu zapísané s chvostom, a aktuálneho stavu — bez chvosta. V prípade Euklidovho algoritmu budeme mať do činenia s disjunkciou dvoch formulí, kde jedna z nich x je najväčšia hodnota, a v druhej — y:
V prvom prípade nová hodnota y zodpovedá predchádzajúcej hodnote y, zatiaľ čo novú hodnotu x získavame odčítaním menšej premennej od väčšej. V druhom prípade robíme opak.
Vráťme sa k Euklidovmu algoritmu. Predpokladajme znova, že M = 12, N = 18. To určuje jediný počiatočný stav, (x = 12) ∧ (y = 18). Potom tieto hodnoty dosadíme do vyššie uvedenej formulácie a dostaneme:
Tu je jediné možné riešenie: x' = 18 - 12 ∧ y' = 12, a dostávame správanie: [x = 12, y = 18]. Rovnako môžeme opísať všetky stavy v našom správaní: [x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6].
V poslednom stave [x = 6, y = 6] budú obe časti výrazu nepravdivé, a teda nasledujúceho stavu niet. Takže máme úplnú špecifikáciu druhého kroku — ako vidíme, je to celkom obyčajná matematika, akú používajú inžinieri a vedci, a nie zvláštna, ako v informatike.
Tieto dve vzorce je možné spojiť do jedného vzorca temporálnej logiky. Je elegantný a nie je ťažké ho vysvetliť, ale momentálne na to nie je čas. Temporálna logika nám môže byť potrebná iba pre vlastnosť živosti, pre bezpečnosť nie je potrebná. Temporálna logika ako taká nie je obľúbená, nie je to úplne bežná matematika, ale v prípade živosti je to nevyhnutné zlo.
V Euklidovom algoritme pre každú hodnotu x a y existujú jedinečné hodnoty x' a y', ktoré robia vzťah so nasledujúcim stavom pravdivým. Inými slovami, Euklidov algoritmus je deterministický. Aby sme mohli modelovať nedeterministický algoritmus, musí mať aktuálny stav niekoľko možných budúcich stavov, a pre každú hodnotu premennej bez úpravy musí existovať niekoľko hodnôt premennej s úpravou, pri ktorých je vzťah so nasledujúcim stavom pravdivý. Nie je to ťažké urobiť, ale teraz nebudem uvádzať príklady.
Aby sme vytvorili funkčný nástroj, potrebujeme formálnu matematiku. Ako vyrobiť špecifikáciu formálnej? Na to potrebujeme formálny jazyk, napríklad . Špecifikácia Euklidovho algoritmu na tomto jazyku vyzerá nasledovne:
Symbol znaku rovnosti s trojuholníkom znamená, že hodnota naľavo od znaku je definovaná ako rovná hodnote napravo od znaku. V podstate je špecifikácia definíciou, v našom prípade dvoma definíciami. K špecifikácii v TLA+ je potrebné pridať vyhlásenia a určitú syntaktiku, ako je to na snímke vyššie. V ASCII to bude vyzerať takto:
Ako vidíme, nič zložité. Špecifikáciu na TLA+ je možné overiť, t.j. prejsť všetky možné správanie v malej modeli. V našom prípade bude touto modelou určené hodnoty M a N. Je to veľmi efektívny a jednoduchý spôsob overenia, ktorý sa celkom vykonáva automaticky. Okrem toho je možné napísať formálne dôkazy pravdivosti a overiť ich mechanicky, ale na to je potrebný veľa času, preto to takmer nikto nerobí.
Hlavným nedostatkom TLA+ je, že ide o matematiku, a programátori a počítačoví vedci sa matematiky boja. Na prvý pohľad to znie ako vtip, ale, žiaľ, hovorím to úplne vážne. Môj kolega mi práve rozprával, ako sa snažil vysvetliť TLA+ niekoľkým vývojárom. Ako sa na obrazovke objavili vzorce, okamžite dostali sklenené oči. Takže ak TLA+ desí, môžete použiť , čo je akýsi hračkový programovací jazyk. Výraz v PlusCal môže byť akýmkoľvek výrazom TLA+, to znamená, že v podstate akýmkoľvek matematickým výrazom. Okrem toho, PlusCal má syntax pre nedeterministické algoritmy. Vďaka tomu, že v PlusCal môžeme zapísať akýkoľvek výraz TLA+, je výrazne výrečnejší ako akýkoľvek reálny programovací jazyk. Ďalej, PlusCal sa kompiluje do ľahko čitateľnej špecifikácie TLA+. To neznamená, že zložitá špecifikácia PlusCal sa premení na jednoduchú v TLA+ — jednoducho medzi nimi je zrejmý súlad, nedôjde k dodatočnej zložitosti. Nakoniec, túto špecifikáciu bude možné overiť nástrojmi TLA+. Všeobecne, PlusCal môže pomôcť prekonať fóbiu z matematiky, je to ľahko pochopiteľné aj pre programátorov a počítačových vedcov. V minulosti som nejaký čas (asi 10 rokov) publikoval na ňom algoritmy.
Možno niekto oponuje, že TLA+ a PlusCal — to je matematika, a matematika pracuje len na vymyšlených príkladoch. V praxi však potrebujeme skutočný jazyk s typmi, procedúrami, objektmi a podobne. To nie je pravda. Tu je, čo píše Chris Newcomb, ktorý pracoval v Amazone: „Používali sme TLA+ v desiatich veľkých projektoch, a v každom prípade prínos jeho využitia bol významný pre vývoj, pretože sme dokázali zachytiť nebezpečné bugy pred tým, ako sa dostali do produkcie, a pretože nám poskytol pochopenie a dôveru potrebnú pre agresívne optimalizácie výkonu, ktoré neovplyvnili pravdivosť programu“. Často počuť, že pri používaní formálnych metód dostávame neefektívny kód — v praxi je však všetko presne naopak. Okrem toho existuje názor, že manažérov nemožno presvedčiť o potrebe formálnych metód, aj keď programátori sú presvedčení o ich užitočnosti. A Newcomb píše: „Manažéri teraz vo všetkom podnecujú písanie špecifikácií pre TLA+ a osobitne na to vyčleňujú čas“. Takže keď manažéri vidia, že TLA+ funguje, s radosťou ho prijmú. Chris Newcomb to napísal pred asi šiestimi mesiacmi (v októbri 2014), teraz, ak viem, sa TLA+ používa v 14 projektoch, nie 10. Ďalší príklad sa týka návrhu XBox 360. K Charlesovi Teckerovi prišiel stážista a napísal špecifikáciu pre systém pamäte. Vďaka tejto špecifikácii bol objavený bug, ktorý by inak ostal bez povšimnutia, a kvôli ktorému by každá XBox 360 zlyhala po štyroch hodinách používania. Inžinieri z IBM potvrdili, že ich testy by tento bug neodhalili.
O TLA+ si môžete podrobnejšie prečítať na internete, a teraz sa poďme porozprávať o neformálnych špecifikáciách. Zriedkakedy musíme písať programy, ktoré počítajú najmenší spoločný násobok a podobne. Častejšie píšeme programy, ako je nástroj na formátovanie výstupu (pretty-printer), ktorý som napísal pre TLA+. Po najjednoduchšom spracovaní by kód v TLA+ vyzeral takto:
Ale v uvedenom príklade si používateľ pravdepodobne želal, aby znaky konjunkcie a rovnosti boli zarovnané. Takže správne formátovanie by vyzeralo skôr takto:
Pozrime sa na ďalší príklad:
Tu, naopak, zarovnanie znakov rovnosti, sčítania a násobenia v zdroji bolo náhodné, takže najjednoduchšie spracovanie je úplne postačujúce. Vo všeobecnosti neexistuje presná matematická definícia správneho formátovania, pretože „správne“ v tomto prípade znamená „aké si želá používateľ“, a to sa matematicky definovať nedá.
Mohlo by sa zdať, že ak nemáme definíciu pravdivosti, potom je špecifikácia zbytočná. Ale nie je to pravda. Ak nevieme, čo presne má program robiť, neznamená to, že si nemáme premyslieť jeho fungovanie — práve naopak, mali by sme do toho investovať ešte viac úsilia. Špecifikácia je tu obzvlášť dôležitá. Určiť optimálny program pre štrukturálne formátovanie nie je možné, ale to neznamená, že sa na to nemáme pozerať vôbec, a písať kód ako tok vedomia — to nie je v poriadku. Nakoniec som napísal špecifikáciu zo šiestich pravidiel s definíciami vo forme komentárov v súbore Java. Tu je príklad jedného z pravidiel: token left-comment je LeftComment zhodný so svojím pokrývacím tokenom. Toto pravidlo je napísané takpovediac na matematickej angličtine: LeftComment zhodný, left-comment a pokrývací token — termíny s definíciami. Takto matematiky opisujú matematiku: píšu definície termínov a na ich základe — pravidlá. Výhodou takejto špecifikácie je, že pochopiť a doladiť šesť pravidiel je oveľa jednoduchšie ako 850 riadkov kódu. Treba povedať, že napísať tieto pravidlá nebolo jednoduché, na ich ladenie sa venovalo dosť veľa času. Špeciálne na tento účel som napísal kód, ktorý hlásil, ktoré konkrétne pravidlo sa používa. Vďaka tomu, že som tieto šesť pravidiel otestoval na niekoľkých príkladoch, nemusel som ladit 850 riadkov kódu a chyby sa ukázali byť pomerne ľahko identifikovateľné. V Jave na to existujú skvelé nástroje. Keby som len napísal kód, trvalo by mi to výrazne dlhšie a formátovanie by bolo horšej kvality.
Prečo sa nedala použiť formálna špecifikácia? Z jednej strany, správnosť vykonania tu nie je až taká dôležitá. Štrukturálna tlač sa určite niekomu nepáči, takže som nemusel dosahovať správnu funkciu vo všetkých neobvyklých situáciách. Ešte dôležitejšie je, že som nemal adekvátne nástroje. Nástroj na kontrolu modelov TLA+ tu je zbytočný, takže by som musel príklady písať manuálne.
Uvedená špecifikácia má znaky spoločné pre všetky špecifikácie. Je na vyššej úrovni ako kód. Môže byť implementovaná v akomkoľvek jazyku. Na jej písanie sú akékoľvek nástroje alebo metódy zbytočné. Žiadny kurz programovania vám nepomôže napísať túto špecifikáciu. A neexistujú žiadne nástroje, ktoré by mohli túto špecifikáciu urobiť zbytočnou, ak samozrejme nepíšete jazyk špeciálne pre písanie programov so štrukturálnou tlačou na TLA+. Nakoniec, táto špecifikácia nehovorí nič o tom, ako presne budeme písať kód, iba uvádza, čo tento kód robí. Píšeme špecifikáciu, aby nám pomohla premyslieť problém, ešte predtým, než začneme rozmýšľať o kóde.
Ale táto špecifikácia má aj vlastnosti, ktoré ju odlišujú od iných špecifikácií. 95% ostatných špecifikácií je podstatne kratších a jednoduchších:
Ďalej, táto špecifikácia je súbor pravidiel. Zvyčajne je to znakom zlej špecifikácie. Pochopiť dôsledky súboru pravidiel je dosť ťažké, a preto mi trvalo veľa času, kým som ich doladil. Napriek tomu v tomto prípade som nenašiel lepší spôsob.
Stojí za to povedať pár slov o programoch, ktoré fungujú nepretržite. Zvyčajne pracujú paralelne, napríklad operačné systémy alebo distribuované systémy. Rozumieť im v mysli alebo na papieri dokáže len veľmi málo ľudí, a ja sa medzi nich nepočítam, hoci kedysi som to zvládal. Preto sú potrebné nástroje, ktoré budú kontrolovať našu prácu — napríklad TLA+ alebo PlusCal.
Prečo som mal písať špecifikáciu, keď som už vedel, čo kód má robiť? V skutočnosti sa len zdalo, že to viem. Okrem toho, ak existuje špecifikácia, netreba nikomu, kto nie je zasvätený, preniknúť do kódu, aby pochopil, čo vlastne robí. Mám pravidlo: nesmú existovať žiadne všeobecné pravidlá. Toto pravidlo samozrejme má výnimku, je to jediné všeobecné pravidlo, ktorému sa riadim: špecifikácia toho, čo robí kód, by mala oznámiť ľuďom všetko, čo potrebujú vedieť pri použití tohto kódu.
Čo konkrétne by sa programátori mali naučiť o spôsobe myslenia? Predovšetkým to isté, čo aj všetci ostatní: ak nepíšete, iba sa vám zdá, že myslíte. Okrem toho je potrebné premýšľať predtým, ako začnete kódovať, čo znači, že musíte písať predtým, ako začnete kódovať. Špecifikácia je to, čo píšeme predtým, než začneme kódovať. Špecifikácia je potrebná pre akýkoľvek kód, ktorý môže byť použitý alebo zmenený niekým iným. A týmto „niekým“ môže byť aj samotný autor 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ější časti jednotlivých metód. Čo konkrétne by sa malo napísať o kóde? Je potrebné popísať, čo robí, teda to, čo môže byť užitočné pre akúkoľvek osobu, ktorá tento kód používa. Niekedy môže byť potrebné uviesť, ako kód dosahuje svoj cieľ. Ak sme tento spôsob preberali v kurze algoritmov, voláme to algoritmus. Ak ide o niečo špeciálnejšie a nové, nazývame to vysokoúrovňovým dizajnom. Formálny rozdiel medzi nimi nie je: oboje je abstraktný model programu.
Ako by sa mala písať špecifikácia kódu? Hlavné: mala by byť na úrovni vyššie než samotný kód. Mala by popisovať stavy a správanie. Musí byť tak rigorózna, ako to požaduje úloha. Ak píšete špecifikáciu spôsobu realizácie úlohy, môže byť napísaná v pseudokóde alebo pomocou PlusCal. Naučiť sa písať špecifikácie by sa malo na formálnych špecifikáciách. To vám poskytne potrebné zručnosti, ktoré pomôžu aj s neformálnymi. A ako sa naučiť písať formálne špecifikácie? Keď sme sa učili programovanie, písali sme programy a potom ich ladili. To isté platí aj tu: musíte napísať špecifikáciu, skontrolovať ju pomocou nástroja na overovanie modelov a opraviť chyby. TLA+ nemusí byť najlepší jazyk pre formálnu špecifikáciu a pre vaše konkrétne potreby pravdepodobne lepšie vyhovuje iný jazyk. Výhodou TLA+ je, že skvele učí matematickému mysleniu.
Ako prepojiť špecifikáciu a kód? Pomocou komentárov, ktoré spájajú matematické pojmy a ich realizáciu. Ak pracujete s grafmi, na úrovni programu budete mať polia uzlov a polia väzieb. Preto musíte napísať, ako konkrétne sa graf realizuje týmito programovacími štruktúrami.
Je potrebné poznamenať, že nič z vyššie uvedeného sa netýka samotného procesu písania kódu. Keď píšete kód, teda vykonávate tretí krok, musíte tiež premýšľať a rozpracovať program. Ak sa podúloha ukáže ako zložitá alebo nejasná, je potrebné pre ňu napísať špecifikáciu. O samotnom kóde tu však nehovorím. Môžete používať akýkoľvek programovací jazyk, akúkoľvek metodológiu, nejde o ne. Okrem toho, nič z vyššie uvedeného vás nezbavuje potreby testovať a ladit kód. Aj keď je abstraktný model napísaný správne, jeho realizácia môže obsahovať chyby.
Písanie špecifikácií je ďalší krok v procese písania kódu. Vďaka nemu je možné nájsť mnohé chyby s menším úsilím — to vieme z praxe programátorov z Amazonu. So špecifikáciami sa kvalita programov zvyšuje. Prečo sa však tak často zaobídeme bez nich? Pretože písanie je ťažké. A písanie je ťažké, pretože si musíte premýšľať, a premýšľať je tiež ťažké. Vždy je jednoduchšie tváriť sa, že premýšľate. Môžeme tu urobiť analógiu s behom — čím menej beháte, tým pomalšie bežíte. Musíte trénovať svoje svaly a cvičiť v písaní. Potrebujete prax.
Špecifikácia môže byť nepresná. Môžete mať niekde chybu, alebo sa mohli zmeniť požiadavky, alebo sa ukázalo, že je potrebné urobiť vylepšenie. Akýkoľvek kód, ktorý niekto používa, sa musí meniť, takže skôr či neskôr prestane špecifikácia zodpovedať programu. V ideálnom prípade je v takomto prípade potrebné napísať novú špecifikáciu a úplne prepísať kód. Dobre vieme, že tak nikto nerobí. V praxi opravujeme kód a možno aktualizujeme špecifikáciu. Ak sa to nevyhnutne stane skôr či neskôr, prečo vôbec písať špecifikácie? Po prvé, pre človeka, ktorý bude upravovať váš kód, bude každé zbytočné slovo v špecifikácii na váhe zlata, a tým človekom môžete byť pokojne vy sami. Často sa na seba hnevám za nedostatočnú špecifikáciu, keď opravujem svoj kód. A píšem viac špecifikácií ako kódu. Preto, keď opravujete kód, musíte vždy aktualizovať špecifikáciu. Po druhé, s každou úpravou sa kód zhoršuje, stáva sa ťažšie čitateľným a udržiavateľným. Je to nárast entropie. Ale ak nezačnete so špecifikáciou, každá napísaná línia bude opravou a kód bude od začiatku objemný a ťažko čitateľný.
Ako hovoril , žiadna bitka nebola vyhraná podľa plánu, a žiadna bitka nebola vyhraná bez plánu. A on vedel niečo o bitkách. Existuje názor, že písanie špecifikácií je zbytočné plytvanie časom. Niekedy to naozaj tak je, a úloha je tak jednoduchá, že nie je čo premýšľať. Ale vždy je potrebné pamätať na to, že keď vám radia, aby ste nepísali špecifikácie, znamená to, že vám radia, aby ste nemysleli. A o tom si vždy treba zamyslieť. Premýšľanie o úlohe nezaručuje, že neurobíte chyby. Ako vieme, nikto nevymyslel čarovnú paličku, a programovanie je zložitá činnosť. Ale ak nepripravujete úlohu, zaručene urobíte chyby.
Viac o TLA+ a PlusCal si môžete prečítať na špeciálnej stránke, tam sa dá prísť z mojej domovskej stránky. . Na tomto mám všetko, ďakujem za pozornosť.
Pripomínam, že ide o preklad. Keď budete písať komentáre — pamätajte, že autor ich neprečíta. Ak sa naozaj chcete s autorom porozprávať, bude na konferencii Hydra 2019, ktorá sa uskutoční 11.-12. júla 2019 v Petrohrade. Lístky je možné zakúpiť .
Zdroj: habr.com
Russian
Italian
German
Polish
Estonian
Albanian
Bulgarian
Croatian
Czech
Danish
Dutch
English
French
Hungarian
Latvian
Norwegian
Portuguese
Romanian
Slovak
Slovenian
Spanish
Swedish