© 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 O’Reilly online learning.

O’Reilly members experience live online training, plus books, videos, and digital content from 200+ publishers.