Abstract
When we want to write a specification involving some data structure, we need some sort of definition of the data structure. Further, we need one that’s independent of the algorithm. That means we should write data structures as separate modules that are extended or instantiated in our spec. We’ll use the example of linked lists (LL), in a file we’ll call LinkedLists.tla.
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). Data Structures. In: Practical TLA+. Apress, Berkeley, CA. https://doi.org/10.1007/978-1-4842-3829-5_8
Download citation
DOI: https://doi.org/10.1007/978-1-4842-3829-5_8
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