Idiomatic TLA+

For example multiple assignments in Python:

x = y = z = 'foo'

or formatting strings:

def user_info(user):
  return 'Name: {user.name} Age: {user.age}'.format(user=user)

or swap values:

b, a = a, b

or even conditional expression in C. The C language has a ternary expression (using the two operators ? and :) and corresponding C idiom is:

b = a == 4 ? 5 : a - 1;

TLA+ has it’s own idioms and Leslie Lamport described some of them in his great book “Specifying Systems” (Chapter 7. Writing a specification. Some advice.).

The benefits of being familiar with idioms, particularly the larger ones, is that when looking at code you can see several lines of code but because it is familiar as a particular idiom you can mentally represent and think about the code as that single idiom instead of having to necessarily read and comprehend each line individually.

In turn authors of Apalache collect specification idioms that aid them in writing TLA+ specifications. These idioms are quite likely different from the original ideas of Leslie Lamport (the author of TLA+). Apalache documentation describes more TLA+ idioms and I like them a lot.

Let me list all of them here:

  1. Keep state variables to the minimum
  2. Update state variables with assignments
  3. Apply primes only to state variables
  4. Isolate updates to VARIABLES
  5. Isolate non-determinism in actions
  6. Introduce pure operators
  7. Introduce a naming convention for operator parameters
  8. Use Boolean operators in actions, not IF-THEN-ELSE
  9. CHOOSE smart, prefer \E
  10. Do not over-structure
  11. Do not over-modularize
  12. Separate normal paths from error paths
  13. Do you really need those nice recursive operators?
  14. Do you really need set cardinalities?
  15. Do you really need integers?
Теги: softwaretlafeeden