TLA from first principles

I'm working on v0.5 of Logic for Programmers. In the process of revising the "System Modeling" chapter, I stumbled on a great way to explain the temporal logic of actions that TLA+ is based on. I'm reproducing that bit here with some changes to fit the newsletter format.

Note that by this point the reader has already encountered property testing, formal verification, decision tables, and nontemporal specifications, and should already have a lot of practice expressing things as predicates.

We have some bank users, each with an account balance. Bank users can wire money to each other. We have overdraft protection, so wires cannot reduce an account value below zero.

For the purposes of introducing the ideas, we'll assume an extremely simple system: two hardcoded variables alice and bob, both start with 10 dollars, and transfers are only from Alice to Bob. Also, the transfer is totally atomic: we check for adequate funds, withdraw, and deposit all in a single moment of time. Later [in the chapter] we'll allow for multiple nonatomic transfers at the same time.

In programming, we'd think of alice and bob as variables that change. How do we represent those variables purely in terms of predicate logic? One way is to instead think of them as arrays of values. alice[0] is the initial state of alice, alice[1] is after the first time step, etc. Time, then, is "just" the set of natural numbers.

Leave a Comment