Tips for constructing basic loop invariants?

Question

One of the topics that I've struggled to grasp the most in my basic computer theory course is that of making a loop invariant to prove correctness of an algorithm. Even with what should be fairly straightforward algorithms, I just don't really understand what sort of properties I should be using in order to make an effective loop invariant that helps to prove algorithm correctness.

Here's an example of some basic pseudocode that I can't create a loop invariant for:

FUNCTION(a, b):
p <- 1
l <- 0
while p < a:
    p <- p * b
    l <- l + 1
return l

Does anyone have some tips or resources that would help me get a better grasp on making loop invariants?

Answer 1

For that example, you want an invariant about $p$ and $l$ because these are the values that are changing. Before the loop, you have $p=1$ when $l=0$. After the first time trhough the loop, you have $p=b$ and $l=1$. Then $p=b^2$ when $l=2$. Now you can guess a general invariant: $p=b^l$. Next, prove it by induction. So, what is the value of $p$ (and $l$) when the loop ends? For that you need to answer: how many times is the loop executed?

Answer 2

The appropriate loop invariant dependents on the property you want to show that the program has. It doesn't make sense to say: here is a program, what should be the loop invariant.

The most common properties that are used are eventual termination (i.e. the program will terminate in finite time) and correctness of the output (i.e. when the program terminate, it outputs the value of the associated function on the given input).

Finding a good loop invariant is similar to finding a mathematical proof of a theorem.

Answer 3

Loop invariants are simply the desired property in your iterations that you would want to maintain throughout the execution.

You could use this to prove program correctness. That is if you started off with a "correct state" and maintained it throughout the course of algorithm(invariant), then you know that you have a correct algorithm.

So you would need to show that you have a desired property, the invariance, in 3 steps:

i. Initialization: Can you show that you have the invariant property of the algorithm in the first step of the iteration of the loop?

ii. Maintenance: Are you maintaining the invariance? If it was true for the iteration up to that point, is it true for the next iteration?

iii.Termination: When your loop finally terminates, the invariant will be used to show that the algorithm you wrote is correct.

Let us take an example to prove that the algorithm below is correct. OR how do we know that building of max heap actually builds a max heap!

BuildMaxHeap(A)
  heap-size[A] = length[A]
   for i : length[A]/2 to 1
       Max-Heapify(A, i)
Source. CLRS

Following our above intuition, we need to decide on a desired property that we maintain throughout the algorithm. What is the desired property in the MaxHeap? heap[i]>= heap[i*2]. No matter how much you mess around with the heap, if it still has that property, then it is a MaxHeap, right?

Initialization : Prior to the first iteration. Everything is a leaf so it is already a heap.

Maintainence : Let us assume that we have a working solution till now. The children of node i are numbered higher than i. MaxHeapify preserves the loop invariant as well. We maintain the invariance at each step.

Termination : Terminates when the i drops down to 0 and by the loop invariant, each node is the root of a max-heap.

Hence the algorithm you wrote is correct.

The basic idea is to figure out what is it that you want to achieve by maintaining the invariance and prove it in 3 steps.