# Check whether loop invariants are correct?

I'm trying to prove some code is correct, using Hoare logic. How do I check whether my loop invariants are correct?

I'm asked to prove (using Hoare Logic) that the following program is valid:

x=1;
i=N;
while (i!=0){
i--;
x*=A;
}


with the pre-condition that N>=0 and post-condition that x=A^N.

This is my attempt:

{ N>=0 }
x=1;
i=N;
{i >= 0}
while (i!=0){
{i>=0}
{x = product(i in (0:N-i); A)}    (loop invariant)
i--;
x*=A;
}
{x = A^N}


The curly brackets represent invariants that are supposed to hold at that point in the code. The 2 loop invariants seem to hold for every instance of the loop.

Is my attempt correct? Are my loop invariants sufficient? Do I have too many?

I know that {i>=0} is given by the definition of the loop. Should I remove that loop invariant then, since it is the case by default?

EDIT: My new attempt

{N>=0}
x=1;
{x = A^(N-N)=A^0=1}
i=N;
{x = A^(N-i)}
while (i!=0){
{i>=0}
i--;
{x = product(i in (0:N-i-1);A)}
x*=A;
{x = product(i in (0:N-i);A)}
}
{x=A^N}


Rather than telling you whether your specific invariants are correct, let me teach you the procedure for how you can check whether your invariants are correct on your own.

Basically, you break it down by looking at each chunk of code separately. For each chunk of code, you look at the invariant before it and after it and see whether they're consistent with that chunk of code. If this check passes for all of the chunks, you're done: you're entitled to conclude that your program is "correct". The beauty of this is that this helps you break down the task into small manageable pieces. You never have to think about the entire program as a whole -- you only look at one chunk, in isolation, at any given time.

The way you verify a chunk of code depends on what kind of statement it contains. There are only a few cases you need to worry about:

1. Straight-line code. Suppose you have a statement with no branching, e.g.,

{P}
stuff;
{Q}


What you need to do is check that if P is true before the statement, then after executing the statement, Q will surely be true. In other words, if all we know about the state of the program is that P is true, and then we execute stuff, then afterwards it is guaranteed that Q will be true.

Notice that you check this by looking only at P, Q, and stuff: you shouldn't need look at any code in the rest of the program. If you find yourself trying to think about what the rest of the program is doing or ways you might be able to reach this chunk of code, you're doing something wrong, and probably you need to strengthen P (add some additional clauses that record more information about what states of the program are possible at that point).

2. Loops. Suppose you have a while-loop, e.g.,

{P}
while (e) {
{Q}
stuff
{R}
}
{S}


Then you need to check four things. First, you need to check that the path that skips the loop entirely is valid, i.e., check that P && !e implies S. Second, you need to check that, on the first iteration of the loop, the loop invariant will hold: i.e., check that P && e implies Q. Third, you need to check that on any iteration of the loop, the following is valid:

{Q}
stuff
{R}


Fourth, you need to check that R && e implies Q. Fifth, you need to check that on the last iteration, S is enforced, i.e., that R && !e implies S. If all of these checks pass, then your invariants for the while-loop are OK.

Here's a different way to think about it that might feel more intuitive. You can try to find an invariant T that lets you annotate the loop with

{T}
while (e) {
{T && e}
stuff
{T}
}
{T && !e}


All you need to check is that the following code block is valid:

{T && e}
stuff
{T}


If that code block is valid, then the entire while-loop construct is acceptable.

3. Conditional statements. If statements can be handled similarly, but are a bit easier than while-loops. For instance, if you have

{P}
if (e) {
{Q}
stuff
{R}
}
{S}


then you need to check both the false-path and the true-path through the conditional. To check the false-path, check that P && !e implies S. To check the true-path, check that P && e implies Q, that R implies S, and that the following is valid:

{Q}
stuff
{R}


In this way, you should be able to check all of your invariants step-by-step. The only two things you need to know how to do are: (1) check whether one logical formula implies another, and (2) verify invariants for straight-line code. Everything else reduces to those operations.

With practice, you'll find that this becomes pretty mechanical. And with practice, you'll find that many of these invariants can be omitted (if it's straightforward for a reader to re-derive them), but when you start out, it's best to be verbose and include them all, without trying to omit stuff.

• Have you checked if we have another general answer on the site? This one may be reference-answer material, good job! (Disclaimer: I did not real the details, I'm just observing the general and instructive nature of the answer.) – Raphael Dec 9 '15 at 21:54
• For loops, writing the pattern differently shows better what the invariant may look like: {I} while (e) do {I & e} stuff {I} done {I & !e}. – Raphael Dec 9 '15 at 21:56
• What a great answer! I'm going to post an update and see if I interpreted all of what you said correctly. – Greg Peckory Dec 9 '15 at 21:56
• – Gilles 'SO- stop being evil' Dec 9 '15 at 22:00
• @Gilles Maybe? I guess you guys can discuss in Computer Science Chat what kind of reference questions for verifications we should list in the meta thread. – Raphael Dec 9 '15 at 22:09