Practical TLA+ pp 127-136 | Cite as

Data Structures

  • Hillel Wayne


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.

Copyright information

© Hillel Wayne 2018

Authors and Affiliations

  • Hillel Wayne
    • 1
  1. 1.ChicagoUSA

Personalised recommendations