# Discussion Session 6: Program Verification¶

## Intepretation¶

formula ::=  true | false
formula ::=  not formula
formula ::=  formula and formula
formula ::=  formula or formula


Python code:

def formula_true():
return "True"

def formula_false():
return "False"

def formula_not(formula):
return {"Not": [formula]}

def formula_and(formula1, formula2):
return {"And": [formula1, formula2]}

def formula_or(formula1, formula2):
return {"Or": [formula1, formula2]}

def evaluateFormula(formula):
if is_true(formula):
return True
if is_false(formula):
return False
if is_not(formula):
return not evaluateFormula(formula["Not"][0])
if is_and(formula):
formula1 = formula["And"][0]
formula2 = formula["And"][1]
return evaluateFormula(formula1) and evaluateFormula(formula2)
if is_or(formula):
formula1 = formula["Or"][0]
formula2 = formula["Or"][1]
return evaluateFormula(formula1) or evaluateFormula(formula2)
return None


Discussion

• What’s the type for formula?
• How to prove that evaluateFormula is implemented correctly?
• What is correct? (Hint: Evaluation Rule)

## Bounded Exhaustive Testing¶

Set of all possible inputs is defined inductively. We can enumerate them exhaustively. See notes. The introduction of metric guarantees that we do enumerate all the possibilities.

• If formula is of format “true” or “false”, then its height is 1.
• If formula is of format “not formula0”, then its height is 1 + height of “formula0”.
• If formula is of format “formula1 and formula2”, then its height is 1 + max(height of “formula1”, height of “formula2”.
• If formula is of format “formula1 and formula2”, then its height is 1 + max(height of “formula1”, height of “formula2”.

Code:

def metric(f):
if is_true(f) or is_false(f):
return 1
if is_not(f):
return 1 + metric(f["Not"][0])
if is_and(f):
f1 = f["And"][0]
f2 = f["And"][1]
return 1 + max(metric(f1), metric(f2))
if is_or(f):
f1 = f["Or"][0]
f2 = f["Or"][1]
return 1 + max(metric(f1), metric(f2))

def formulas(n):
if n <= 0:
[]
elif n == 1:
return [formula_true(), formula_false()]
else:
fs = formulas(n-1)
fsN = []
fsN += [formula_not(f) for f in fs]
fsN += [formula_and(f1, f2) for f1 in fs for f2 in fs]
fsN += [formula_or(f1, f2)  for f1 in fs for f2 in fs]
return fs + fsN


## Proof by Induction¶

• Base Case: evaluateFormula is correct for formula whose height is 1.
• Inductive Step: The input formula has height n+1.
• Induction Hypothesis: evaluateFormula is correct for formula whose height is <= n.

## Example of fibonacci function¶

### Definition of fibonacci function¶

fib(n) =

0 if n = 0

1 if n = 1

fib(n-1) + f(n-2) if n > 1

### Implementation of fibonacci function¶

def Fib(n):
def Fib0(n, x, y):
if n = 0:
return y
if n > 0:
return Fib0(n - 1, x + y, x)

return Fib0(n, 1, 0)


For any n >= 0, fib(n) == Fib(n).

### Proof By Induction¶

For any n >= 0, for any a >= 0, Fib0(n, fib(a+1), fib(a)) == fib(a+n).

Base Case:
When n = 0, we have
for any a >= 0, Fib0(0, fib(a+1), fib(a)) = fib(a) <== (By def of Fib0)
Inductive Step:

n = m > 0

Inductive Hypothesis: For any m0 < m, for any a >= 0, Fib0(m0, fib(a+1), fib(a)) == fib(a+m0).

For any a >= 0, we have the following

Fib0(m, fib(a+1), fib(a))

= Fib0(m-1, fib(a+1) + fib(a), fib(a+1)) <== (By def of Fib0)

= Fib0(m-1, fib(a+2), fib(a+1)) <== (By def of fib)

= fib(a+1 + m-1) <== (By Induction Hypothesis)

= fib(a+m) <== (Done)

### Programming with Theorem Proving¶

Advanced programming languages provide us with abilities to write proof along with code so that the compiler can help check the correctness of our implementation. One example of such language is ATS.

dataprop fib (int, int) =
| fibzero (0, 0) of ()
| fibone (1, 1) of ()
| {n:nat} {r1,r2:int}
fibcons (n+2, r1 + r2) of (fib (n+1, r1), fib (n, r2))

fun Fib0 {n:nat} {a:nat} {r1,r0:int} .<n>.(
pf1: fib (a+1, r1), pf0: fib (a, r0)
| x: int n, y1: int r1, y0: int r0):<fun>
[r: int] (fib (a+n, r) | int r) =
if x = 0 then (pf0 | y0)
else let
prval pf2 = fibcons (pf1, pf0) // fib (a+2, r1 + r0)
in
Fib0 (pf2, pf1 | x - 1, y1 + y0, y1)
end

fun Fib {n:nat} .<>.(x: int n):<fun> [r:int] (fib (n, r) | int r) =
Fib0 (fibone, fibzero | x, 1, 0)


You can try type checking the code at http://www.ats-lang.org/SERVER/MYCODE/Patsoptaas_serve.php?mycode=hello.