Z Specification

In Z, we think of the execution of a system as a sequence of states (trace):

where each state is a mapping from variables to values.

In a Z system spec, we describe:

1. Types of data manipulated by the system (optional)
2. Constants (elements that aren't changed by the system) and their types (optional)
3. State space (set of possible states): system elements, their types, and invariants about relationships between system elements
4. Operations and how these change the elements of the system
   • System operations which change the system state or elements:
   • System operations which report the system state:

A schema is a way of grouping together related information

We can include one schema in another schema by listing its name in the signature part of another schema. This adds the signature and predicates from the included schema.

is equivalent to writing:

We wish to describe both the current and next values of a variable in the in the state.

We refer to the value of a variable in the next state by attaching a prime to the variable name, e.g .

If we include schema like , that is equivalent to:

A delta schema ( schema) describes an operation on a state of the system, and gives us access to both the current and next values of the system

is equivalent to writing:

An operation that increments the values of both state variables:

A xi schema ( schema) means there are no changes to the state. Every variable is automatically set to .

• ? as in means is an input
• ! as in means is an output

• Preconditions are conditions on the current state variables and inputs
• Postconditions are conditions on the next state variables and the outputs

Types of types:

1. Built-in types: , etc.
2. Generic types: types that exist without explicitly stating what the elements of the type are
   Generic types are also called uninterpreted types, because they don't have a standard interpretation and we don't care
   For example, or
3. Free (enumerated) types: a new type for which we describe its possible values
   For example,
   These values are assumed to be distinct
4. Compound Types

See Properties of Binary Relations#Uniqueness Properties

On top of the primary operations of a system, we also want to define exception handling operations for when preconditions are not met.

• Don't think "how" to build a set, think declaratively: "what" should the state element satisfy after it has been constructed. You aren't writing the program to do the work, just the spec
• Set comprehension is usually not the right answer

Create a Z specification of the game of musical chairs:

The game involves a collection of chairs and players. There is always one less chair than players. In each round the players walk around while music plays and when the music goes off, the players must immediately sit on a chair. The person who doesn’t get a chair is eliminated. The winner is the person who gets a chair in the round where there are only two players left.

Src: Nimal Nissanke, Formal Specification, Springer, 1999

solution
Generic types:

Operations

dom(occupied') = ch' means every chair has a person on it

Create a Z specification for the voting system for the Canadian federal House of Commons. Create operations for:

1. Add candidates for ridings. The candidate must reside in the riding and be Canadian and at least 18 years of age.
2. Register voters. Voters must be at least 18 years old, Canadian, and live in the riding. Ridings are determined by the voter’s postal code.
3. Voting. A voter must be registered and can only vote for a candidate in the riding where he or she resides. A voter can make at most one vote.
4. Determining the winner(s) for a riding.

Credit to Shahram Esmaeilsabzali for this example.

solution
Generic types:

Exceptions