0
$\begingroup$

What is the logic behind using a loop invariant proof for proving the correctness of an algorithm? How is it proved that using the loop invariant proof indeed proves the correctness of a loop?

$\endgroup$
1
  • 1
    $\begingroup$ The topic of loop invariants is standard, and you can find many textbooks and lecture notes covering it. There is even a Wikipedia page with examples. $\endgroup$ Jan 26 at 12:39

2 Answers 2

0
$\begingroup$

What does it mean to say a program is correct?

When we say that a program (or a segment of code) is correct, we mean if the proper condition to run the program holds, and the program is run, then the program will halt, and when it halts, the desired result follows.

The proper condition to run a program is called its precondition.

That the program halts is called termination.

The desired result following a program’s termination is called its postcondition.

Note that program correctness is always described with respect to its precondition and postcondition I.e., correctness also depends on precondition and postcondition.

The pre/post-condition pair is called the program’s specification.

With the above terminology, we can think of program correctness as follows. Program correctness: if precondition then (termination and postcondition).

So proving correctness means proving precondition ⇒ (termination and postcondition). Sometimes it is convenient to prove separately the termination part and the postcondition part. In this case we divide the proof into two parts. (a) precondition ⇒ termination — this part is sometimes just called termination,

(b) (precondition and termination) ⇒ postcondition — this part is called partial correctness.

So proving correctness means proving partial correctness and termination.

⋆ Proving correctness of iterative programs

Iterative programs are programs with loops. When proving that a loop (or program with a loop) is correct (with respect to some pre/post-condition pair), we prove partial correctness and termination separately. For both parts we need a loop invariant, which describes how the variables in the loop are used to achieve the postcondition.

◦ Loop invariants A loop invariant (LI) is a statement that is true on entering the loop, and after every iteration (assuming the precondition holds). To prove an LI, we use a form of induction, where

(a) Basis: we prove that the LI holds on entering the loop,

(b) Induction Step we prove that if the LI holds before an iteration, then it also holds after that iteration.

$\endgroup$
4
  • $\begingroup$ Two steps missing: We prove that the loop ends eventually, and we use that fact that after the loop, both the loop invariant is true, and the condition for repeating the loop is false. For example if your loop looks like "for (i = 0; i < n && a[i] != 0; ++i) { ... } then after the loop finishes, you know that either i >= n or a[i] == 0, and the loop invariant is true. $\endgroup$
    – gnasher729
    Jan 26 at 13:58
  • $\begingroup$ What I wanted to ask was, how did we arrive at this conclusion that using loop invariant proof proves the correctness of the iterative algorithm? What is the intuition behind it? I am not able to see how they are related. $\endgroup$
    – Kashish
    Jan 26 at 14:07
  • $\begingroup$ @Kashish What we do is generally we find a statement (loop invariant) which relates "variables" inside the loop, (because it is difficult to check for every iteration ) so with given pre conditions and with help of loop invariant we achieve the goal(post conditions) , so we achieved the post condition means the program is indeed correct. So loop invariant helps to connect pre condition and post conditions for given loop $\endgroup$
    – user145450
    Jan 26 at 15:27
  • $\begingroup$ @Kashish You prove the first iteration does the right thing. You prove the second iteration does the right thing. You prove the third iteration does the right thing. And so on. All the proofs have to be the same proof, because the loop could go for a billion iterations and you won't write a billion different proofs. $\endgroup$
    – user253751
    Jun 2 at 16:32
0
$\begingroup$

The proof of correctness of an algorithm can be seen as a succession of annotations like

{ P }
Statement
{ P' }

where it can be proven that the statement guarantees the postcondition P' if the precondition P holds.

In the case of a loop, the conditions P must be somewhat special because if we unroll a loop, say three times, we write

{ P }
Loop-body
{ P' }
Loop-body
{ P'' }
Loop-body
{ P''' }

The predicate must be such that it remains true across the iterations (whatever their number), hence its name, "invariant".

Example: we want to compute the sum of the integers from 1 to n. We will do so by accumulating integers into a single variable.

s= 0
i= 0
while i ≤ n:
  s+= i
  i+= 1

Obviously, we are computing partial sums and the invariant will express that s contains the i-th partial sum, which we denote as S(i)$:=\sum_{k=0}^{i-1} k$.

s= 0
i= 1
{ s = S(1) = S(i) }
while i ≤ n:
  { s = S(i) }
  s+= i
  { s = S(i+1) }
  i+= 1
  { s = S(i) }
{ s = S(n+1) }

As you can see, we start the loop with the invariant holding, we perform some operations that invalidate it, then we restore the invariant so that another iteration can be performed in similar conditions.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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