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 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