Goodreads helps you keep track of books you want to read.
Start by marking “Practical TLA+: Planning Driven Development” as Want to Read:
Practical TLA+: Planning Driven Development
Enlarge cover
Rate this book
Clear rating
Open Preview

Practical TLA+: Planning Driven Development

4.20  ·  Rating details ·  20 ratings  ·  7 reviews
Learn how to design complex, correct programs and fix problems before writing a single line of code. This book is a practical, comprehensive resource on TLA+ programming with rich, complex examples. Practical TLA+ shows you how to use TLA+ to specify a complex system and test the design itself for bugs.

You’ll learn how even a short TLA+ spec can find critical bugs. Start
...more
Kindle Edition, 248 pages
Published October 11th 2018 by Apress
More Details... Edit Details

Friend Reviews

To see what your friends thought of this book, please sign up.

Reader Q&A

To ask other readers questions about Practical TLA+, please sign up.

Be the first to ask a question about Practical TLA+

This book is not yet featured on Listopia. Add this book to your favorite list »

Community Reviews

Showing 1-49
Average rating 4.20  · 
Rating details
 ·  20 ratings  ·  7 reviews


More filters
 | 
Sort order
Start your review of Practical TLA+: Planning Driven Development
Rafael
Oct 29, 2018 rated it it was amazing
As far as I know, this is the first book covering in depth the algorithm language PlusCal (formerly called +CAL). PlusCal is meant to replace pseudo-code for writing high-level descriptions of algorithms. An algorithm written in PlusCal is translated into a TLA+ specification that can be checked with the TLC model checker.

Frederick P. Brooks already reflected on formal methods in his very well known essay "No Silver Bullet: Essence and Accident in Software Engineering":

"Much of the effort in
...more
Bugzmanov
Oct 07, 2019 rated it really liked it
Shelves: 2019
I'm a big fan of Hillel's blog and his presentations and I had high expectations for this book. And it's a good book, it lays out pluscal syntax foundations and does a good job of showing that the modeling technique is applicable in multiple vastly different scenarios: validating invariants of data structures, checking temporal properties for concurrent code, looking for gaps in business requirements, etc.

However, I was expecting some kind of revelation, like the one you get from learning about
...more
John
Nov 06, 2018 rated it it was amazing
I found this book to be an excellent guide to the world of "using a tool to help you think good about software design." A few points:
- it's not just for doing fancy distributed systems, you can also use it to help reason about complex product requirements
- since it's a tool for reasoning about systems in general, you don't even need to limit yourself to software!
- the first half is a little bit dry so I quit after that. Don't do this, I went back to it and the second half is so worth it - lots
...more
Xavier Shay
Mar 20, 2019 rated it it was amazing
Does what it says on the tin. I didn't know anything about TLA+ beforehand, save the name and that enabled formal verification maybe? Didn't see how it could be useful to my day to day. Now I do! Particularly liked the final two chapters, walking through designing a library system and map reduce, including dead ends. Already see places where I want to start using these techniques.
Stephen Adams
Jul 16, 2019 rated it really liked it  ·  review of another edition
A really good introduction to TLA+ and PlusCal. The author is able to set out the basics of using the toolbox and modelling systems clearly and succinctly.

I wish the author had expanded more on when he felt it was necessary to use TLA vs PlusCal. A second edition of the book could also benefit from some concrete examples of TLA+'s use in industry.

Overall though it is a very good introduction to TLA+ and the mindset that you must approach formal software specification.
Parnell
Apr 27, 2019 rated it really liked it  ·  review of another edition
I was convinced I needed to learn TLA+ after:

