## Lecture 2-1

# Elements of Z Notation

Bart Massey

# A Function In Python

```
def f(n):
t = 0
for i in range(n - 1, 0, -1):
t += i
return t
```

What does it do?

Is it right?

Is there a better way to write it?

# Python Done Better

```
# Return the number of pairs one can make
# from the given number of elements.
def pairs(elements):
pairs_found = 0
for i in range(elements - 1, 0, -1):
pairs_found += i
return pairs_found
```

Now we know what it does..or do we?

- What about negative elements?
- Will it work for really large elements?

Is it correct?

Is there a better way to write it?

# A Z Specification

```
| pairs : N -> N
|---------------
| forall n : N @ pairs n = sum 1..n
```

This looks a lot like our code, but...

It goes in the other order, and starts at 1

- It actually doesn't go in
*any*order - Omitting 0 from a sum doesn't change it

- It actually doesn't go in
It specifies that pairs works over non-negative numbers. We should add this to the comment

No summation variable

Works for arbitrarily large

`x`

# Better Z

```
| pairs : N -> N
|---------------
| forall n : N @ pairs n = n * (n - 1) div 2
```

Use

*Gauss's Sum*to get a closed form- Works because math
- Harder to prove Python matches Z
Can transform Python to match Z

`# Return the number of pairs one can make # from the given non-negative number of elements. def pairs(elements): assert elements >= 0 return elements * (elements - 1) // 2`

To prove: the

`div`

is really just a divide

# A State Machine That Can Kill Or Heal

See Jacky for description of radiation therapy machine and its states

We want to describe the state machine symbolically

- So that it can be checked for consistency and completeness
- So that we can prove other important properties
- So that we can try to turn it directly into code
- So that we can easily elaborate it with more behavior

Last modified: Monday, 11 January 2016, 2:22 AM