Finding an invariant for a simple loop

I have never felt so woefully inadequate as I am when trying to prove to Dafny that my program is correct, so I need your help: The given program looks as follows:

method doingMath(N: int, M: int) returns (s: int)
requires N <= M //given precondition
ensures 2*s == M*(M+1)-N*(N+1) //given postcondition
{
    var a: int := N;
    var r: int := 0;

    while a < M 
    invariant FIND ME!
    {
        a := a+1;
        r := r+a;
    }
    return r;
}

As first step I wanted to figure out what the loop does, so I made a table:

With that I worked out a loop invariant for r:

invariant r == (a-N)*N + (a-N)*((a-N)+1)/2

which holds before (0==0), and after each iteration of the loop (following the formula). Clearly it does not satisfy the Termination criteria

When the loop terminates, the loop invariant along with the reason that the loop terminated gives us a useful property.

Since the loop guard is simple enough I figured the complete invariant should be

invariant a<=M && r == (a-N)*N + (a-N)*((a-N)+1)/2

And thus my invariant satisfies Initialization, Maintenance and Termination. However Dafny complains that

Error: This loop invariant might not be maintained by the loop.

How do I make Dafny happy?

I managed to stay clear of any non-linear arithmetic hick-ups. Here's how I think of the problem:

You're trying to establish a postcondition that, for the sake of clarity, I will write as P(s, N, M), that is, some function of s, N, and M. One technique for coming up with a loop that does this is "replace a constant by a variable". What this means is that you pick one of the constants of the desired postcondition (here, you can choose either N or M, since s is not a constant) and replace it by a variable that is going to change in each loop iteration. Let's pick M as the constant and let's introduce (as you had already done in your program) a as the variable. Since we picked M as the constant, we'll want the final value of a to be M, so we'll start a at N. We then have:

method doingMath(N: int, M: int) returns (s: int)
  requires N <= M
  ensures P(s, N, M)
{
  var a := N;

  while a < M
    invariant N <= a <= M
    invariant P(s, N, a)  // postcondition, but with variable a instead of constant M
}

If you type in this program (but expand out the P(s, N, a) to the actual condition), then you will find that Dafny proves the postcondition. In other words, the verifier is giving you the information that if you can establish and maintain this loop invariant, then the program will correctly establish the postcondition.

You can see this yourself, too. The negation of the loop guard gives you M <= a, which combined with the loop invariant a <= M gives you a == M. When you combine a == M and the loop invariant P(s, N, a), you get the postcondition P(s, N, M).

Great. But the verifier issues a complaint that the loop invariant does not hold on entry. This is because we didn't provide any initial value for s. Since a has the initial value N, we need to find a value for s that satisfies P(s, N, N). That value is 0, so we update the program to

method doingMath(N: int, M: int) returns (s: int)
  requires N <= M
  ensures P(s, N, M)
{
  var a := N;
  s := 0;

  while a < M
    invariant N <= a <= M
    invariant P(s, N, a)
}

Next, let's write the loop body. (Notice how I have started with the loop invariant, rather than starting with loop body and then trying to figure out an invariant. For these sorts of programs, I find that's the easiest way.) We already decided that we want to vary a from the initial value N up to the final value M, so we add the assignment a := a + 1;:

method doingMath(N: int, M: int) returns (s: int)
  requires N <= M
  ensures 2*s == M*(M+1) - N*(N+1)
{
  var a := N;
  s := 0;

  while a < M
    invariant N <= a <= M
    invariant P(s, N, a)
  {
    a := a + 1;
  }
}

This addresses termination. The final thing we need to do is update s inside the loop so that the invariant is maintained. This is mostly easily done backward, in a goal-directed fashion. Here's how: At the end of the loop body, we want to make sure P(s, N, a) holds. That means we want the condition P(s, N, a + 1) to hold before the assignment to a. You obtain this condition (again, remember we're working backward) by replacing a in the desired condition with (the right-hand side of the assignment) a + 1.

Okay, so before the assignment to a, we want to have P(s, N, a + 1), and what we've got just inside the loop body is the invariant P(s, N, a). Now, it's time for me to expand P(...) to your actual condition. Alright, we have

2*s == a*(a+1) - N*(N+1)                (*)

and we want

2*s == (a+1)*(a+2) - N*(N+1)            (**)

Let's rewrite (a+1)*(a+2) in (**) as 2*(a+1) + a*(a+1). So, (**) can equivalently be written as

2*s == 2*(a+1) + a*(a+1) - N*(N+1)      (***)

If you compare (***) (which is what we want) with (*) (which is what we've got), then you notice that the right-hand side of (***) is 2*(a+1) more than the right-hand side of (*). So, we must arrange to increase the left-hand side with the same amount.

If you increase s by a+1, then the left-hand side 2*s goes up by 2*(a+1), which is what we want. So, our final program is

method doingMath(N: int, M: int) returns (s: int)
  requires N <= M
  ensures 2*s == M*(M+1) - N*(N+1)
{
  var a := N;
  s := 0;

  while a < M
    invariant N <= a <= M
    invariant 2*s == a*(a+1) - N*(N+1)
  {
    s := s + a + 1;
    a := a + 1;
  }
}

If you want, you can swap the order of the assignments to s and a. This will give you

method doingMath(N: int, M: int) returns (s: int)
  requires N <= M
  ensures 2*s == M*(M+1) - N*(N+1)
{
  var a := N;
  s := 0;

  while a < M
    invariant N <= a <= M
    invariant 2*s == a*(a+1) - N*(N+1)
  {
    a := a + 1;
    s := s + a;
  }
}

In summary, we have built the loop body from the loop invariant, and we designed this loop invariant by "replacing a constant with a variable" in the postcondition.

Rustan