Proofs of Correctness of Algorithms (Jan 18)

Note: You should have Java up and running on your own computer by now. If you are having trouble with this, let me know as we will be using Java in class next week.

Course website - Tutorial 2

You were given a lot of warmup exercises to do before this tutorial. I will briefly cover a few of the important concepts, before moving on to the main exercise. You will then be given some time to attempt the exercise in steps, and you can ask for help during this time. I will cover the steps to follow, but I won't go through the solution in detail. You can do this on your own after the solution is posted by the prof. Reading solutions don't help you nearly as much if you haven't tried to solve the problem, hence the focus on the exercise rather than the solution.

There is a link to the Linear Search solution on the course website, but you cannot access it yet. I assume it will be made available after the Thursday morning tutorials.

Warmup exercises

Since most people did not do these, please take a few minutes to at least skim through them and find out what you should know. The Fundamental Concepts are especially important, you need to know these to do the proofs of correctness. The proofs part (after propositional logic) include 4 very short exercises to prove single statement algorithms. This will take you less than 5 minutes.

If you plan to look at the solutions, PLEASE keep in mind:

  1. Reading solutions will make you feel like you understand something, but if you haven't attempted the problem, it won't be very helpful. Just try the problem again 2 days after you read the solution, and you'll realize this.
  2. For the Fundamental Concepts, I've taken all the definitions from the lecture notes. You should try to come up with your own wording; paraphrase it in a way that makes sense to you.
  3. I do not guarantee all my solutions are correct. If you notice any errors, please let me know (thanks).

Proofs

First, you want to take your problem definition and design pseudocode. This step is important, and can affect the complexity of your proof.

Take for example the Linear Search problem:

Better solution Another solution

int LinearSearch(T key)
   i = 0

   while(i < n) and (A[i] ≠ key) do
      // loop invariants are true here
         i = i + 1
   end while

   if i < n then
      return i
   else
      throw KeyNotFoundException
   end if

int LinearSearch2 (T key)
   i = 0

   while(i < n) and (A[i] ≠ key) do
      // loop invariants are true here
      i = i + 1

      if A[i] == key then
         return i
      end if

      if i == n then
         throw KeyNotFoundException
      end if
   end while

Both algorithms will work, but the first algorithm is much simpler to prove. This comes down to making our loop simpler, and moving the conditionals outside the loop. The conditionals are then executed only once, outside the loop. You can then consider the cases from the conditional, independent of the loop.

If you look at the proof examples in the warmup exercises above, you will see 4 examples. In these examples, you are given precondition {P}, some single statements S, and postcondition {Q}. Assuming you have valid input which satisfies P, and you execute S, you should get output matching Q. When you have a loop in your program/algorithm S, the overall process stays the same. You need to go through each step in S, before checking the output with Q. However, the loop can be both confusing and intimidating.

To conceptualize this, imagine a loop L which executes n times.

L0, L1, L2, ... Ln

Looking at our pseudocode (the better solution), our algorithm is like this:

{P} Loop; Conditionals {Q}
{P} L0, L1, L2, ...Ln; Conditionals {Q}

Since we want to move from one state to the next, we want to start at P. We then move towards Q one step at a time. The problem is that we don't know how many times the loop will run. If the loop runs 5 times, then i = 5. If it runs a hundred times, then i = 100. That means the state at Ln can vary. We need to find something that stays the same, no matter how many times the loop body executes; this is called the LOOP INVARIANT. The loop invariant, by definition, holds true at the beginning of every loop execution, after the loop conditions have been satisfied, but before the loop body actually executes. (Refer to the pseudocode above.) Regardless of 5 executions or 100, the loop invariant will be true at the beginning of the last execution in the loop (Ln). We can then trace the last loop execution as single statements, giving us a known state before we move on to the conditionals.

Of course, you can't just make up any loop invariant. As part of a proof, you need to show the loop invariant indeed holds true at the beginning of each loop execution. We do this by induction (base case + induction step). We are trying to show that given any loop execution i and the subsequent execution (i+1st), the loop invariant holds true. If we can show this, then we can apply this proof to executions i+2nd, i+3rd, i+4th, etc. until we reach the last execution.

Assuming you've proven the loop invariant to be correct, and you traced the last loop execution (from the loop invariant), you would have derived the state of your algorithm at the end of the loop. You can then continue with the single statements (in this case, the conditionals).

At this point you have proved partial correctness. To prove (complete) correctness, you need to show that your loop will halt and therefore your algorithm S will halt. We need to find what's called the LOOP VARIANT, which is something which changes after every loop execution. The loop variant usually depends on the loop condition. The loop variant is a function of some variables (again look at the loop condition), which decreases after every loop execution. Eventually the loop variant should be equal or less than 0; this is when your loop terminates. By proving partial correctness and termination, you have proven (complete) correctness.