Abstract
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.
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). Business Logic. In: Practical TLA+. Apress, Berkeley, CA. https://doi.org/10.1007/978-1-4842-3829-5_10
Download citation
DOI: https://doi.org/10.1007/978-1-4842-3829-5_10
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