Author: Stan Eisenstat
Subject: Re: [Cs223] Loop Invariants
Date: Monday, 02 Mar 2020, 07:59:13

c:
Bcc: bcc

    > Message Posted By: Unknown
    >
    > How do you pick a good loop invariant? and should it tell us anything
    > about the algorithm?

The exams will not require loop invariants.

A loop invariant must:

* be true before entering the loop;

* be true at the end of the body of the loop if it is
  true at the beginning; and

* imply the property that you want satisfied when the
  loop exits.

The choice of a good loop invariant is often more art
than science.
=====

    > You mentioned in class that loop invariants can be used to check if the
    > output of an algorithm is correct. Does that mean the loop invariant must
    > somehow relate the input with the output?

Yes, as described above.
=====

    > Let's say we have the following loop:
    >
    >   sum = 0;
    >   for (int i=0; i<5; i++) {
    >     sum +=i;
    >   }
    >
    > Can the loop invariant be something like i<=sum? Would it be a good loop
    > invariant? If so, would it tell us anything significant?


Rewrite the loop as

  sum = 0;
  int i = 0;
  while (i<5) {
    sum +=i;
    i++;
  }

to better separate the different pieces of a for loop.
If your goal is to prove that when the loop ends sum is
equal to the sum of the integers between 0 (inclusive)
and 5 (exclusive), then then a loop invariant would be

  sum = "sum of all integers j satisfying 0 <= j < i"

Clearly it satisfies the properties above.

--Stan-