Practical TLA+: Planning Driven Development

© Hillel Wayne 2018

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

8. Data Structures

Hillel Wayne¹ 

(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 ...