Abstract
Specifications are more expressive than code. This comes at a cost: it’s not always clear how to go from a specification to reality. A technique for handling this is to write a very abstract spec and expand it into a more detailed, lower-level “implementation” that is closer to the program you’ll be writing. One very common pattern for doing this is to use a state machine. In this chapter, we will learn how to represent them and use them in writing our specifications.
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). State Machines. In: Practical TLA+. Apress, Berkeley, CA. https://doi.org/10.1007/978-1-4842-3829-5_9
Download citation
DOI: https://doi.org/10.1007/978-1-4842-3829-5_9
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