## Proving Algorithms Correct

# 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

- In particular, a
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