Practical TLA+ pp 149-166 | Cite as

Business Logic

  • Hillel Wayne


We use TLA+ to find flaws in our designs. But there’s another, subtler benefit: we also find places where the spec is ambiguous. Formally specifying your problem forces you to decide what you actually want out of your system. This is especially important when we model “business logic,” features, and requirements. To work through this, we’ll use TLA+ to spec a simple library system and show how the act of specifying can itself find faults in the spec.

Copyright information

© Hillel Wayne 2018

Authors and Affiliations

  • Hillel Wayne
    • 1
  1. 1.ChicagoUSA

Personalised recommendations