TLA+

This post shows how to write your first simple TLA+ specification. What is a specification? In software, the behaviour of a system is described as a sequence of states. Mathematically, each state is expressed as a function F(t), which represents the state of a system at time t. To completely specify a system, we write out each state to fully define the systems behaviour. A simple clock This example comes from Chapter 2 of the book Specifying Systems by the creator of TLA+, Leslie Lamport....

At its most basic, TLA+ is a written description of what a system is supposed to do. More specifically, TLA+ is a specification language for formally defining the behavioural properties of a system. TLA+ is based on temporal logic, which is built on top of first-order logic and set theory, and provides some conveniences for working with large specifications for complex systems. You can think of a TLA+ specification as mostly ordinary math and logic, glued together with temporal logic for parts requiring it....

I’ve been helping define some concurrent algorithms and I’m struggling with a number of issues: concurrent algorithms are difficult to design, they are often difficult to implement, and, even after they are designed, are difficult to guarantee that they are correct. This lead me into some research on formal specifications for algorithms, and how they can help. Finally, I settled on TLA+ as a viable tool for just such a problem....