Tla+ pratico: Sviluppo guidato dalla pianificazione

Recensioni dei lettori

Il libro fornisce un'introduzione accessibile a PlusCal, un linguaggio che si compila in TLA+, con esempi pratici e uno stile didattico chiaro da parte dell'autore. È adatto ai principianti della verifica formale, anche se alcuni dettagli fondamentali di TLA+ possono essere trascurati. Ci sono errori minori e alcune aree in cui il contenuto sembra incompleto. Nel complesso, aiuta i lettori ad acquisire una certa padronanza di PlusCal, fungendo al contempo da potenziale trampolino di lancio per un'esplorazione più approfondita di TLA+.

⬤ Ottimi esempi e spiegazioni chiare
⬤ applicazione pratica di PlusCal
⬤ stile di scrittura accessibile
⬤ adatto ai principianti
⬤ esempi di utilizzo reali
⬤ ha aiutato i lettori a diventare esperti di PlusCal.

⬤ Il titolo è fuorviante in quanto si concentra più su PlusCal che sul nucleo di TLA+
⬤ sono presenti alcuni errori minori
⬤ mancano esercizi per l'autoverifica
⬤ alcune parti della sintassi e del contenuto possono essere confuse o incomplete
⬤ alcuni lettori potrebbero ritenere che sia necessario un contenuto più avanzato.

(basato su 6 recensioni dei lettori)

Titolo originale:

Practical Tla+: Planning Driven Development

Contenuto del libro:

Imparate a progettare programmi complessi e corretti e a risolvere i problemi prima di scrivere una sola riga di codice. Questo libro è una risorsa pratica e completa sulla programmazione TLA+ con esempi ricchi e complessi. Practical TLA+ mostra come utilizzare TLA+ per specificare un sistema complesso e testare il progetto stesso per individuare eventuali bug.

Imparerete come anche una breve specifica TLA+ possa trovare bug critici. Iniziate con un esempio di TLA+ utilizzato in un sistema di trasferimento bancario, per vedere come vi aiuta a progettare, testare e costruire un'applicazione migliore. Quindi, si apprenderanno i fondamenti degli operatori, della logica, delle funzioni, di PlusCal, dei modelli e della concorrenza di TLA+. Lungo il percorso scoprirete come organizzare i vostri progetti e come specificare i sistemi distribuiti e l'eventuale coerenza.

Infine, metterete in pratica quanto appreso con alcuni casi di studio, applicando TLA+ a un'ampia varietà di problemi pratici: dalle prestazioni degli algoritmi e dalle strutture dati al codice aziendale e a MapReduce. Dopo aver letto e utilizzato questo libro, avrete tutto ciò che vi serve per iniziare a usare TLA+ e per utilizzarlo nelle vostre applicazioni mission-critical.

Cosa imparerete

⬤ Leggere e scrivere le specifiche TLA+.

⬤ Controllare le specifiche per verificare la presenza di invarianti non validi, condizioni di gara e bug di liveness.

⬤ Progettare la concorrenza e i sistemi distribuiti.

⬤ Imparare come TLA+ può aiutarvi nel vostro lavoro di produzione quotidiano.

Per chi è questo libro?

Coloro che hanno esperienza di programmazione e sono nuovi alla progettazione e a TLA+.