Loop Invariants and General Invariants

Question

Let's say I have an iterative algorithm for the summation of numbers from a to b:

def summ(a, b):
    c, v = a, 0
    while c <= b:
        v = v + c
        c = c + 1
    return v

Firstly, is it correct to say that a <= c <= b is a loop invariant, and a <= c <= b+1 a generic invariant for the whole algorithm? If yes, is it redundant to specify these two invariants separately?

And secondly, are there any other invariants that I have not identified in the algorithm? Given an algorithm, how can you be sure that you have identified all the useful invariants?

For the second part of the question I was thinking, another invariant could be something like:

$$v = v_{0} + \sum_{i=0}^n c_{i}$$

where $v_{0}$ is the initialized value of $v$ and $c_{i}$ goes from $a$ to $b$.

Answer 1

is it correct to say that a <= c <= b is a loop invariant

Ummm, yes, mostly. I certainly agree with the intent. I would only be willing to say that is an "invariant" if we establish the base case, if we verify that the caller didn't mess up:

def summ(a, b):
    assert a <= b
    ...

Also, where you say b, I would say b + 1, since we can enter the loop with c == b and then the loop gets to do one more increment on c.

... and a <= c <= b+1

No, I disagree. Or rather, I understood the specification "summation of numbers from a to b" to mean that e.g. summ(3, 3) would give zero. Part of how that understanding is revealed is by noticing I didn't write assert a < b as the precondition. Now, maybe that was Author's Intent. I just didn't pick that up from what I saw written down.

Also, the expression you wrote admits of a == b + 1, which I believe is not your intent.

If yes, is it redundant to specify these two invariants separately?

For the a part, sure. Which leaves us with a pair of statements:

• c <= b
• c <= b + 1

Clearly if the 1st is true, the 2nd will definitely be true, it's redundant, yes.

---

Your LaTeX expression looks good to me.

---

There is a whole literature on finding invariants. See e.g. Automatically Generating Loop Invariants Using Quantifier Elimination from 2004. Much work has been done since then. Related areas are symbolic evaluation, concolic (concretized) evaluation, and leveraging unit tests to automatically synthesize source code bug fixes.

I invite you to import hypothesis. It comes from fuzz-testing, and is very good at revealing minimal test cases which violate some boolean property. It needs an oracle, so its best match is for I/O encode / decode, cryptographic encode / decode, and similar symmetric operations. Also, if you assign same problem to students A and B, obtaining a pair of independently implemented solutions, it is very good at answering the question "do these two implementations behave identically?" That is to say, it is terrific at revealing inputs which correspond to corner cases.