Buy new:
-29% $31.76
FREE delivery Monday, July 22 on orders shipped by Amazon over $35
Ships from: Amazon.com
Sold by: Amazon.com
$31.76 with 29 percent savings
List Price: $44.99

The List Price is the suggested retail price of a new product as provided by a manufacturer, supplier, or seller. Except for books, Amazon will display a List Price if the product was purchased by customers on Amazon or offered by other retailers at or above the List Price in at least the past 90 days. List prices may not necessarily reflect the product's prevailing market price.
Learn more
Get Fast, Free Shipping with Amazon Prime FREE Returns
FREE delivery Monday, July 22 on orders shipped by Amazon over $35. Order within 14 hrs 49 mins
In Stock
$$31.76 () Includes selected options. Includes initial monthly payment and selected options. Details
Price
Subtotal
$$31.76
Subtotal
Initial payment breakdown
Shipping cost, delivery date, and order total (including tax) shown at checkout.
Ships from
Amazon.com
Ships from
Amazon.com
Sold by
Amazon.com
Sold by
Amazon.com
Returns
Eligible for Return, Refund or Replacement within 30 days of receipt
Eligible for Return, Refund or Replacement within 30 days of receipt
This item can be returned in its original condition for a full refund or replacement within 30 days of receipt.
Read full return policy
Returns
Eligible for Return, Refund or Replacement within 30 days of receipt
This item can be returned in its original condition for a full refund or replacement within 30 days of receipt.
Read full return policy
Payment
Secure transaction
Your transaction is secure
We work hard to protect your security and privacy. Our payment security system encrypts your information during transmission. We don’t share your credit card details with third-party sellers, and we don’t sell your information to others. Learn more
Payment
Secure transaction
We work hard to protect your security and privacy. Our payment security system encrypts your information during transmission. We don’t share your credit card details with third-party sellers, and we don’t sell your information to others. Learn more
$25.95
Get Fast, Free Shipping with Amazon Prime FREE Returns
Pages have no markings, no highlighting, underlinging or margin notes. Cover has light wear at edges and corners. Binding is tight. Shipped directly from Amazon. Pages have no markings, no highlighting, underlinging or margin notes. Cover has light wear at edges and corners. Binding is tight. Shipped directly from Amazon. See less
FREE delivery Wednesday, July 24 on orders shipped by Amazon over $35
Or fastest delivery Tuesday, July 23. Order within 2 hrs 4 mins
Only 1 left in stock - order soon.
$$31.76 () Includes selected options. Includes initial monthly payment and selected options. Details
Price
Subtotal
$$31.76
Subtotal
Initial payment breakdown
Shipping cost, delivery date, and order total (including tax) shown at checkout.
Access codes and supplements are not guaranteed with used items.
Kindle app logo image

Download the free Kindle app and start reading Kindle books instantly on your smartphone, tablet, or computer - no Kindle device required.

Read instantly on your browser with Kindle for Web.

Using your mobile phone camera - scan the code below and download the Kindle app.

QR code to download the Kindle App

Practical TLA+: Planning Driven Development 1st ed. Edition

by Hillel Wayne (Author)
4.7 4.7 out of 5 stars 47 ratings
See all formats and editions
{"desktop_buybox_group_1":[{"displayPrice":"$31.76","priceAmount":31.76,"currencySymbol":"$","integerValue":"31","decimalSeparator":".","fractionalValue":"76","symbolPosition":"left","hasSpace":false,"showFractionalPartIfEmpty":true,"offerListingId":"RvZPBjb601ymi9gNuiCfr6jIs92dbORbLBwGvxUryKA0pZd0UdHWE6rNWegUE%2FnExbkitk5LRvgUOaLKsyCVM0DlBJ4K02vxY%2B5mooy%2BES6lr%2B0HJToab6OaOH8M56LM4q%2BcMO%2FS%2BOB2WyqR4SxcQg%3D%3D","locale":"en-US","buyingOptionType":"NEW","aapiBuyingOptionIndex":0}, {"displayPrice":"$25.95","priceAmount":25.95,"currencySymbol":"$","integerValue":"25","decimalSeparator":".","fractionalValue":"95","symbolPosition":"left","hasSpace":false,"showFractionalPartIfEmpty":true,"offerListingId":"RvZPBjb601ymi9gNuiCfr6jIs92dbORbQN5%2B8y%2Fnl7g6Fb0ENa6I7j1UH65j50pNrNTg7lBEXUsivv9ywQ9jXv9Y9yZHgnpWtVwdzn2%2FQHXiZwcQ4vjMIZSuvzT%2FEdr0a%2By%2FxrJahUDYBhHTBY82wKUCSlQQjhPJQR%2Bbmu8ICK81SrRIy4Zdc53RyFnGCjN9","locale":"en-US","buyingOptionType":"USED","aapiBuyingOptionIndex":1}]}

