# Z Notation

The Z notation is a formal specification language used for describing and modelling computing systems. It is targeted at the clear specification of computer programs and computer-based systems in general. Developed at Oxford University.

### Z Notation for Set Comprehension

For set comprehension, for we have the notation

• = term in Predicate Logic, i.e., an expression using variables and functions that returns a value.
• lists the variables used in and their types, can be omitted if we are doing Untyped Predicate Logic
• = any wff formula in predicate logic with the variables used in as free variables in the formula

can be written as which can be shortened to .

is the set

### States

In Z, we think of the execution of a system as a sequence of states (trace) where each state is a mapping from variables (state elements) to values.

We specify the behaviour of the system by describing in logic what are valid steps of the system.

### Z Specification

In a Z system specification, we describe:

1. Generic and free types for 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): the system elements, their types and Invariants about relationships between the system elements.
4. Initial state (optional).
5. Operations and how these change the elements of the system
1. Use NameOfSchema, which is equivalent to writing
• NameOfSchema
• NameOfSchema’

### Schema Inclusion

We use the schema inclusion to define the initial system state.

### Input and Output

In Z, we use the following notation for inputs and outputs:

• “?” as in p? means p? is an input
• “!” as in q! means q! is an output

### Local Variable

We can use a local variable, such as in the example below

### Exceptions

I will probably need to add this in the exam.

Notice that for the errors, we don’t use a Schema. Rather we use a “zai” schema to represent the fact that operations on state variables do not change the state.

• You could also just use a standard Schema and just specify that all the states don’t change, but this is much quicker
• You output error! : Errors

### Working with Relations

If the tuple is part of a TOTAL function (you CANNOT do this if it is a non-total function):

• Use to get the 2nd element associated with

Else (for relation/non-total function)

• Use to get the SET of possible second elements associated with a 1st element
• Extract an arbitrary element using
1. Use or to get the SET of possible 1st elements associated with a 2nd element

### In Practice

So what I see is that there are a few steps

1. List Out Constants as a Schema
1. List out State Space Schema
1. List out initial State as a Schema