# 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⟩⋅⟨signature⟩∣⟨wff⟩}$

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

${x∣x∈nat∧x≤6}$ can be written as ${x•x:nat∣x≤6}$ which can be shortened to ${x:nat∣x≤6}$.

${x+y•x,y:nat∣x≤2∧y≤1}$ is the set ${0,1,2,3}$

### States

In Z, we think of the execution of a system as a sequence of states (trace) $state_{0}→state_{1}→state_{2}→…$ 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:

- Generic and free types for data manipulated by the system (optional).
- Constants (elements that aren’t changed by the system) and their types (optional).
- State space (set of possible states): the system elements, their types and Invariants about relationships between the system elements.
- Initial state (optional).
- Operations and how these change the elements of the system
- Use $Δ$NameOfSchema, which is equivalent to writing
- NameOfSchema
- NameOfSchema’

- Use $Δ$NameOfSchema, which is equivalent to writing

### 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 $f$ (you CANNOT do this if it is a non-total function):

- Use $f(x)$ to get the 2nd element associated with $x$

Else (for relation/non-total function)

- Use $R(∣{x}∣)$ to get the SET of possible second elements associated with a 1st element $x$
- Extract an arbitrary element using $y∈R(∣{x}∣)$

- Use $dom(R▷{y})$ or $R_{∼}(∣{y}∣)$ to get the SET of possible 1st elements associated with a 2nd element $y$

### In Practice

So what I see is that there are a few steps

- Define your types

- List Out Constants as a Schema

- List out State Space Schema

- List out initial State as a Schema

- Add all of your operations
- This is where there are the key logics for your functions
- Don’t forget to add exceptions
- There should be exception handling schemas for every precondition that can be violated. These schemas can be combined when the same error message is appropriate for multiple exceptions