Tento článek je překladem . Ale před ní malý úvod. Jak se tvoří zombie? Každý se dostal do situace, kdy chce posunout kamaráda nebo kolegu na svou úroveň, ale nejde to. A není to ani tak u vás, jako u něj, že „to nejde“: na jedné straně stupnice je normální plat, úkoly a tak dále a na druhé potřeba přemýšlet. Myšlení je nepříjemné a bolestivé. Rychle to vzdává a pokračuje v psaní kódu, aniž by vůbec zapnul mozek. Představujete si, kolik úsilí stojí překonat bariéru naučené bezmoci, a prostě to neuděláte. Tak vznikají zombie, které se, zdá se, dají vyléčit, ale zdá se, že to nikdo neudělá.
Když jsem to viděl (ano, ten samý soudruh z učebnic) a nevytváří zprávu, ale relaci otázek a odpovědí, byl jsem trochu opatrný. Pro každý případ, Leslie je světoznámý vědec, autor zásadních děl v distribuovaném počítání a můžete ho znát také podle písmen La ve slově LaTeX - „Lamport TeX“. Druhým alarmujícím faktorem je jeho požadavek: každý, kdo přijde, si musí (zcela zdarma) předem vyslechnout pár jeho reportáží, vymyslet na ně alespoň jednu otázku a teprve pak přijít. Rozhodl jsem se podívat, co tam Lamport vysílal – a je to skvělé! Je to přesně ta věc, magická pilulka na vyléčení zombie. Varuji vás: z textu se mohou výrazně spálit milovníci superflexibilních metodik a ti, kteří neradi testují napsané.
Po habrokat ve skutečnosti začíná překlad semináře. Příjemné čtení!
Ať už se ujmete jakéhokoli úkolu, vždy musíte projít třemi kroky:
- rozhodnout, jakého cíle chcete dosáhnout;
- rozhodnout, jak dosáhnete svého cíle;
- dojít ke svému cíli.
To platí i pro programování. Když píšeme kód, potřebujeme:
- rozhodnout, co má program dělat;
- určit, jak má plnit svůj úkol;
- napište odpovídající kód.
Poslední krok je samozřejmě velmi důležitý, ale o tom dnes nebudu mluvit. Místo toho budeme diskutovat o prvních dvou. Každý programátor je provádí před zahájením práce. Nesednete k psaní, pokud jste se nerozhodli, zda píšete prohlížeč nebo databázi. Musí být přítomna určitá představa o cíli. A určitě přemýšlíte o tom, co přesně program udělá, a nepište nějak v naději, že se kód nějak změní v prohlížeč.
Jak přesně k tomuto předběžnému promýšlení kódu dochází? Kolik úsilí bychom tomu měli věnovat? Vše záleží na tom, jak složitý problém řešíme. Předpokládejme, že chceme napsat distribuovaný systém odolný proti chybám. V tomto případě bychom si měli věci pečlivě promyslet, než si sedneme ke kódu. Co když potřebujeme zvýšit celočíselnou proměnnou o 1? Na první pohled je zde vše triviální a není třeba přemýšlet, ale pak si uvědomíme, že může dojít k přetečení. Proto i k tomu, abyste pochopili, zda je problém jednoduchý nebo složitý, musíte nejprve přemýšlet.
Pokud si předem promyslíte možná řešení problému, můžete se vyhnout chybám. Ale to vyžaduje, aby vaše myšlení bylo jasné. Abyste toho dosáhli, musíte si zapsat své myšlenky. Velmi se mi líbí citát Dicka Guindona: „Když píšete, příroda vám ukazuje, jak nedbalé je vaše myšlení.“ Pokud nepíšete, myslíte si pouze, že přemýšlíte. A své myšlenky si musíte zapsat ve formě specifikací.
Specifikace plní mnoho funkcí, zejména ve velkých projektech. Ale budu mluvit pouze o jednom z nich: pomáhají nám jasně myslet. Jasné myšlení je velmi důležité a docela obtížné, takže zde potřebujeme jakoukoli pomoc. V jakém jazyce bychom měli psát specifikace? Obecně je to vždy první otázka pro programátory: v jakém jazyce budeme psát. Na to neexistuje jediná správná odpověď: problémy, které řešíme, jsou příliš rozmanité. Pro některé je TLA+ jazyk specifikace, který jsem vyvinul. Pro ostatní je výhodnější používat čínštinu. Vše závisí na situaci.
Důležitější je jiná otázka: jak dosáhnout jasnějšího myšlení? Odpověď: Musíme myslet jako vědci. Toto je způsob myšlení, který se za posledních 500 let osvědčil. Ve vědě budujeme matematické modely reality. Astronomie byla možná první vědou v přísném slova smyslu. V matematickém modelu používaném v astronomii se nebeská tělesa jeví jako body s hmotností, polohou a hybností, i když ve skutečnosti jde o extrémně složité objekty s horami a oceány, přílivy a odlivy. Tento model, jako každý jiný, byl vytvořen k řešení určitých problémů. Je to skvělé pro určení, kam namířit dalekohled, pokud potřebujete najít planetu. Ale pokud chcete předpovídat počasí na této planetě, tento model nebude fungovat.
Matematika nám umožňuje určit vlastnosti modelu. A věda ukazuje, jak tyto vlastnosti souvisí s realitou. Pojďme se bavit o naší vědě, informatice. Realitou, se kterou pracujeme, jsou výpočetní systémy různého druhu: procesory, herní konzole, počítače, spouštěcí programy a tak dále. Budu mluvit o spuštění programu na počítači, ale celkově platí, že všechny tyto závěry platí pro jakýkoli výpočetní systém. V naší vědě používáme mnoho různých modelů: Turingův stroj, částečně uspořádané sady událostí a mnoho dalších.
co je to program? Toto je jakýkoli kód, který lze zvážit nezávisle. Předpokládejme, že potřebujeme napsat prohlížeč. Provádíme tři úkoly: navrhneme uživatelský pohled na program, poté napíšeme diagram na vysoké úrovni programu a nakonec napíšeme kód. Při psaní kódu si uvědomujeme, že potřebujeme napsat textový formátovač. Zde opět musíme vyřešit tři problémy: určit, jaký text tento nástroj vrátí; vyberte algoritmus pro formátování; napsat kód. Tento úkol má svůj dílčí úkol: správně vložit do slov spojovník. I tento dílčí úkol řešíme ve třech krocích – jak vidíte, opakují se na mnoha úrovních.
Podívejme se podrobněji na první krok: jaký problém program řeší. Zde nejčastěji modelujeme program jako funkci, která přijímá nějaký vstup a vytváří nějaký výstup. V matematice se funkce obvykle popisuje jako uspořádaná množina párů. Například kvadratura pro přirozená čísla je popsána jako množina {<0,0>, <1,1>, <2,4>, <3,9>, …}. Definičním oborem takové funkce je množina prvních prvků každé dvojice, tedy přirozených čísel. Abychom mohli definovat funkci, musíme určit její rozsah a vzorec.
Ale funkce v matematice nejsou totéž jako funkce v programovacích jazycích. Matematika je mnohem jednodušší. Protože nemám čas na složité příklady, uvažujme jeden jednoduchý: funkci v C nebo statickou metodu v Javě, která vrací největší společný dělitel dvou celých čísel. Ve specifikaci této metody budeme psát: počítá GCD(M,N) pro argumenty M и NKde GCD(M,N) - funkce, jejíž doménou je množina dvojic celých čísel a návratová hodnota je největší celé číslo, které je dělitelné číslem M и N. Jak tento model souvisí s realitou? Model funguje na celých číslech, zatímco v C nebo Javě máme 32bitový int. Tento model nám umožňuje rozhodnout, zda je algoritmus správný GCD, ale nezabrání chybám při přetečení. To by vyžadovalo složitější model, na který není čas.
Promluvme si o omezeních funkce jako modelu. Některé programy (například operační systémy) nejen vracejí určitou hodnotu pro určité argumenty, ale mohou běžet nepřetržitě. Navíc funkce jako model není příliš vhodná pro druhý krok: plánování, jak problém vyřešit. Rychlé třídění a třídění podle bublin počítají stejnou funkci, ale jsou to zcela odlišné algoritmy. Proto, abych popsal, jak je dosaženo cíle programu, používám jiný model, nazvěme ho standardní behaviorální model. Program v něm je reprezentován jako soubor všech přípustných chování, z nichž každé je zase posloupností stavů a stav je přiřazení hodnot proměnným.
Podívejme se, jak by vypadal druhý krok pro Euclidův algoritmus. Musíme počítat GCD(M, N). Inicializujeme M как xa N как y, pak opakovaně odečtěte menší z těchto proměnných od větší, dokud se nebudou rovnat. Například pokud M = 12a N = 18, můžeme popsat následující chování:
[x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6]
Pokud M = 0 и N = 0? Nula je dělitelná všemi čísly, takže v tomto případě neexistuje největší dělitel. V této situaci se musíme vrátit k prvnímu kroku a zeptat se: opravdu potřebujeme vypočítat GCD pro nekladná čísla? Pokud to není nutné, stačí změnit specifikaci.
Zde bychom měli udělat malou odbočku k produktivitě. Často se měří v počtu řádků kódu napsaných za den. Vaše práce je ale mnohem užitečnější, pokud se zbavíte určitého počtu řádků, protože máte méně místa pro chyby. A nejjednodušší způsob, jak se zbavit kódu, je v prvním kroku. Je zcela možné, že prostě nepotřebujete všechny zvonky a píšťalky, které se snažíte implementovat. Nejrychlejší způsob, jak zjednodušit program a ušetřit čas, je nedělat věci, které by se dělat neměly. Druhý krok je druhým nejvíce časově úsporným potenciálem. Pokud měříte produktivitu na základě napsaných řádků, pak vás přiměje přemýšlet o tom, jak splnit úkol méně produktivní, protože stejný problém můžete vyřešit s menším množstvím kódu. Nemohu zde uvést přesnou statistiku, protože nemám jak spočítat počet řádků, které jsem nenapsal kvůli tomu, že jsem strávil čas nad specifikací, tedy prvním a druhým krokem. A experiment zde také nelze nastavit, protože v experimentu nemáme právo dokončit první krok, úkol je předem daný.
Je snadné přehlédnout mnoho obtíží v neformálních specifikacích. Na sepsání striktních specifikací pro funkce není nic složitého, o tom nebudu diskutovat. Místo toho budeme mluvit o psaní silných specifikací pro standardní chování. Existuje teorém, který říká, že pomocí vlastnosti zabezpečení lze popsat jakoukoli sadu chování (bezpečnost) a vlastnosti přežití (živost). Zabezpečení znamená, že se nestane nic špatného, program neposkytne nesprávnou odpověď. Přežití znamená, že dříve nebo později se stane něco dobrého, tj. program dá dříve nebo později správnou odpověď. Bezpečnost je zpravidla důležitějším ukazatelem, zde dochází nejčastěji k chybám. Proto pro úsporu času nebudu mluvit o přežití, i když je samozřejmě také důležitá.
Bezpečnosti dosáhneme předepsáním, nejprve, množiny možných počátečních stavů. A za druhé, vztahy se všemi možnými dalšími stavy pro každý stát. Chovejme se jako vědci a definujme stavy matematicky. Množina počátečních stavů je popsána vzorcem, například v případě Euklidova algoritmu: (x = M) ∧ (y = N). Pro určité hodnoty M и N existuje pouze jeden počáteční stav. Vztah k dalšímu stavu je popsán vzorcem, ve kterém jsou proměnné následujícího stavu zapsány s prvočíslem a proměnné aktuálního stavu jsou zapsány bez prvočísla. V případě Euklidova algoritmu se budeme zabývat disjunkcí dvou formulí, z nichž jedna x je největší hodnota a ve druhé - y:
V prvním případě je nová hodnota y rovna předchozí hodnotě y a novou hodnotu x získáme odečtením menší proměnné od větší. V druhém případě postupujeme opačně.
Vraťme se k Euklidovu algoritmu. Předpokládejme, že znovu M = 12, N = 18. To definuje jediný počáteční stav, (x = 12) ∧ (y = 18). Tyto hodnoty pak zapojíme do výše uvedeného vzorce a získáme:
Zde je jediné možné řešení: x' = 18 - 12 ∧ y' = 12a dostaneme chování: [x = 12, y = 18]. Podobně 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] obě části výrazu budou nepravdivé, takže nemá žádný další stav. Takže máme kompletní specifikaci druhého kroku - jak vidíte, je to docela obyčejná matematika jako u inženýrů a vědců a ne divná, jako v informatice.
Tyto dva vzorce lze spojit do jednoho vzorce časové logiky. Je elegantní a snadno se vysvětluje, ale teď na ni není čas. Časovou logiku můžeme potřebovat jen pro živost, pro bezpečnost ji nepotřebujeme. Časová logika jako taková mě nebaví, není to úplně obyčejná matematika, ale v případě živosti je to nutné zlo.
V Euklidově algoritmu pro každou hodnotu x и y mají jedinečné hodnoty x' и y', které činí vztah s dalším stavem pravdivým. Jinými slovy, Euklidův algoritmus je deterministický. Aby bylo možné modelovat nedeterministický algoritmus, musí mít aktuální stav několik možných budoucích stavů a každá hodnota proměnné bez primární báze má více hodnot primárních proměnných, takže vztah k dalšímu stavu je pravdivý. To je snadné, ale nebudu nyní uvádět příklady.
K výrobě pracovního nástroje potřebujete formální matematiku. Jak učinit specifikaci formální? K tomu potřebujeme formální jazyk, např. . Specifikace Euklidova algoritmu by v tomto jazyce vypadala takto:
Symbol rovnítka s trojúhelníkem znamená, že hodnota nalevo od znaménka je definována jako rovna hodnotě napravo od znaménka. Specifikace je v podstatě definice, v našem případě dvě definice. Ke specifikaci v TLA+ je potřeba přidat deklarace a nějakou syntaxi, jako na snímku výše. V ASCII by to vypadalo takto:
Jak vidíte, nic složitého. Specifikace pro TLA+ lze otestovat, tj. obejít všechna možná chování v malém modelu. V našem případě tento model bude mít určité hodnoty M и N. Jedná se o velmi účinnou a jednoduchou metodu ověřování, která je zcela automatická. Je také možné psát formální pravdivostní důkazy a kontrolovat je mechanicky, ale to zabere hodně času, takže to skoro nikdo nedělá.
Hlavní nevýhodou TLA+ je, že je to matematika a programátoři a informatici se matematiky bojí. Na první pohled to zní jako vtip, ale bohužel to myslím úplně 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 vzorce objevily na obrazovce, okamžitě se z nich staly skleněné oči. Takže pokud vás TLA+ děsí, můžete použít , je to takový hračkářský programovací jazyk. Výrazem v PlusCal může být jakýkoli výraz TLA+, tedy celkově jakýkoli matematický výraz. PlusCal má navíc syntaxi pro nedeterministické algoritmy. Protože PlusCal dokáže napsat jakýkoli výraz TLA+, je PlusCal mnohem výraznější než jakýkoli skutečný programovací jazyk. Dále je PlusCal zkompilován do snadno čitelné specifikace TLA+. To samozřejmě neznamená, že se složitá specifikace PlusCal promění v jednoduchou na TLA + - jen vzájemná korespondence je zřejmá, žádná další složitost nebude. Nakonec lze tuto specifikaci ověřit pomocí nástrojů TLA+. Celkově vzato může PlusCal pomoci překonat matematickou fobii a je snadno srozumitelný i pro programátory a počítačové vědce. V minulosti jsem na něm nějakou dobu (asi 10 let) publikoval algoritmy.
Možná někdo namítne, že TLA + a PlusCal je matematika a matematika funguje jen na vymyšlených příkladech. V praxi potřebujete skutečný jazyk s typy, procedurami, objekty a tak dále. To je špatně. Zde je to, co Chris Newcomb, který pracoval v Amazonu, píše: „Použili jsme TLA+ na deseti velkých projektech a v každém z nich to znamenalo významný rozdíl ve vývoji, protože jsme byli schopni zachytit nebezpečné chyby ještě před zahájením výroby a protože nám to dalo vhled a jistotu, kterou jsme potřebovali k agresivnímu výkonu. optimalizace bez ovlivnění pravdivosti programu". Často můžete slyšet, že při použití formálních metod dostáváme neefektivní kód – v praxi je vše přesně naopak. Navíc existuje názor, že manažery nelze přesvědčit o potřebě formálních metod, i když jsou programátoři přesvědčeni o jejich užitečnosti. A Newcomb píše: „Manažeři nyní tvrdě tlačí na sepsání specifikací pro TLA + a konkrétně na to přidělují čas“. Takže když manažeři vidí, že TLA+ funguje, rádi to přijmou. Chris Newcomb to napsal asi před půl rokem (říjen 2014), ale nyní, pokud vím, se TLA+ používá ve 14 projektech, ne v 10. Další příklad je v designu XBoxu 360. Za Charlesem Thackerem přišel stážista a napsal specifikaci pro paměťový systém. Díky této specifikaci byla nalezena chyba, která by jinak zůstala nepovšimnuta a kvůli které by každý XBox 360 po čtyřech hodinách používání spadl. Inženýři IBM potvrdili, že jejich testy by tuto chybu nenašly.
Více o TLA + si můžete přečíst na internetu, ale nyní si povíme něco o neformálních specifikacích. Málokdy musíme psát programy, které počítají nejmenšího společného dělitele a podobně. Mnohem častěji píšeme programy, jako je nástroj pretty-printer, který jsem napsal pro TLA+. Po nejjednodušším zpracování by kód TLA + vypadal takto:
Ale ve výše uvedeném příkladu uživatel s největší pravděpodobností chtěl, aby spojka a rovnítko byly zarovnány. Správné formátování by tedy vypadalo spíše takto:
Zvažte další příklad:
Zde bylo naopak zarovnání znamének rovná se, sčítání a násobení ve zdroji náhodné, takže úplně stačí to nejjednodušší zpracování. Obecně neexistuje přesná matematická definice správného formátování, protože „správné“ v tomto případě znamená „co uživatel chce“, a to nelze matematicky určit.
Zdálo by se, že pokud nemáme definici pravdy, pak je specifikace k ničemu. Ale není. To, že nevíme, co má program dělat, neznamená, že nemusíme přemýšlet o tom, jak funguje – naopak, musíme do toho vynaložit ještě více úsilí. Specifikace je zde obzvláště důležitá. Určit optimální program pro strukturovaný tisk nelze, ale to neznamená, že bychom ho vůbec neměli brát a psát kód jako proud vědomí není dobrá věc. Na závěr jsem napsal specifikaci šesti pravidel s definicemi ve formě komentářů v souboru java. Zde je příklad jednoho z pravidel: a left-comment token is LeftComment aligned with its covering token. Toto pravidlo je napsáno, řekněme, matematickou angličtinou: LeftComment aligned, left-comment и covering token - termíny s definicemi. Matematici tak popisují matematiku: píší definice pojmů a na jejich základě pravidla. Výhodou takové specifikace je, že šest pravidel je mnohem snazší pochopit a ladit než 850 řádků kódu. Musím říct, že napsat tato pravidla nebylo jednoduché, jejich odladění zabralo poměrně hodně času. Speciálně pro tento účel jsem napsal kód, který hlásil, které pravidlo bylo použito. Díky tomu, že jsem těchto šest pravidel testoval na několika příkladech, nemusel jsem ladit 850 řádků kódu a chyby se hledaly celkem snadno. Java má na to skvělé nástroje. Kdybych kód napsal jen tak, trvalo by mi to mnohem déle a formátování by bylo horší kvality.
Proč nemohla být použita formální specifikace? Na jedné straně zde není příliš důležité správné provedení. Strukturální výtisky určitě nikoho nepotěší, takže jsem nemusel ve všech zvláštních situacích správně fungovat. Ještě důležitější je fakt, že jsem neměl adekvátní nástroje. Kontrola modelu TLA+ je zde k ničemu, takže bych musel příklady psát ručně.
Výše uvedená specifikace má vlastnosti společné pro všechny specifikace. Je to vyšší úroveň než kód. Může být implementován v jakémkoli jazyce. Jakékoli nástroje nebo metody jsou pro jeho psaní k ničemu. Při psaní této specifikace vám žádný kurz programování nepomůže. A neexistují žádné nástroje, které by mohly učinit tuto specifikaci zbytečnou, pokud samozřejmě nepíšete jazyk speciálně pro psaní strukturovaných tiskových programů v TLA+. Nakonec tato specifikace neříká nic o tom, jak přesně kód napíšeme, pouze uvádí, co kód dělá. Píšeme specifikaci, která nám pomůže promyslet problém, než začneme přemýšlet o kódu.
Tato specifikace má ale také vlastnosti, které ji odlišují od ostatních specifikací. 95 % ostatních specifikací je výrazně kratších a jednodušších:
Dále je tato specifikace souborem pravidel. Zpravidla je to známka špatné specifikace. Pochopení důsledků sady pravidel je poměrně obtížné, a proto jsem musel strávit spoustu času jejich laděním. V tomto případě jsem však nemohl najít lepší způsob.
Stojí za to říci pár slov o programech, které běží nepřetržitě. Zpravidla pracují paralelně, například operační systémy nebo distribuované systémy. Jen velmi málo lidí jim rozumí mentálně nebo na papíře a já mezi ně nepatřím, i když jsem to kdysi dokázal. Potřebujeme proto nástroje, které naši práci prověří – například TLA+ nebo PlusCal.
Proč bylo nutné napsat specifikaci, když už jsem věděl, co přesně má kód dělat? Ve skutečnosti jsem si jen myslel, že to vím. Se specifikací se navíc člověk zvenčí již nemusí dostat do kódu, aby pochopil, co přesně dělá. Mám pravidlo: neměla by existovat žádná obecná pravidla. Z tohoto pravidla existuje samozřejmě výjimka, je to jediné obecné pravidlo, které dodržuji: specifikace toho, co kód dělá, by měla lidem sdělit vše, co potřebují vědět při používání kódu.
Co přesně tedy potřebují programátoři vědět o myšlení? Pro začátek to samé jako všichni ostatní: pokud nepíšete, pak se vám jen zdá, že přemýšlíte. Také musíte přemýšlet, než začnete kódovat, což znamená, že musíte psát, než začnete kódovat. Specifikace je to, co napíšeme, než začneme kódovat. Specifikace je potřeba pro jakýkoli kód, který může kdokoli použít nebo upravit. A tento „někdo“ může být sám autorem kódu měsíc po jeho napsání. Specifikace je potřebná pro velké programy a systémy, pro třídy, pro metody a někdy i pro složité části jedné metody. Co přesně by se mělo o kódu napsat? Musíte popsat, co to dělá, to znamená, co může být užitečné pro každého, kdo používá tento kód. Někdy může být také nutné specifikovat, jak kód plní svůj účel. Pokud jsme touto metodou prošli v průběhu algoritmů, pak ji nazýváme algoritmus. Pokud jde o něco speciálnějšího a nového, pak tomu říkáme design na vysoké úrovni. Není zde žádný formální rozdíl: oba jsou abstraktním modelem programu.
Jak přesně byste měli napsat specifikaci kódu? Hlavní věc: měla by být o úroveň výše než samotný kód. Měl by popisovat stavy a chování. Mělo by být tak přísné, jak úkol vyžaduje. Pokud píšete specifikaci toho, jak má být úloha implementována, můžete ji napsat v pseudokódu nebo pomocí PlusCal. Musíte se naučit, jak psát specifikace na formálních specifikacích. Získáte tak potřebné dovednosti, které vám pomohou i s těmi neformálními. Jak se naučíte psát formální specifikace? Když jsme se naučili programovat, psali jsme programy a pak je ladili. Zde je to stejné: napište specifikaci, zkontrolujte ji pomocí kontroly modelů a opravte chyby. TLA+ nemusí být nejlepší jazyk pro formální specifikaci a jiný jazyk bude pravděpodobně lepší pro vaše specifické potřeby. Výhodou TLA+ je, že velmi dobře učí matematické myšlení.
Jak propojit specifikaci a kód? S pomocí komentářů, které propojují matematické pojmy a jejich implementaci. Pokud pracujete s grafy, tak na úrovni programu budete mít pole uzlů a pole vazeb. Proto musíte přesně napsat, jak je graf implementován těmito programovacími strukturami.
Je třeba poznamenat, že nic z výše uvedeného neplatí pro samotný proces psaní kódu. Když píšete kód, to znamená, že provádíte třetí krok, musíte také přemýšlet a promyslet program. Pokud se dílčí úkol ukáže jako složitý nebo nezřejmý, musíte pro něj napsat specifikaci. Ale nemluvím zde o samotném kódu. Můžete použít jakýkoli programovací jazyk, jakoukoli metodiku, není to o nich. Nic z výše uvedeného také nevylučuje nutnost testovat a ladit kód. I když je abstraktní model napsán správně, mohou se v jeho implementaci vyskytnout chyby.
Psaní specifikací je dalším krokem v procesu kódování. Díky němu lze s menší námahou zachytit mnoho chyb – známe to ze zkušeností programátorů z Amazonu. Se specifikacemi se kvalita programů zvyšuje. Tak proč tedy tak často chodíme bez nich? Protože psaní je těžké. A psaní je obtížné, protože k tomu musíte myslet a myšlení je také obtížné. Vždy je snazší předstírat, co si myslíte. Zde můžete nakreslit analogii s běháním – čím méně běháte, tím pomaleji běháte. Musíte trénovat svaly a cvičit psaní. Potřebujete praxi.
Specifikace může být nesprávná. Je možné, že jste někde udělali chybu nebo se požadavky změnily nebo je třeba provést vylepšení. Jakýkoli kód, který kdokoli používá, se musí změnit, takže dříve nebo později nebude specifikace programu odpovídat. V ideálním případě je v tomto případě potřeba napsat novou specifikaci a kompletně přepsat kód. Dobře víme, že to nikdo nedělá. V praxi opravujeme kód a případně aktualizujeme specifikaci. Pokud se to dříve nebo později stane, proč vůbec psát specifikace? Za prvé, pro osobu, která bude upravovat váš kód, bude mít každé slovo navíc ve specifikaci cenu zlata a touto osobou můžete být klidně vy. Často se nadávám, že při úpravě kódu nedostávám dostatečnou specifikaci. A píšu více specifikací než kódu. Proto je při úpravě kódu vždy potřeba aktualizovat specifikaci. Za druhé, s každou revizí se kód zhoršuje, je stále obtížnější jej číst a udržovat. To je nárůst entropie. Ale pokud nezačnete specifikací, pak každý řádek, který napíšete, bude úpravou a kód bude od začátku nepraktický a těžko čitelný.
Jak bylo řečeno , žádná bitva nebyla vyhrána plánem a žádná bitva nebyla vyhrána bez plánu. A věděl něco o bitvách. Existuje názor, že psaní specifikací je ztráta času. Někdy je to pravda a úkol je tak jednoduchý, že není o čem přemýšlet. Ale měli byste si vždy pamatovat, že když vám bude řečeno, abyste nepsali specifikace, bylo vám řečeno, abyste nepřemýšleli. A měli byste na to myslet pokaždé. Promyšlení úkolu nezaručí, že nebudete dělat chyby. Jak víme, kouzelnou hůlku nikdo nevynalezl a programování je obtížný úkol. Pokud ale problém nepromyslíte, zaručeně uděláte chyby.
Více o TLA + a PlusCal si můžete přečíst na speciální webové stránce, můžete tam přejít z mé domovské stránky . To je z mé strany vše, děkuji za pozornost.
Upozorňujeme, že se jedná o překlad. Když budete psát komentáře, pamatujte, že je autor nebude číst. Pokud si s autorem chcete opravdu popovídat, pak bude na konferenci Hydra 2019, která se bude konat 11. – 12. července 2019 v Petrohradu. Vstupenky je možné zakoupit .
Zdroj: www.habr.com