Formal specs as sets of behaviors

The most developed one I know of is Atelier B [0], which uses the B-Method and has a C code generator. I believe this was the tool used to develop several driverless train control systems in the Paris Metro and other subways.

There is a free version but unfortunately it is not open source.

[0] https://www.atelierb.eu/en/

> I was just contrasting the way TFA explained specifications as being definitions of groups of acceptable execution traces (perhaps checked using a model checker) with Dijkstra’s approach of characterizing the acceptable behavior without simulating any executions.

I think that's a misunderstanding, as TLA+ doesn't require simulating anything (even the model checker doesn't work like that; it can check a formula that corresponds to an uncountable infinity of behaviours, each of them infinite, in a second [1]), and Dijkstra's approach is separate from the logical semantics.

It is true that a TLA formula denotes a set (really, a class) of something called "behaviours" (which could be interpreted as execution traces when a formula is interpreted to describe a program) just as the statement x > 3 denotes the set of all integers greater than 3 (in a logic over the integers), but in neither case is enumerating or "simulating" anything required, either in principle or in practice. It's just simple logical semantics, and Dijkstra's approach is easily expressed in a logic with such simple semantics.

In fact, TLA serves as a generalisation of Dijkstra's approach, as that is lacking when dealing with concurrency. While in sequential programs it is easy to specify invariants as pre/post conditions, it is hard to do that in concurrent/distributed programs.

[1]: You can ask the TLC model checker to simulate behaviours if you want (it can be useful sometimes), but checking mode, not simulation mode, is the default. Obviously, in simulation mode TLC doesn't work as a model checker. Technically speaking, every TLA formula denotes an uncountable infinity of behaviours of infinite lengths, where between any two states in the behaviour there is an infinite number of steps (it is in this regard that TLA is different from other temporal logics like LTL), and each state in every behaviour is an assignment to an infinite number of variables (in fact, that uncountable infinity is so large that it doesn't even correspond to a set in the set theory sense but to something called a class). The large infinities are what makes TLA so suitable for expressing abstractions and refinement and interactions between components.

This may sound strange, but it's actually how most simple logics work. When I said before that `x > 3` in a logic over the integers denotes the set of integers greater than 3, I wasn't entirely precise. What it really denotes is: "x is in the set of integers greater than three and any other imaginable variable could be any integer".

> TLA+ doesn't require simulating anything

I was referring to way the Python REPL examples/tree diagrams and sections on execution histories were used to explain things in the article, not to TLA+. I was contrasting how the author explained specifications versus how someone like Dijkstra would, not anything about TLA+. I don’t know enough about TLA+ to say anything interesting, but I appreciate your explanations of its approach!

TLA+ was specifically designed for practitioners (https://lamport.azurewebsites.net/tla/book.html), although he did use earlier incarnations of TLA to analyse his own concurrent and distributed algorithms.

His paper explaining TLA [1] says:

> We are motivated not by an abstract ideal of elegance, but by the practical problem of reasoning about real algorithms. Rigorous reasoning is the only way to avoid subtle errors in concurrent algorithms, and we want to make reasoning as simple as possible by making the underlying formalism simple.

The introduction to the book says:

> TLA provides a mathematical foundation for describing systems. To write specifications, we need a complete language built atop that foundation. I ini- tially thought that this language should be some sort of abstract programming language whose semantics would be based on TLA. I didn’t know what kind of programming language constructs would be best, so I decided to start writing specifications directly in TLA. I intended to introduce programming constructs as I needed them. To my surprise, I discovered that I didn’t need them. What I needed was a robust language for writing mathematics.

> Although mathematicians have developed the science of writing formulas, they haven’t turned that science into an engineering discipline. ... The specification of a real system can be dozens or even hundreds of pages long. Mathematicians know how to write 20-line formulas, not 20-page formulas. So, I had to introduce notations for writing long formulas. What I took from programming languages were ideas for modularizing large specifications.

And the Getting Started portion says:

> A system specification consists of a lot of ordinary mathematics glued together with a tiny bit of temporal logic. That’s why most TLA+ constructs are for expressing ordinary mathematics. To write specifications, you have to be familiar with this ordinary math. Unfortunately, the computer science departments in many universities apparently believe that fluency in C++ is more important than a sound education in elementary mathematics. So, some readers may be unfamiliar with the math needed to write specifications. Fortunately, this math is quite simple. If exposure to C++ hasn’t destroyed your ability to think logically, you should have no trouble filling any gaps in your mathematics education.

He recognises the tradeoffs of abandoning the programming style, but it is done to make the language simple and practitioner-friendly (and it is a much simpler language than Python, let alone any other specification language, all while preserving maximal expressive power). You can have an opinion on whether this is a good tradeoff or not, but it was done intentionally, and with the purpose of helping practitioners.

[1]: https://lamport.azurewebsites.net/pubs/lamport-actions.pdf

Thanks. Tangentially TLA+ seems to be most useful for finding concurrency bugs. I'm yet to find a compelling example of it used for a fairly mundane, by that I mean composed of mainly sequential processes, systems architecture.