Consider the following python function
that takes two integers and returns another.
def foo(x, y):
z = x + y
return z – 1
The return value formula is x + y – 1 . With this formula, we are able
to prove/disprove properties like “If both inputs are positive, the return
value is also positive.”
In this assignment, we will write a python program that automatically
derives the return value formula. For simplicity, we will only consider pure
python functions that
Take two integers x and y , and return one integer.
Do not have function calls, imports, loops, or exceptions.
Only have integer local variables.
Examples:
Input 1
def foo(x, y):
return x * 2
Output 1: x * 2 (or x + x , etc.)
Input 2:
def foo(x, y):
x += y
return x + y
Output 2: x + 2 * y (or x + y + y , etc.)
Input 3:
def foo(x, y):
z = x – y
x -= y
z *= x
return z + 1
Output 3: (x – y) ^ 2 + 1 (or any other equivalent form)
We will use Z3 to handle formulas. Example usage:
>>> import z3
>>> x = z3.Int(‘x’)
>>> y = z3.Int(‘y’)
>>> z = x – y
>>> x -= y
>>> z *= x
>>> z + 1
(x – y)*(x – y) + 1
>>>
Please search for the documentation to get familiar with z3. Please note
the difference between the z3 variable z3.Int(‘x’) and the python
variable x . The latter can be re-assigned during the execution, but the
former cannot.
The input of our program is a python source code in string format.
The output of our program is a z3 expression. You can use any library
to parse the python source code. You are welcome to search on the internet
for any documentation. Please do not collaborate with others on the
assignment.
Z3 can also handle conditionals:
>>> z = z3.If(a > b, a, b)
>>> z
If(a > b, a, b)
More examples:
Input 4:
def foo(x, y):
if x > y:
return x
return y
Output 4: If(x > y, x, y) .
Input 5:
def foo(x, y):
z = x
if x > 10:
z = x – 10
return z
Output 5: If(x > 10, x – 10, x) .
Input 6:
def foo(x, y):
if x < 10:
return x
x -= 10
if x < 10:
return x
return x - 10
Output 6: If(x < 10, x, If(x < 20, x - 10, x - 20))