Records

Records are like structs or objects - they group named fields together. In TLA+, records are simply functions whose domain is a set of strings (the field names), but because this pattern occurs so frequently, TLA+ provides dedicated syntax for them.

Creating Records

[name |-> "Alice", age |-> 30]

Accessing Fields

Use dot notation:

person.name      \* "Alice"
person.age       \* 30

Record Types (Sets of Records)

[name: {"Alice", "Bob"}, age: 0..120]

This is the set of all records with a name field from the given set and an age field from 0..120. Useful for TypeOK invariants.

Updating Records (EXCEPT)

Just like functions, use EXCEPT:

person' = [person EXCEPT !.age = @ + 1]

Records Are Functions

Under the hood, a record is a function from field names (strings) to values:

[name |-> "Alice", age |-> 30]

is the same as:

[x \in {"name", "age"} |-> IF x = "name" THEN "Alice" ELSE 30]

Try It

The spec models a simple user account system with records.