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?

• 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