1. Reading Hillel's blog post explaining the differences between formal specification and formal verification; and,
2. Encountering an unfortunate series of system design misses and mistakes in a couple of work projects (where we use Haskell too, a good type system won't save you from sloppy designs!!)

After two-ish weeks of part-time reading effort I was comfortable enough with PlusCal and the tools to try writing a very rough and high-level
...more
Eduardo
Nov 17, 2018 rated it it was amazing
This is a very gentle introduction to the formalism of Leslie Lamport's TLA+ specification language. It serves as a nice first step before Specifying Systems. I also enjoyed the focus on PlusCal, which looks a lot less alien to most software engineers.
Steven
rated it it was amazing
Nov 10, 2018
Victor Grigoriu
rated it liked it
Feb 01, 2019
Steven
rated it it was amazing
Nov 27, 2018
Lorin Hochstein
rated it it was amazing
Dec 23, 2018
Michael Terry
rated it liked it
Feb 07, 2019
superfunc
rated it really liked it
Sep 07, 2019
San
rated it liked it
Jul 08, 2019
Bogdan-Ciprian Rusu
rated it really liked it
Oct 17, 2019
Andrew Helwer
rated it it was amazing
Jan 11, 2019
Piotr
rated it really liked it
Sep 17, 2019
Freddy Potargent
rated it it was amazing
Nov 24, 2018
Ruben
rated it really liked it
Nov 10, 2018
Kadri J
rated it it was ok
Dec 29, 2018
Alfredo Motta
marked it as to-read
Aug 01, 2018
Sophie Smithburg
marked it as to-read
Aug 23, 2018
Emre Sevinç
marked it as to-read
Sep 25, 2018
Hares Faiez
marked it as to-read
Oct 18, 2018
Eric
is currently reading it
Oct 21, 2018
Dmitry
marked it as to-read
Oct 21, 2018
Igor Bondarenko
marked it as to-read
Oct 27, 2018
Martijn Faassen
marked it as to-read
Oct 27, 2018
Gunar
marked it as to-read
Nov 04, 2018
Zach
marked it as to-read
Nov 14, 2018
Colin Jones
marked it as to-read
Nov 30, 2018
Babak
marked it as to-read
Dec 05, 2018
Vladimir Dorokhov
marked it as to-read
Dec 05, 2018
Nokie Rae
marked it as to-read
Dec 05, 2018
Santosh
marked it as to-read
Dec 06, 2018
James
marked it as to-read
Dec 11, 2018
Miles Gould
marked it as to-read
Dec 12, 2018
Alena Varkockova
marked it as to-read
Dec 13, 2018
Brian
added it
Dec 15, 2018
Shawn Moore
marked it as to-read
Dec 15, 2018
MikeG
marked it as to-read
Dec 24, 2018
Jon Bennett
marked it as to-read
Dec 24, 2018
Sylvain
marked it as to-read
Dec 26, 2018
Betsy-the-muffin
marked it as to-read
Jan 02, 2019
Derek Argueta
is currently reading it
Jan 19, 2019
Xabier
is currently reading it
Jan 21, 2019
Mark
marked it as to-read
Jan 26, 2019
Winar
marked it as to-read
Jan 27, 2019
There are no discussion topics on this book yet. Be the first to start one »

Readers also enjoyed

  • Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers
  • Enterprise Integration Patterns: Designing, Building, and Deploying Messaging Solutions
  • Super Pumped: The Battle for Uber
  • Finding Success (and Failure) in Haskell
  • Life in Code: A Personal History of Technology
  • 暗殺教室 2 [Ansatsu Kyoushitsu 2] (Assassination Classroom, #2)
  • 暗殺教室 4 [Ansatsu Kyoushitsu 4] (Assassination Classroom, #4)
  • 暗殺教室 3 [Ansatsu Kyoushitsu 3] (Assassination Classroom, #3)
  • 暗殺教室 9 [Ansatsu Kyoushitsu 9] (Assassination Classroom, #9)
  • 暗殺教室 10 [Ansatsu Kyoushitsu 10] (Assassination Classroom, #10)
  • 暗殺教室 7 [Ansatsu Kyoushitsu 7] (Assassination Classroom, #7)
  • 暗殺教室 11 [Ansatsu Kyoushitsu 11] (Assassination Classroom, #11)
  • 暗殺教室 5 [Ansatsu Kyoushitsu 5] (Assassination Classroom, #5)
  • 暗殺教室 6 [Ansatsu Kyoushitsu 6] (Assassination Classroom, #6)
  • 暗殺教室 8 [Ansatsu Kyoushitsu 8] (Assassination Classroom, #8)
  • 暗殺教室 15 [Ansatsu Kyoushitsu 15] (Assassination Classroom, #15)
  • 暗殺教室 13 [Ansatsu Kyoushitsu 13] (Assassination Classroom, #13)
  • 暗殺教室 17 [Ansatsu Kyoushitsu 17] (Assassination Classroom, #17)
See similar books…

Goodreads is hiring!

If you like books and love to build cool products, we may be looking for you.
Learn more »