Tla+ praktická: Plánováním řízený vývoj

Recenze čtenářů

Kniha poskytuje přístupný úvod do jazyka PlusCal, který se kompiluje do TLA+, s praktickými příklady a jasným stylem výuky od autora. Je vhodná pro začátečníky ve formální verifikaci, i když některé základní detaily TLA+ mohou být přehlédnuty. Vyskytují se zde drobné chyby a některé oblasti, kde se obsah zdá být neúplný. Celkově pomáhá čtenářům získat dovednosti v PlusCal a zároveň slouží jako potenciální odrazový můstek pro hlubší zkoumání TLA+.

⬤ Skvělé příklady a jasná vysvětlení
⬤ praktická aplikace PlusCal
⬤ přístupný styl psaní
⬤ dobře přizpůsobený začátečníkům
⬤ příklady použití v reálném světě
⬤ pomohly čtenářům stát se zběhlými v PlusCal.

⬤ Název je zavádějící, protože se zaměřuje více na PlusCal než na jádro TLA+
⬤ přítomny některé drobné chyby
⬤ chybí cvičení pro vlastní testování
⬤ některé části syntaxe a obsahu mohou být matoucí nebo neúplné
⬤ někteří čtenáři mohou mít pocit, že by to chtělo pokročilejší obsah.

(na základě 6 hodnocení čtenářů)

Původní název:

Practical Tla+: Planning Driven Development

Obsah knihy:

Naučte se navrhovat složité a správné programy a řešit problémy ještě před napsáním jediného řádku kódu. Tato kniha je praktickým, komplexním zdrojem informací o programování v TLA+ s bohatými, komplexními příklady. Praktický TLA+ vám ukáže, jak pomocí TLA+ specifikovat složitý systém a testovat samotný návrh na chyby.

Dozvíte se, jak i krátká specifikace TLA+ může najít kritické chyby. Začněte tím, že si smočíte nohy na příkladu TLA+ použitém v systému bankovních převodů, abyste zjistili, jak vám pomůže navrhnout, otestovat a vytvořit lepší aplikaci. Poté se seznámíte se základy operátorů TLA+, logiky, funkcí, PlusCal, modelů a souběhu. Cestou zjistíte, jak organizovat své plány a jak specifikovat distribuované systémy a případnou konzistenci.

Nakonec si osvojené poznatky vyzkoušíte v praxi s několika pracovními aplikacemi případových studií, které aplikují TLA+ na nejrůznější praktické problémy: od výkonu algoritmů a datových struktur až po obchodní kód a MapReduce. Po přečtení a použití této knihy budete mít vše, co potřebujete k tomu, abyste mohli začít pracovat s TLA+ a jak jej používat ve svých kritických aplikacích.

Co se naučíte

⬤ Číst a psát specifikace TLA+.

⬤ Kontrolovat specifikace na porušené invarianty, závodní podmínky a chyby živosti.

⬤ Navrhování souběžných a distribuovaných systémů.

⬤ Zjistěte, jak vám TLA+ může pomoci při každodenní produkční práci.

Pro koho je tato kniha určena

Těm, kteří mají zkušenosti s programováním a jsou v oblasti návrhu a TLA+ nováčky.