Records

Records are like structs or objects — they group named fields together.

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.