Toto je překlad článku . Ale před ním je krátký úvod. Jak se vytvářejí zombie? Každý se ocitl v situaci, kdy chce někoho přivést na svou úroveň, ale to se mu nedaří. A přitom „nedaří se“ není tolik u něj, jako u vás: na jedné misce vah je běžný plat, úkoly a tak dále, a na druhé - nezbytnost přemýšlet. Přemýšlení je nepříjemné a bolestivé. Rychle to vzdá a pokračuje v psaní kódu, aniž by zapojil mozek. Představ si, kolik síly je třeba vynaložit na překonání bariéry naučené bezmoci, a prostě to neuděláš. Tak vznikají zombie, které by teoreticky šly vyléčit, ale prakticky se tomu nikdo nebude věnovat.
Když jsem viděl, že (ano, ten samý chlapík z učebnic) a nedělá přednášku, ale sezení otázek a odpovědí, trochu jsem se ožil. Pro pořádek, Leslie je celosvětově uznávaný vědec, autor základních prací v oblasti distribuovaných výpočtů, a také ho můžete znát podle písmen La ve slově LaTeX - „Lamport TeX“. Dalším znepokojivým faktorem je jeho požadavek: každý, kdo přijde, by měl (zcela zdarma) předem poslechnout pár jeho přednášek, vymyslet k nim alespoň jeden otázku a teprve poté dorazit. Rozhodl jsem se podívat, co Lamport hlásá - a je to skvělé! Je to přesně ta věc, kouzelný odkaz-tabletka na léčbu zombie stavu. Varuji: text může velmi rozhněvat milovníky superflexibilních metodologií a odpůrce testování napsaného.
Po hubrokátu vlastně začíná překlad semináře. Příjemné čtení!
Ať už se pustíte do jakéhokoli úkolu, vždy musíte projít třemi kroky:
- určit, jakého cíle chcete dosáhnout;
- rozhodnout, jakým způsobem svou cíle dosáhnete;
- dojít k svému cíli.
To platí i pro programování. Když píšeme kód, musíme:
- rozhodnout, co má program dělat;
- určit, jakým způsobem by měla úkol splnit;
- napsat odpovídající kód.
Poslední krok je samozřejmě velmi důležitý, ale dnes o něm mluvit nebudu. Místo toho prodiskutujeme prvních několik. Ty provádí každý programátor, než začne pracovat. Nepř sitnete psát, pokud jste se nerozhodli, co přesně píšete: prohlížeč nebo databázi. Určitá představa o cíli musí být nutně přítomna. A vždy uvažujete o tom, co program vlastně bude dělat, a ne že napíšete něco bezmyšlenkovitě v naději, že se kód nějak promění v prohlížeč.
Jak přesně probíhá toto předběžné promýšlení kódu? Kolik úsilí bychom měli věnovat tomu? Všechno závisí na tom, jak složitý problém řešíme. Předpokládejme, že chceme napsat vysoce dostupný distribuovaný systém. V tomto případě bychom se měli dobře zamyslet, než se posadíme kódu. A pokud jednoduše potřebujeme zvýšit celočíselnou proměnnou o 1? Na první pohled se to zdá banální a žádné uvažování není potřeba, ale pak si vzpomeneme, že může dojít k přetečení. Proto i k určení, zda je problém jednoduchý nebo složitý, je třeba nejprve přemýšlet.
Předběžným promyšlením možných řešení problému se dají předejít chybám. Abychom to mohli udělat, je však nutné mít jasné myšlení. K tomu je potřeba zapisovat si své myšlenky. Líbí se mi citát Dika Gindona: „Když píšete, příroda vám ukazuje, jak neohrabané je vaše myšlení.“ Pokud nepíšete, máte jen pocit, že přemýšlíte. A myšlenky je třeba zapisovat ve formě specifikací.
Specifikace plní mnoho funkcí, zejména u velkých projektů. Ale budu hovořit pouze o jedné z nich: pomáhají nám jasně myslet. Jasné myšlení je velmi důležité a docela obtížné, a proto potřebujeme jakoukoli podporu. V jakém jazyce bychom měli psát specifikace? To je obecně vždy první otázka pro programátory: v jakém jazyce budeme psát. Neexistuje jedna správná odpověď: problémy, které řešíme, jsou příliš rozmanité. Pro některé je užitečný TLA+ — to je jazyk specifikací, který jsem vyvinul. Pro jiné je pohodlnější používat čínštinu. Všechno závisí na situaci.
Je důležité se zaměřit na jinou otázku: jak dosáhnout jasnějšího myšlení? Odpověď: musíme myslet jako vědci. Tento způsob myšlení se v posledních 500 letech osvědčil. Ve vědě vytváříme matematické modely reality. Astronomie byla pravděpodobně prvním vědním oborem v pravém slova smyslu. V matematickém modelu používaném v astronomii jsou nebeská tělesa reprezentována jako body s hmotností, polohou a impulsem, i když ve skutečnosti jsou velmi složitými objekty s horami, oceány, přílivy a odlivy. Tento model, jako každý jiný, je navržen k řešení určitých úloh. Skvěle se hodí k určení, kam nasměrovat teleskop, pokud chceme najít planetu. Ale pokud chcete předpovědět počasí na této planetě, tento model neplatí.
Matematika nám umožňuje určit vlastnosti modelu. A věda ukazuje, jak se tyto vlastnosti vztahují k realitě. Pojďme mluvit o naší vědě, informatikě. Realita, se kterou pracujeme, jsou výpočetní systémy různých typů: procesory, herní konzole, počítače spouštějící programy a tak dále. Budu mluvit o vykonávání programu na počítači, ale obecně se všechny tyto závěry vztahují na jakýkoli výpočetní systém. V naší vědě používáme řadu různých modelů: Turingovy stroje, částečně uspořádané množiny událostí a mnoho dalších.
Co je to program? Je to jakýkoli kód, který lze považovat za samostatný. Představme si, že potřebujeme napsat prohlížeč. Máme tři úkoly: navrhnout uživatelské rozhraní programu, poté napsat vysoce úrovňový design programu a nakonec napsat kód. Během psaní kódu si uvědomujeme, že potřebujeme vytvořit nástroj pro formátování textu. Zde musíme opět vyřešit tři úkoly: definovat, jaký text tento nástroj vrátí; vybrat algoritmus pro formátování; napsat kód. Tato úloha má svou podúlohu: správně vkládat pomlčku do slov. Tuto podúlohu také řešíme ve třech krocích — jak vidíme, opakují se na mnoha úrovních.
Podívejme se podrobněji na první krok: jaký problém program řeší. Zde většinou modelujeme program jako funkci, která přijímá nějaké vstupy a vrací určité výstupy. V matematice je funkce obvykle popsána jako seřazená množina párů. Například funkce umocňování na druhou pro přirozená čísla je popsána jako množina {, , , , …}. Oblast definice této funkce je množina prvních elementů každého páru, tedy přirozená čísla. Abychom funkci definovali, musíme uvést její oblast definice a vzorec.
Ale v matematice funkce nejsou totéž jako funkce v programovacích jazycích. Matematika je mnohem jednodušší. Protože na složité příklady nemám čas, probereme jednoduchý: funkce v jazyce C nebo statická metoda v Javě, která vrací největší společný dělitel dvou celých čísel. Ve specifikaci této metody napíšeme: počítá GCD(M,N) pro argumenty M a N, kde GCD(M,N) — funkce, jejíž oblast definice je množina párů celých čísel, a návratová hodnota je největší celé číslo, které dělí M a N. Jak se tento model vztahuje na realitu? Model operuje s celými čísly, zatímco v C nebo Javě máme 32-bitový int. Tento model nám umožňuje posoudit, zda je algoritmus správný GCD, ale nezabrání chybě přetečení. Pro to by byl potřeba složitější model, na který není čas.
Pojďme si promluvit o omezeních funkce jako modelu. Práce některých programů (například operačních systémů) se nezakládá pouze na vracení určité hodnoty pro určité argumenty, mohou běžet nepřetržitě. Dále, funkce jako model je špatně přizpůsobena pro druhý krok: plánování způsobu řešení úkolu. Rychlé třídění a bublinkové třídění počítají stejnou funkci, ale jsou to zcela různé algoritmy. Proto pro popis způsobu dosažení cíle programu používám jiný model, nazvěme to standardní behaviorální model. V něm je program prezentován jako množina všech povolených chování, z nichž každé je sekvencí stavů, a stav je přiřazení hodnot proměnným.
Podívejme se, jak bude vypadat druhý krok pro Euklidův algoritmus. Musíme vypočítat GCD(M, N). Inicializujeme M jak x, a N jak y, poté opakovaně odečítáme menší z těchto proměnných od větší, dokud nebudou rovny. Například, pokud M = 12, a N = 18, můžeme popsat následující chování:
[x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6]
A pokud M = 0 a N = 0? Ноль делится на все числа, поэтому наибольшего делителя в этом случае нет. В этой ситуации нам нужно вернуться к первому шагу и спросить: действительно ли нам нужно вычислять НОД для неположительных чисел? Если в этом нет необходимости, то нужно просто изменить спецификацию.
Zde je třeba udělat malou odbočku o produktivitě. Často se měří počtem řádků kódu napsaných za den. Ale vaše práce je mnohem užitečnější, pokud se vám podařilo zbavit určitého množství řádků, protože máte méně prostoru pro chyby. A zbavit se kódu je nejjednodušší právě v prvním kroku. Je dost možné, že všechny ty vymoženosti, které se snažíte realizovat, jednoduše nepotřebujete. Nejrychlejší způsob, jak zjednodušit program a ušetřit čas, je nedělat věci, které dělat nemáte. Druhý krok je na druhém místě z hlediska potenciálu úspor času. Pokud měříte produktivitu podle počtu napsaných řádků, pak promýšlení způsobu, jak úkol splnit, vás učiní méně produktivními, protože stejný úkol vyřešíte menším objemem kódu. Přesnou statistiku tu uvést nemohu, protože nemám způsob, jak spočítat ty řádky, které jsem nenapsal díky tomu, že jsem strávil čas specifikací, tedy prvním a druhým krokem. A experiment tu také není možné provést, protože v experimentu nemáme právo vykonat první krok, úkol je předem definován.
Ve neformálních specifikacích je snadné přehlédnout mnoho obtíží. Není nic složitého na psaní přísných specifikací pro funkce, o tom diskutovat nebudu. Místo toho si promluvíme o psaní přísných specifikací pro standardní chování modelů. Existuje věta, která říká, že jakýkoli soubor chování může být popsán pomocí vlastnosti bezpečnosti (safety) a vlastnosti živosti (liveness). Bezpečnost znamená, že se nic špatného nestane, program nevydá nesprávnou odpověď. Odolnost znamená, že dříve či později dojde k něčemu dobrému, t. j. program dříve nebo později poskytne správnou odpověď. Obecně je bezpečnost důležitější ukazatel, protože chyby nejčastěji vznikají právě zde. Proto pro úsporu času nebudu hovořit o odolnosti, ačkoli ta je samozřejmě také důležitá.
Dosahujeme bezpečnosti tím, že nejprve definujeme množství možných výchozích stavů. A za druhé, vztahy se všemi možnými následujícími stavy pro každý stav. Budeme se chovat jako vědci a vymezíme stavy matematicky. Sada výchozích stavů je popsána vzorcem, například v případě Euklidova algoritmu: (x = M) ∧ (y = N). Pro určité hodnoty M a N existuje pouze jeden výchozí stav. Vztah k následujícímu stavu je popsán vzorcem, ve kterém jsou proměnné následujícího stavu zapsány s čárkou, a aktuálního stavu — bez čárky. V případě Euklidova algoritmu se budeme zabývat disjunkcí dvou vzorců, z nichž jeden x je nejvyšší hodnota, a ve druhém — y:
V prvním případě nové hodnoty y je rovno předchozí hodnotě y, a nové hodnoty x získáme odečtením menší proměnné od větší. V druhém případě uděláme opak.
Vraťme se k Euklidovu algoritmu. Předpokládejme znovu, že M = 12, N = 18. To určuje jediný výchozí stav, (x = 12) ∧ (y = 18). Poté tato hodnoty dosadíme do výše uvedeného vzorce a získáme:
Zde je jediným možným řešením: x' = 18 - 12 ∧ y' = 12, a dostáváme chování: [x = 12, y = 18]. Takto můžeme popsat všechny stavy našeho chování: [x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6].
V posledním stavu [x = 6, y = 6] budou obě části výrazu nepravdivé, což znamená, že dalšího stavu nemá. Takže máme úplnou specifikaci druhého kroku — jak vidíme, je to zcela běžná matematika, jako u inženýrů a vědců, a ne podivná, jak v informatice.
Tyto dvě formule lze sloučit do jedné formule temporální logiky. Je elegantní a není těžké ji vysvětlit, ale momentálně na to není čas. Temporální logika nám může být potřeba pouze pro vlastnost živosti, pro bezpečnost není nutná. Samotná temporální logika se mi nelíbí, není to úplně běžná matematika, ale v případě živosti je to nezbytné zlo.
V Euklidově algoritmu pro každou hodnotu x a y jsou unikátní hodnoty x' a y', které činí vztah s následujícím stavem pravdivým. Jinými slovy, Euklidův algoritmus je deterministický. Abychom modelovali nedeterministický algoritmus, musí mít současný stav několik možných budoucích stavů, a každá hodnota proměnné bez čárky by měla mít několik hodnot proměnné s čárkou, při nichž je vztah s následujícím stavem pravdivý. Není to těžké udělat, ale nyní nebudu uvádět příklady.
Abychom vytvořili funkční nástroj, potřebujeme formální matematiku. Jak udělat specifikaci formální? K tomu potřebujeme formální jazyk, například . Specifikace Euklidova algoritmu bude v tomto jazyce vypadat následovně:
Symbol znaku rovnosti s trojúhelníkem znamená, že hodnota vlevo od znaku je definována jako rovna hodnotě vpravo od znaku. V podstatě, specifikace je definice, v našem případě dvě definice. K specifikaci v TLA+ je třeba přidat prohlášení a nějakou syntaxi, jako na obrázku výše. V ASCII to bude vypadat takto:
Jak vidíme, nic složitého. Specifikaci v TLA+ lze ověřit, tj. procházet všechny možné chování v malé modelu. V našem případě je tímto modelem určité hodnoty M a N. To je velmi efektivní a jednoduchý způsob ověření, který probíhá plně automaticky. Navíc lze napsat formální důkazy pravdivosti a zkontrolovat je mechanicky, ale to zabere hodně času, takže to téměř nikdo nedělá.
Hlavní nevýhodou TLA+ je to, že je to matematika, a programátoři a počítačoví vědci se matematiky obávají. Na první pohled to zní jako vtip, ale bohužel to myslím naprosto vážně. Můj kolega mi právě vyprávěl, jak se snažil vysvětlit TLA+ několika vývojářům. Jakmile se na obrazovce objevily vzorce, jejich oči se okamžitě skleněně zaostřily. Takže pokud vás TLA+ děsí, můžete použít , což je takový druh hračkového programovacího jazyka. Výraz v PlusCal může být jakýmkoli výrazem TLA+, tedy, z podstaty, jakýmkoli matematickým výrazem. Kromě toho, PlusCal má syntaxi pro nedeterministické algoritmy. Díky tomu, že v PlusCal lze zapsat jakýkoli výraz TLA+, je výrazně výstižnější než jakýkoli skutečný programovací jazyk. Dále, PlusCal se kompiluje do snadno čitelné specifikace TLA+. To ovšem neznamená, že složitá specifikace PlusCal se promění v jednoduchou na TLA+ — pouze vzájemná shoda mezi nimi je zřejmá, nevznikne žádná dodatečná složitost. Nakonec lze tuto specifikaci ověřit pomocí nástrojů TLA+. Celkově může PlusCal pomoci překonat fobii z matematiky, snadno se chápe i programátorům a počítačovým vědcům. V minulosti jsem nějakou dobu (asi 10 let) publikoval algoritmy na něm.
Někdo může namítnout, že TLA+ a PlusCal — to je matematika, a ta funguje pouze na vymyšlených příkladech. V praxi však potřebujeme skutečný jazyk s typy, procedurami, objekty a tak dále. To však není pravda. Tady je, co píše Chris Newcomb, který pracoval v Amazonu: „Použili jsme TLA+ v deseti velkých projektech a v každém případě jeho použití mělo významný přínos pro vývoj, protože jsme dokázali odhalit nebezpečné chyby před jejich uvedením do produkce, a protože nám poskytl porozumění a sebedůvěru potřebnou pro agresivní optimalizace výkonu, které neovlivnily pravdivost programu“. Často slyšíme, že při používání formálních metod dostaneme neefektivní kód — v praxi je to však naprosto naopak. Dále je rozšířený názor, že manažery není možné přesvědčit o potřebě formálních metod, i když programátoři jsou přesvědčeni o jejich užitečnosti. A Newcomb píše: „Manažeři nyní všemožně povzbuzují k psaní specifikací v TLA+, a speciálně na to vyčleňují čas“. Takže když manažeři vidí, že TLA+ funguje, s radostí ho přijímají. Chris Newcomb to napsal asi před šesti měsíci (v říjnu 2014), nyní, jak vím, je TLA+ používáno v 14 projektech, a ne v 10. Další příklad se týká návrhu XBox 360. K Charlesi Teckerovi přišel stážista a napsal specifikaci pro systém paměti. Díky této specifikaci byla odhalena chyba, která by jinak zůstala nepovšimnuta, a kvůli které by každá XBox 360 selhávala po čtyřech hodinách používání. Inženýři z IBM potvrdili, že jejich testy by tuto chybu neobjevily.
Podrobněji o TLA+ si můžete přečíst na internetu, a teď pojďme mluvit o neformálních specifikacích. Zřídka píšeme programy, které vypočítávají nejmenší společný dělitel a podobně. Mnohem častěji píšeme programy jako nástroj pro strukturovaný tisk (pretty-printer), který jsem napsal pro TLA+. Po nejjednodušším zpracování by kód v TLA+ vypadal takto:
Ale v uvedeném příkladu chtěl uživatel pravděpodobně, aby byly znaky konjunkce a rovnosti zarovnány. Takže správné formátování by vypadalo spíše takto:
Zvažme další příklad:
Zde, naopak, bylo zarovnání znaků rovnosti, sčítání a násobení ve zdrojovém kódu náhodné, takže pro nejjednodušší zpracování je docela dostačující. Obecně neexistuje přesná matematická definice správného formátování, protože „správné“ v tomto případě znamená „takové, jaké chce uživatel“, a to nelze matematicky definovat.
Zdálo by se, že pokud nemáme definici pravdivosti, pak je specifikace zbytečná. Ale to není pravda. Pokud nevíme, co by přesně program měl udělat, neznamená to, že bychom neměli přemýšlet o jejím chodu — naopak, měli bychom na tom strávit ještě více úsilí. Specifikace je zde obzvlášť důležitá. Určit optimální program pro strukturovaný tisk není možné, ale to neznamená, že bychom se jí neměli věnovat vůbec, a psát kód jako proud vědomí — to není správné. Nakonec jsem napsal specifikaci se šesti pravidly s definicemi ve formě komentářů v Java souboru. Zde je příklad jednoho z pravidel: token left-comment je LeftComment zarovnaný s jeho pokrývajícím tokenem. Toto pravidlo je napsáno v, řekněme, matematické angličtině: Zarovnaný LeftComment, left-comment a pokrývající token — termíny s definicemi. Takto matematikové popisují matematiku: píší definice termínů a na jejich základě — pravidla. Užitečnost takové specifikace spočívá v tom, že pochopit a odladit šest pravidel je mnohem snazší než 850 řádků kódu. Musím říct, že napsat tato pravidla nebylo snadné, dost času bylo vynaloženo na jejich ladění. K tomu jsem napsal kód, který uváděl, které pravidlo se používá. Díky tomu, že jsem tato šest pravidel vyzkoušel na několika příkladech, nebylo potřeba ladit 850 řádků kódu a chyby se ukázalo snadno najít. V Java existují skvělé nástroje pro toto. Kdybych napsal kód jen tak, trvalo by mi to mnohem déle a formátování by bylo horší kvality.
Proč nebylo možné použít formální specifikaci? Z jedné strany, správnost provádění zde není příliš důležitá. Strukturovaný tisk určitě někomu nebude vyhovovat, takže jsem nemusím usilovat o správnou funkčnost ve všech neobvyklých situacích. Ještě důležitější je ten fakt, že jsem neměl adekvátní nástroje. Nástroj pro kontrolu modelů TLA+ je zde k ničemu, takže bych musel příklady psát ručně.
U uvedené specifikace existují rysy, které jsou společné pro všechny specifikace. Je to na vyšší úrovni než kód. Může být realizována v jakémkoli jazyce. Při jejím psaní jsou jakékoliv nástroje nebo metody zbytečné. Žádný kurz programování vám nepomůže napsat tuto specifikaci. A neexistují žádné nástroje, které by tuto specifikaci učinily zbytečnou, pokud tedy nepíšete jazyk speciálně pro psaní programů strukturálního tisku v TLA+. Nakonec, tato specifikace nic neříká o tom, jak přesně budeme psát kód, pouze uvádí, co tento kód dělá. Píšeme specifikaci, abychom nám pomohli promyslet problém, než začneme přemýšlet o kódu.
Ale tato specifikace má i rysy, které ji odlišují od ostatních specifikací. 95% ostatních specifikací je výrazně kratších a jednodušších:
Tato specifikace je soubor pravidel. Obecně je to znak špatné specifikace. Pochopit důsledky souboru pravidel je docela těžké, a právě proto jsem musel strávit hodně času jejich laděním. Nicméně v tomto případě jsem nenašel lepší způsob.
Je dobré zmínit několik slov o programech, které běží nepřetržitě. Obecně pracují paralelně, například operační systémy nebo distribuované systémy. Pochopit je v mysli nebo na papíře dokáže velmi málo lidí, a já mezi ně nepatřím, i když jsem to kdysi zvládal. Proto jsou potřeba nástroje, které budou kontrolovat naši práci — například TLA+ nebo PlusCal.
Proč bylo potřeba psát specifikaci, když jsem přece věděl, co má kód dělat? Ve skutečnosti jsem měl jen pocit, že to vím. Kromě toho, s existencí specifikace už cizí člověk nemusí šahat do kódu, aby pochopil, co vlastně dělá. Mám pravidlo: nemělo by existovat žádné obecné pravidlo. Toto pravidlo má samozřejmě výjimku, a to je jediné obecné pravidlo, kterého se držím: specifikace toho, co kód dělá, by měla lidem sdělovat vše, co potřebují vědět při používání tohoto kódu.
Co by měli programátoři vědět o myšlení? Začneme tím, co je nutné vědět všem: pokud nepíšete, jen si myslíte, že myslíte. Také je potřeba přemýšlet před tím, než kódíte, což znamená, že musíte psát předtím, než začnete kódovat. Specifikace je to, co píšeme před tím, než začneme kódovat. Specifikace je důležitá pro jakýkoliv kód, který může být použit nebo změněn kýmkoliv. A tím „kýmkoliv“ může být i autor kódu měsíc po jeho napsání. Specifikace je nutná pro velké programy a systémy, pro třídy, pro metody a někdy i pro složité části jednotlivé metody. Co přesně bychom měli o kódu napsat? Musíme popsat, co dělá, tedy to, co může být užitečné každému, kdo tento kód používá. Někdy může být také nutné uvést, jakým způsobem kód dosahuje svého cíle. Pokud tento způsob známe z kursu algoritmů, nazýváme to algoritmem. Pokud se jedná o něco specifičtějšího a nového, nazýváme to vysoce úrovňovým návrhem. Formálně zde žádný rozdíl není: oboje je abstraktním modelem programu.
Jak správně napsat specifikaci kódu? Hlavní pravidlo: musí být na úrovni nad samotným kódem. Musí popisovat stavy a chování. Musí být tak přísná, jak je úkol vyžaduje. Pokud píšete specifikaci způsobu realizace úkolu, můžete ji napsat v pseudokódu nebo pomocí PlusCal. Naučit se psát specifikace je nutné z formálních specifikací. To vám poskytne potřebné dovednosti, které pomohou i s neformálními. A jak se naučit psát formální specifikace? Když jsme se učili programování, psali jsme programy a pak je ladili. Totéž platí zde: musíte napsat specifikaci, zkontrolovat ji pomocí nástroje pro ověřování modelů a opravit chyby. TLA+ možná není nejlepší jazyk pro formální specifikaci, a pro vaše konkrétní potřeby pravděpodobně lépe vyhovuje jiný jazyk. Výhodou TLA+ je, že výborně učí matematickému myšlení.
Jak spojit specifikaci a kód? Pomocí komentářů, které propojují matematické pojmy a jejich realizaci. Pokud pracujete s grafy, na úrovni programu budete mít pole uzlů a pole vazeb. Proto musíte napsat, jak přesně je graf realizován těmito programovacími strukturami.
Je třeba poznamenat, že nic z výše uvedeného se netýká samotného procesu psaní kódu. Když píšete kód, tedy vykonáváte třetí krok, musíte také myslet a promýšlet program. Pokud se podúloha ukáže být obtížnou nebo nejasnou, je nutné pro ni napsat specifikaci. O samotném kódu zde však nemluvím. Můžete používat jakýkoli programovací jazyk, jakoukoli metodologii, o těchto věcech to není. Kromě toho nic z výše uvedeného neodstraňuje nutnost testovat a ladit kód. I když je abstraktní model napsán správně, v jeho realizaci mohou být chyby.
Psaní specifikací je další fází v procesu psaní kódu. Díky němu lze mnoho chyb chytit s menšími námahou — to víme z zkušenosti programátorů z Amazonu. Se specifikacemi se kvalita programů zvyšuje. Tak proč tedy tak často obejdeme bez nich? Protože psaní je obtížné. A psaní je obtížné, protože k tomu musíte myslet, a myslet je také těžké. Vždy je jednodušší dělat, že přemýšlíte. Můžeme tu provést analogii s běháním — čím méně běháte, tím pomalejší budete. Je třeba trénovat své svaly a cvičit v psaní. Potřebujete praxi.
Specifikace může být nesprávná. Mohli jste někde udělat chybu, nebo se mohly změnit požadavky, nebo bylo nutné provést vylepšení. Jakýkoliv kód, jejž někdo používá, se musí měnit, a proto dříve nebo později specifikace přestane odpovídat programu. Ideálně bychom v takovém případě měli napsat novou specifikaci a zcela přepracovat kód. Dobře víme, že to nikdo nedělá. V praxi patcheme kód a možná aktualizujeme specifikaci. Pokud se to pravidelně děje, proč vůbec psát specifikace? Za prvé, pro člověka, který bude upravovat váš kód, každé slovo navíc ve specifikaci bude mít cenu zlata, a tím člověkem můžete být klidně i vy sami. Často si nadávám za nedostatečnou specifikaci, když upravuji svůj kód. A já píši více specifikací než kódu. Proto, když upravujete kód, specifikaci je vždy nutné aktualizovat. Za druhé, s každou úpravou se kód zhoršuje, stává se čím dál tím těžším k přečtení a údržbě. Je to nárůst entropie. Ale pokud nezačnete se specifikací, každá napsaná řádka bude úpravou a kód bude na samém začátku objemný a obtížně čitelný.
Jak říkal , žádná bitva nebyla vyhrána podle plánu, a žádná bitva nebyla vyhrána bez plánu. A on věděl něco o bitvách. Existuje názor, že psaní specifikací je ztráta času. Někdy tomu tak opravdu je, a úkol je tak jednoduchý, že nad ním není co uvažovat. Ale vždy musíte mít na paměti, že když vám radí, abyste nepsali specifikace, znamená to, že vám radí, abyste nepřemýšleli. A o tom byste měli vždy přemýšlet. Promyšlení úkolu nezaručuje, že se vyhnete chybám. Jak víme, žádná kouzelná hůlka nebyla vynalezena a programování je složitá činnost. Ale pokud úkol nepromýšlíte, zaručeně uděláte chyby.
Další informace o TLA+ a PlusCal si můžete přečíst na speciální stránce, na kterou se lze dostat z mé domácí stránky . Tímto končím, děkuji za pozornost.
Připomínám, že se jedná o překlad. Když budete psát komentáře, pamatujte, že autor je nečetl. Pokud se s ním opravdu chcete spojit, bude na konferenci Hydra 2019, která se koná 11.-12. července 2019 v Petrohradu. Vstupenky lze zakoupit .
Zdroj: habr.com
