Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

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?

share|improve this question

migrated from cstheory.stackexchange.com Apr 26 '11 at 1:05

This question came from our site for theoretical computer scientists and researchers in related fields.

add comment

3 Answers 3

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.

share|improve this answer
    
"It doesn't make sense to say: here is a program, what should be the loop invariant." Sorry, yeah, that makes sense. –  Mana Apr 26 '11 at 1:18
    
By which I meant what you just said makes sense. Not what I said. Argh, poor choice of words. –  Mana Apr 26 '11 at 1:39
add comment

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?

share|improve this answer
    
I took the function straight out of one of the previous finals for this course. It's supposed to return $l$. Thanks for the tips though! –  Mana Apr 26 '11 at 1:24
    
@Mana, right, I misread the code. I've edited my answer. –  lhf Apr 26 '11 at 1:26
    
Probably doesn't help that the typeface makes $l$ and 1 look practically identical in code, haha. –  Mana Apr 26 '11 at 1:29
add comment

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.

share|improve this answer
add comment

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.