Practical TLA+ pp 113-126 | Cite as


  • Hillel Wayne


One of the benefits of TLA+ being a specification language is that operators can be far more expressive and powerful than program functions can be. This is also a drawback: if your spec uses a “too powerful” operator, you cannot directly translate it to code. Usually this is fine: if you’re specifying a large system, you probably aren’t worrying that your sort function is correct.

Copyright information

© Hillel Wayne 2018

Authors and Affiliations

  • Hillel Wayne
    • 1
  1. 1.ChicagoUSA

Personalised recommendations