CODEWITHSUNDEEP
loops
Nubbins
Nubbins

Reputation: 49

Understanding Loop invariant. Finding and proving them for an algorithm

I need a little help understanding loop invariant. I just need someone to explain how to go about finding a loop invariant and proving it for the following algorithm:

public int sumSquares ( int n )
{
    int sum = 0 ;
    for ( int i = 1 ; i <= n ; i++)
    {
        sum += i ∗ i ;
    }
    return sum ;
}

Upvotes: 4

Views: 561

Answers (3)

user1196549
user1196549

Reputation:

As said by others, the invariant is true before and after each iteration. In general it becomes invalid somewhere inside the loop and is later restored.

To establish a proof, you track conditions that hold between the individual statements and relate them to the invariant.

For the given example, follow the annotations; for clarity, the for statement is rewritten as a while.

    int sum = 0 ;
    i= 1;
    // This trivially establishes the invariant: sum == 0 == Σ k² for 0<=k<i=1
    while (i <= n)
    {
        // The invariant is still true here (nothing changed)
        sum += i ∗ i ;
        // We now have sum == Σ k² for 0<=k<=i (notice the <=; this differs from the invariant)
        i++;
        // As i has been increased, sum == Σ k² for 0<=k<i is restored
    }
    // Here the invariant holds, as well as i == n+1
    // Hence sum == Σ k² for 0<=k<n+1
    return sum ;

In general the invariant expresses that we have solved a part of the problem. In the given example, it says that a part of the sum has been computed. Initially, the partial solution is trivial (and useless). As the iterations progress, the partial solution gets closer and closer to the complete one.

Upvotes: 1

Pawel Gumiela
Pawel Gumiela

Reputation: 2040

You can also note the similarity to mathematical induction.

When you prove that a property holds, you prove a base case and an inductive step.

If the invariant hold before the first iteration it is similar to the base case. Showing that the invariant loop holds from iteration to iteration is similar to inductive step.

Upvotes: 1

CollinD
CollinD

Reputation: 7573

The loop invariant is a statement that is provably true immediately before and after each iteration of a loop. Turns out there are lots of these, but the trick is proving one that actually helps.

For example, it is true that

the value of i is always equal to i before and after each iteration.

Not terribly helpful. Instead, think about what you want to prove

When i is equal to n, sum is equal to the sum of the first n squares

In this case, if you want to prove your algorithm produces the sum of the first n squares, you'll want to state the following invariant. For each i,

The value of sum is equal to the sum of the first i squares

Upvotes: 4

Related Questions