Bring your work with you to class on the 18th, so that we can review
it on the board.
1. Assume that this function is already proved to satisfy its specification.
(The checker will prove the correctness of succ on its own.)
Write the proof that the function is called correctly:
# Q1.py
def succ(x) :
"""{ pre x > 1
post y > x
return y
}"""
y = x + x
return y
a = readInt()
assert a > 0
# PROVE HERE that a + 1 > 1
b = succ(a + 1)
# PROVE HERE that b > a and a > 0
2. Write the missing code and its correctness proof for this specification:
# Q2.py
def max(x, y, z) :
"""{ pre True
post (ans >= x and ans >= y) and ans >= z
return ans
}"""
# ... INSERT CODE AND PROOF HERE ...
# PROVE HERE that (ans >= x and ans >= y) and ans >= z
return ans
3.
Prove that this function meets its
postcondition and preserves the global invariants.
Then, prove that the subsequent call is legal and leads to
the final correctness property:
# Q3.py
time = 88
"""{ 1. time == 88 premise
2. time > 0 algebra 1
}"""
# Now, we assert the global invariant on time:
"""{ globalinv time > 0 }"""
# And for bonus:
bonus = 2
"""{ globalinv bonus > 0 }"""
def tick(howmany) :
"""{ pre howmany > 0
post ans > 0 and ans + howmany == time - bonus
return ans
}"""
global time, bonus
ans = time
time = time + (howmany + bonus)
# PROVE: (ans > 0 and ans + howmany == time - bonus) and (time > 0 and bonus > 0)
return ans
# Now, we can call the function:
oldtime = tick(2)
# PROVE HERE that time > oldtime
4. Here is a module that models the movement of an object along a
diagonal. Prove the module's data-structure invariant
and the correctness of its move method:
# Q4.py
### module SpritePosition maintains the position of a sprite on a grid.
range = readInt() # the total range of movement of the sprite on the grid
assert range > 99
xpos = 80 # the x-position of the sprite on the grid
ypos = range - 80 # the y-position of the sprite on the grid
# PROVE HERE that xpos + ypos == range and also xpos > 0
"""{ globalinv xpos + ypos == range
globalinv xpos > 0 }"""
# The checker will automatically verify the postconditions and invariants for these
# two methods, because they are so simple:
def getX() :
"""{ pre True
post ans == xpos
return ans
}"""
global xpos, ypos, range
ans = xpos
return ans
def getY() :
"""{ pre True
post ans == ypos
return ans
}"""
global ypos, ypos, range
ans = ypos
return ans
# You must prove this one:
def move(increment) :
"""{ pre increment < xpos and increment > 0
post ypos > ypos_in # note: as the Lecture notes explained,
# ypos_in is the value of ypos when
# the function was entered.
}"""
global xpos, ypos
xpos = xpos - increment
ypos = ypos + increment
# REPROVE HERE the two globalinvs and PROVE the postcondition
5. Finish the correctness proof of this recursively defined function:
# Q5.py
# exp(n) defines exponentiation of 2, e.g., exp(3) == 2^3 == 2 * 2 * 2 == 8
"""{ def exp(0) == 1
def exp(n) == exp(n-1) * 2 }"""
def pow(n) : # computes 2^n
"""{ pre n >= 0
post ans == exp(n)
return ans }"""
if n == 0 :
ans = 1
# PROVE HERE that ans == exp(n)
else :
ans = pow(n-1)
ans = ans + ans
# PROVE HERE that ans == exp(n)
return ans