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
  • 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