Tla+ práctico: Desarrollo basado en la planificación

Opiniones de los lectores

El libro proporciona una introducción accesible a PlusCal, un lenguaje que se compila en TLA+, con ejemplos prácticos y un estilo de enseñanza claro por parte del autor. Es adecuado para principiantes en la verificación formal, aunque pueden pasarse por alto algunos detalles básicos de TLA+. Hay errores menores y algunas áreas en las que el contenido parece incompleto. En general, ayuda a los lectores a adquirir destreza en PlusCal al tiempo que sirve como un posible trampolín para una exploración más profunda de TLA+.

⬤ Grandes ejemplos y explicaciones claras
⬤ aplicación práctica de PlusCal
⬤ estilo de escritura accesible
⬤ muy adecuado para principiantes
⬤ ejemplos de uso del mundo real
⬤ ayudó a los lectores a dominar PlusCal.

⬤ El título es engañoso ya que se centra más en PlusCal que en el núcleo de TLA+
⬤ algunos errores menores presentes
⬤ carece de ejercicios para autoevaluación
⬤ ciertas partes de la sintaxis y el contenido pueden ser confusas o incompletas
⬤ algunos lectores pueden sentir que necesita un contenido más avanzado.

(basado en 6 opiniones de lectores)

Título original:

Practical Tla+: Planning Driven Development

Contenido del libro:

Aprenda a diseñar programas complejos y correctos y a solucionar problemas antes de escribir una sola línea de código. Este libro es un recurso práctico y completo sobre la programación TLA+ con ejemplos ricos y complejos. Practical TLA+ le muestra cómo utilizar TLA+ para especificar un sistema complejo y probar el propio diseño en busca de errores.

Aprenderá cómo incluso una especificación TLA+ corta puede encontrar errores críticos. Empiece mojándose los pies con un ejemplo de TLA+ utilizado en un sistema de transferencia bancaria, para ver cómo le ayuda a diseñar, probar y construir una aplicación mejor. A continuación, conozca los fundamentos de los operadores, la lógica, las funciones, PlusCal, los modelos y la concurrencia de TLA+. A lo largo del camino descubrirá cómo organizar sus planos y cómo especificar sistemas distribuidos y consistencia eventual.

Por último, pondrá en práctica lo aprendido con algunas aplicaciones de casos prácticos, aplicando TLA+ a una amplia variedad de problemas prácticos: desde rendimiento de algoritmos y estructuras de datos hasta código empresarial y MapReduce. Después de leer y utilizar este libro, tendrá lo que necesita para empezar con TLA+ y cómo utilizarlo en sus aplicaciones de misión crítica.

Lo que aprenderá

⬤ Leer y escribir especificaciones TLA+.

⬤ Comprobar invariantes rotas, condiciones de carrera y bugs de liveness.

⬤ Diseñar sistemas concurrentes y distribuidos.

⬤ Aprenda cómo TLA+ puede ayudarle en su trabajo diario de producción.

Para quién es este libro

Aquellos con experiencia en programación que son nuevos en el diseño y en TLA+.