Purchase options and add-ons

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 by getting your feet wet with an example of TLA+ used in a bank transfer system, to see how it helps you design, test, and build a better application. Then, get some fundamentals of TLA+ operators, logic, functions, PlusCal, models, and concurrency. Along the way you will discover how to organize your blueprints and how to specify distributed systems and eventual consistency.

Finally, you’ll put what you learn into practice with some working case study applications, applying TLA+ to a wide variety of practical problems: from algorithm performance and data structures to business code and MapReduce. After reading and using this book, you'll have what you need to get started with TLA+ and how to use it in your mission-critical applications.
What You'll Learn
  • Read and write TLA+ specs
  • Check specs for broken invariants, race conditions, and liveness bugs
  • Design concurrency and distributed systems
  • Learn how TLA+ can help you with your day-to-day production work

Who This Book Is For
Those with programming experience who are new to design and to TLA+.
Previous slide of product details
  1. ISBN-10
    1484238281
  2. ISBN-13
    978-1484238288
  3. Edition
    1st ed.
  4. Publisher
    Apress
  5. Publication date
    October 12, 2018
  6. Language
    English
  7. Dimensions
    7.01 x 0.56 x 10 inches
  8. Print length
    244 pages
  9. See all details
Next slide of product details
Amazon First Reads | Editors' picks at exclusive prices

Frequently bought together

Practical TLA+: Planning Driven Development
$31.76
Get it as soon as Monday, Jul 22
In Stock
Ships from and sold by Amazon.com.
+
Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers
$35.99
Get it as soon as Monday, Jul 22
In Stock
Ships from and sold by Amazon.com.
+
Software Abstractions, revised edition: Logic, Language, and Analysis (Mit Press)
$35.05
Get it as soon as Monday, Jul 22
In Stock
Ships from and sold by Amazon.com.
Total price:
To see our price, add these items to your cart.
Details
Added to Cart
spCSRF_Control
Choose items to buy together.

Editorial Reviews

From the Back Cover

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 by getting your feet wet with an example of TLA+ used in a bank transfer system, to see how it helps you design, test, and build a better application. Then, get some fundamentals of TLA+ operators, logic, functions, PlusCal, models, and concurrency. Along the way you will discover how to organize your blueprints and how to specify distributed systems and eventual consistency.

Finally, you’ll put what you learn into practice with some working case study applications, applying TLA+ to a wide variety of practical problems:from algorithm performance and data structures to business code and MapReduce. After reading and using this book, you'll have what you need to get started with TLA+ and how to use it in your mission-critical applications.
You will:
  • Read and write TLA+ specifications
  • Check specs for broken invariants, race conditions, and liveness bugs
  • Design concurrency and distributed systems
  • Learn how TLA+ can help you with your day-to-day production work

About the Author

Hillel Wayne is a software consultant who specializes in formal methods and specification. He also writes on empirical engineering, software history, and education. In his free time, he juggles and makes chocolate. He lives in Chicago. You can find his other work at hillelwayne.com or on Twitter at @hillelogram.

Product details

  • Publisher ‏ : ‎ Apress; 1st ed. edition (October 12, 2018)
  • Language ‏ : ‎ English
  • Paperback ‏ : ‎ 244 pages
  • ISBN-10 ‏ : ‎ 1484238281
  • ISBN-13 ‏ : ‎ 978-1484238288
  • Item Weight ‏ : ‎ 15.5 ounces
  • Dimensions ‏ : ‎ 7.01 x 0.56 x 10 inches
  • Customer Reviews:
    4.7 4.7 out of 5 stars 47 ratings

Customer reviews

4.7 out of 5 stars
4.7 out of 5
47 global ratings

Top reviews from the United States

R. Hettinger
5.0 out of 5 stars Great examples
Reviewed in the United States on February 7, 2019
Verified Purchase
The author does a great job creating small examples of specifications that seem completely plausible but that have bugs immediately detectable by the TLC model checker.

