Note :

Ce livre fournit une introduction accessible à PlusCal, un langage qui compile dans TLA+, avec des exemples pratiques et un style d'enseignement clair de la part de l'auteur. Il est bien adapté aux débutants en vérification formelle, bien que certains détails essentiels de TLA+ puissent être négligés. Il y a des erreurs mineures et quelques domaines où le contenu semble incomplet. Dans l'ensemble, il aide les lecteurs à acquérir des compétences dans PlusCal tout en servant de tremplin potentiel pour une exploration plus approfondie de TLA+.
Avantages:⬤ De bons exemples et des explications claires
⬤ une application pratique de PlusCal
⬤ un style accessible
⬤ bien adapté aux débutants
⬤ des exemples concrets d'utilisation
⬤ ont aidé les lecteurs à devenir compétents avec PlusCal.
⬤ Le titre est trompeur car il se concentre plus sur PlusCal que sur TLA+
⬤ quelques erreurs mineures présentes
⬤ manque d'exercices pour l'auto-test
⬤ certaines parties de la syntaxe et du contenu peuvent être confuses ou incomplètes
⬤ certains lecteurs peuvent penser qu'il a besoin d'un contenu plus avancé.
(basé sur 6 avis de lecteurs)
Practical Tla+: Planning Driven Development
Apprenez à concevoir des programmes complexes et corrects et à résoudre les problèmes avant d'écrire une seule ligne de code. Ce livre est une ressource pratique et complète sur la programmation TLA+ avec des exemples riches et complexes. Practical TLA+ vous montre comment utiliser TLA+ pour spécifier un système complexe et tester la conception elle-même pour détecter les bogues.
Vous apprendrez comment même une spécification TLA+ courte peut trouver des bogues critiques. Commencez par vous familiariser avec un exemple de TLA+ utilisé dans un système de transfert bancaire, pour voir comment il vous aide à concevoir, tester et construire une meilleure application. Ensuite, vous apprendrez les bases des opérateurs TLA+, de la logique, des fonctions, de PlusCal, des modèles et de la concurrence. En cours de route, vous découvrirez comment organiser vos plans et comment spécifier les systèmes distribués et la cohérence éventuelle.
Enfin, vous mettrez en pratique ce que vous avez appris à l'aide de quelques études de cas, en appliquant TLA+ à une grande variété de problèmes pratiques : de la performance des algorithmes et des structures de données au code d'entreprise et à MapReduce. Après avoir lu et utilisé ce livre, vous aurez tout ce qu'il faut pour commencer à utiliser TLA+ et l'appliquer à vos applications critiques.
Ce que vous apprendrez
⬤ Lire et écrire des spécifications TLA+.
⬤ Vérifier les spécifications pour les invariants brisés, les conditions de course, et les bogues de vivacité.
⬤ Concevoir des systèmes concurrentiels et distribués.
⬤ Apprenez comment TLA+ peut vous aider dans votre travail de production quotidien.
A qui s'adresse ce livre ?
Ceux qui ont une expérience de la programmation et qui découvrent la conception et TLA+.