© Hillel Wayne 2018
Hillel WaynePractical TLA+https://doi.org/10.1007/978-1-4842-3829-5_8

8. Data Structures

Hillel Wayne1 
(1)
Chicago, Illinois, USA
 

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.

Warning

If you’re making a new specification for this, do not make LinkedLists.tla the root file. Instead, make the root file something else, such as main.tla, and add LinkedLists.tla as a secondary module. This will make it easier to ...

Get Practical TLA+: Planning Driven Development now with the O’Reilly learning platform.

O’Reilly members experience books, live events, courses curated by job role, and more from O’Reilly and nearly 200 top publishers.