Do note that the title is a misnomer. The book focuses on PlusCal rather than core TLA⁺. (Pluscal is a programmer friendly language that compiles into TLA⁺). If you want to know more about TLA⁺ after reading this book, it is worthwhile to view the training videos on the TLA⁺ homepage.

If you do purchase this book, check-out the errata on the authors github page (the errors are mostly minor). It is also informative to look at Leslie Lamport's commentary on the book: https://lamport.azurewebsites.net/tla/practical-tla.html .

The author, Hillel Wayne, has an excellent style and is an experienced instructor. I hope that he writes a follow-on book that delves deeper into TLA⁺, explores more advanced examples, and demonstrates the TLAPS proof assistant.
18 people found this helpful
Helpful
 Report
Thomas
5.0 out of 5 stars Great intro to TLA+
Reviewed in the United States on September 22, 2019
Verified Purchase
It introduces you to a language called PlusCal which transpiles to TLA+.
When I purchased this book, I didn't realize that but for practical purposes it doesn't matter since I'm still able to write specifications in PlusCal and have TLA+ check them.
I enjoyed that the examples showed the thought process that the author took to check the specifications.

One thing I would like to have seen is more exercises that tested your knowledge after each chapter.
3 people found this helpful
Helpful
 Report
James Koppel
4.0 out of 5 stars Turns TLA+ into ordinary programming --- for good and ill
Reviewed in the United States on June 23, 2019
In a lot of ways, I'm not a typical reader of this book. I've spent a good chunk of my career doing things related to formal verification, and took my first model checking course when I was 18.

Also, because I'm friends with Hillel Wayne, and had him on instant messenger the whole time . He gave me a free copy to review, and told me to be extra harsh.

I've posted a long review on my blog. Amazon does not allow links in reviews, but you can find it by search for the blog's name, "Path Sensitive." Below is a summary of my review. Also, Hillel wants me to tell you that my actual rating is 3.5/5, rounded up for Amazon's purposes.

Practical TLA+ is the first of its kind: a practical programming book about formal verification. It is still a rough book. Whenever a snippet of code repeats, the changes are supposed to be marked in bold, yet I’d often find the bolding missing. He once introduced a piece of syntax, and then didn’t use it till 100 pages later. In a lot of ways, the TLA+ syntax makes no sense; as a result, I got completely stuck in the first chapter, and had to ask Hillel to bail me out. The book can teach you TLA+, but if you're just dabbling, consider waiting for the second edition.

For the programmer looking for mind expansion but not code verification, I don’t think this book has much to offer. The benefit of cross-training comes from seeing ideas that are a subtle part of one discipline become a blatant part of another. Just as it’s easier to understand harmony by playing piano than by singing in a choir, new paradigms are valuable when they take concepts that are implicit in software design and give them syntax and compiler errors. For TLA+, these concepts are: modeling, nondeterminism, and temporal correctness properties. However, Practical TLA+ gives you little practice writing correctness properties, and does its best to hide the most mind-expanding parts of modeling (refinement) and nondeterminism (guards) from the reader. It does what it set out to do: turn formal verification into ordinary programming.

But, nonetheless, I can say that I went through Practical TLA+ in an hour a day for 10 days, I had fun doing so, and — hey — now I know TLA+.
12 people found this helpful
Helpful
 Report
Anon
5.0 out of 5 stars Title is accurate
Reviewed in the United States on November 10, 2018
Verified Purchase
TLA+ has a well deserved reputation for difficult. This is the first book I know of that takes TLA+ and shows actual real world examples of its use in model and spec checking. If you have tried Lamport's book and gave up in frustration, start with this one. Many reasonable real world examples, worked out fully and completely.
10 people found this helpful
Helpful
 Report
Andrew Helwer
5.0 out of 5 stars Now I know PlusCal!
Reviewed in the United States on January 12, 2019
I previously had good working knowledge of TLA+ and had applied it some projects at work involving concurrency. This book served as an excellent introduction to PlusCal, which is a variant of TLA+ that addresses shortcomings with how the language handles communicating sequential processes. After working through this book, I am now proficient in PlusCal and am using it in a work project at this very moment! The author has a very approachable style, and I think this applications-focused book is well worth software engineers' time.
6 people found this helpful
Helpful
 Report

Top reviews from other countries

Jamie,Jamie
5.0 out of 5 stars Easy to follow content
Reviewed in the United Kingdom on March 16, 2020
Verified Purchase
All the examples that I tried worked and the concepts were simply explained. This book makes a very complex piece of software understandable
Report