Tla+ practic: Dezvoltarea bazată pe planificare

Recenzii ale cititorilor

Cartea oferă o introducere accesibilă la PlusCal, un limbaj care se compilează în TLA+, cu exemple practice și un stil clar de predare din partea autorului. Este bine adaptată pentru începători în verificarea formală, deși unele detalii de bază ale TLA+ pot fi trecute cu vederea. Există erori minore și unele zone în care conținutul pare incomplet. În general, ajută cititorii să câștige competență în PlusCal, servind în același timp ca un potențial punct de plecare pentru o explorare mai profundă a TLA+.

⬤ Exemple excelente și explicații clare
⬤ aplicare practică a PlusCal
⬤ stil de scriere abordabil
⬤ bine adaptat pentru începători
⬤ exemple reale de utilizare
⬤ a ajutat cititorii să devină competenți în PlusCal.

⬤ Titlul induce în eroare deoarece se concentrează mai mult pe PlusCal decât pe TLA+ de bază
⬤ sunt prezente unele erori minore
⬤ lipsesc exercițiile pentru autotestare
⬤ anumite părți ale sintaxei și ale conținutului pot fi confuze sau incomplete
⬤ unii cititori pot considera că este nevoie de un conținut mai avansat.

(pe baza a 6 recenzii ale cititorilor)

Titlul original:

Practical Tla+: Planning Driven Development

Conținutul cărții:

Învățați cum să proiectați programe complexe, corecte și să rezolvați problemele înainte de a scrie un singur rând de cod. Această carte este o resursă practică și cuprinzătoare privind programarea TLA+ cu exemple bogate și complexe. Practical TLA+ vă arată cum să utilizați TLA+ pentru a specifica un sistem complex și pentru a testa designul în sine pentru erori.

Veți învăța cum chiar și o specificație TLA+ scurtă poate găsi erori critice. Începeți prin a vă familiariza cu un exemplu de TLA+ utilizat într-un sistem de transfer bancar, pentru a vedea cum vă ajută să proiectați, să testați și să construiți o aplicație mai bună. Apoi, obțineți câteva noțiuni de bază despre operatorii TLA+, logică, funcții, PlusCal, modele și simultaneitate. Pe parcurs, veți descoperi cum să vă organizați schițele și cum să specificați sistemele distribuite și consecvența eventuală.

În cele din urmă, veți pune în practică ceea ce învățați cu ajutorul unor aplicații de studiu de caz funcționale, aplicând TLA+ la o mare varietate de probleme practice: de la performanța algoritmilor și structurile de date la codul de afaceri și MapReduce. După citirea și utilizarea acestei cărți, veți avea tot ce vă trebuie pentru a începe să utilizați TLA+ și cum să îl utilizați în aplicațiile dvs. critice.

Ce veți învăța

⬤ Luați și scrieți specificații TLA+.

⬤ Verificați specificațiile pentru invariante rupte, condiții de cursă și erori de liveness.

⬤ Proiectați sisteme distribuite și de simultaneitate.

⬤ Învățați cum vă poate ajuta TLA+ în activitatea dvs. de producție de zi cu zi.

Pentru cine este această carte

Cei cu experiență în programare care sunt noi în proiectare și în TLA+.