Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Author information
Authors and Affiliations
Rights and permissions
Copyright information
© 2018 Hillel Wayne
About this chapter
Cite this chapter
Wayne, H. (2018). Algorithms. In: Practical TLA+. Apress, Berkeley, CA. https://doi.org/10.1007/978-1-4842-3829-5_7
Download citation
DOI: https://doi.org/10.1007/978-1-4842-3829-5_7
Published:
Publisher Name: Apress, Berkeley, CA
Print ISBN: 978-1-4842-3828-8
Online ISBN: 978-1-4842-3829-5
eBook Packages: Professional and Applied ComputingProfessional and Applied Computing (R0)Apress Access Books