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