# Proving Algorithms Correct

Bart Massey

### What is a proof?

• An argument designed to convince other people of a truth

• In particular, a structured argument
• Each step of reasoning so small as to be inarguable
• In other words, if I'm not sure it's a proof, it's not
• Proofs are typically symbolic

• Except in geometry and a few other places
• Aids mechanical generation and evaluation

### How do we prove an algorithm correct? We work from the pseudocode toward the problem statement.

• An algorithm is correct if it returns the correct output for every valid input

• The problem statement describes

• valid inputs
• correct outputs
• The pseudocode describes what the algorithm returns as output for a given input

### Why proof vs execution?

• Because there are too many (in fact, infinite) possible executions: a proof can cover an arbitrary number of executions in a compact form.

• However, if you can exhaustively prove what you need...

### Proving sorting

        SEQUENCE SORTING

Instance: A sequence s of elements drawn from a set S.  A
total order q: SxS->B s.t. q is true when its
arguments are "in order".

Problem: Find a sequence t drawn from S s.t.
t in perm(s) and
forall i, j in 1..|S| . i < j => q (t[i], t[j])

ALGORITHM DUMBSORT
To sort s:
for each permutation t of s
if t satisifies the definition of sorted
return t

ALGORITHM SELECTION SORT
To sort s:
t <- empty
while s is not empty
let i be the index of a minimum element of s
append s[i] to t
delete s[i] from s

Last modified: Tuesday, 15 April 2014, 3:46 PM