int sumFrom( int a, int b )
  sum ← 0
  i   ← a
  while (i < b)
    sum ← sum+i
    i   ← i+1
  return sum


[First you'll need to add comments saying what this
 function does, and then you'll need to phrase
 its purpose in terms of functions, summation-notation, sets, whatever --
 something that we can reason about mathematically.]





Let's walk through the thought process.
We might realize partway through, we need to go back and tweak things.



Attempt 1
What does the code do?
Stupid programmer, didn't provide a description!

/** sumFrom: int, int --> int,  with a ≤ b.
 * Return ∑[a,b).
 * (Using half-open intervals is often handy, to avoid
 *  lots of adding-or-subtracing-by-one-to-get-interval-correct.)
 * Note that if a = b, this interval is empty,
 * so we appropriately return 0.
 */

Next we need to determine the parts of our proof: G, L1, C.
 The goal.  That's easy enough:
When we finish the loop, we want 
          sum = ∑j=ab-1j
Note how we're relating program-variables to a 
mathematical expression that has meaning aside from the program.
Note that a good program-description matches this.
[We'll use the indexed-sum notation for familiarity,
 rather than the interval-notation, but either one would work fine.
 It's neater to use the interval-notation throughout, but less standard.]

 The loop invariant L1.  This is the one part of the proof that
requires non-formulaic thought.
Ask yourself: what is true on the (say) 17th iteration of the loop?
Ah, sum isn't the final quantity, but it is a+(a+1)+...+(a+16).
How to write this in terms of the variables in the program?
Happily, the variable i keeps tracks of where we are in the loop, so
we can exactly characterize the value of sum:
   sum = ∑j=ai-1j
There's a moment of thought about the summation's upper index: i, or i-1?
Remember we'll want this statement to be true before the loop starts,
as well as just before every test.  So yes, i-1 is the correct upper bound.

 C, the loop condition:
We never have choice about this one: it's dictated by the code.
Here, C is i < b.



Okay, now we're ready to begin, and it should be smooth sailing.

Loop invariant holds initially
Initially we see that i=a and sum=0.
  ∑j=ai-1j = ∑j=aa-1j = 0 = sum
so L1 holds.

Loop invariant maintained
That is, L1 ∧ C → L1′.
That is, we want to show
  L1′ = ∑j=a′i′-1j.
But we know from the loop hypothesis L1, that
  sum = ∑j=ai-1j,
and by the code we can see how the primed and non-primed variables relate:
  sum′ = sum+i
  i′   = i+1
  a′   = a     [note]
Note that we ponder for a second, whether we want “sum+i” or “sum+i′”.  
We quickly see that yes we wrote the correct version.
We also realize now how (by adding primed versions) we've left the programming
domain (where a variable's value changes over time)
to regular ol' math variables that we can reason about.


Okay, it's only a bit of algebra to get from L1 to L1': we know
   sum   = ∑j=ai-1j
   sum+i = ∑j=ai-1j + i
   sum′   = ∑j=aij = ∑j=a′i′-1j
which is exactly what we want.

The sharp reader will note that really, a is a program variable that
could conceivably change; L1′ should talk about a′, not a.
True; we'll omit "a=a′ (by insepcting code)".
But realize that if we call a function in the loop body,
and the function modifies our variable a,
then (even though it doesn't look like a changes)

Hmm, we didn't need to use C to conclude L1′.  That's fine, though
sometimes it is needed.

Leaving the loop implies Goal
That is, L1 ∧ ¬C → G.
In our case, we want to conclude
   sum     = ∑j=ab-1j
and we know that
   sum     = ∑j=ai-1j
   ¬ i<b   (that is, i≥b).
This is almost extremely easy.
If we know that i=b, we'd be home free: substituting in for L1 would give G.
(That's why we phrased L1 the way we did!)

But technically, how do we get i=b, when all we're given is i≥b?
Clearly we're not given enough!
Is this a potential bug with our program?
After a moment of thought: no, clearly when we finish the loop we'll have i=b.
It's just that we know even more than L1 ∧ ¬C.
Well, if we really know that, we should include that knowledge in our proof:
In this case, we'll make our loop invariant stronger:
let L2 be “i≤b”, and make our real invariant
     L∗ = L1 ∧ L2.
Sure enough, now L∗ ∧ ¬C is enough to get what we
want: i≤b ∧ i≥b yields i=b.

So:  We realize that our original loop invariant L1 wasn't
quite enough; we need the stronger statement L∗.  We'll go back
and re-write our proof; fortunately it's easy to modify how the loop invariant 
is maintained.  How about showing that L2 holds initially?
This is also true, for a lucky detail: the program's contract
required a≤b, which will make things easy.

termination
We see that i is an integer (which precludes -∞),
and it increases by 1 each iteration,
so² eventually i ≥ b must hold, which is ¬C.




Attempt 2 -- success
Here is the same proof, re-written to use L∗ in all the parts.
Happily, we are typing our solution, so it's easy to use an editor
to patch up our solution.  We also re-write it to make the presentation cleaner.
(Re-writing for clarity is a routine part of doing proofs!)


/** sumFrom: int, int --> int,  with a ≤ b.
 * Return ∑[a,b).
 * (Using half-open intervals is often handy, to avoid
 *  lots of adding-or-subtracing-by-one-to-get-interval-correct.)
 * Note that if a = b, this interval is empty,
 * so we appropriately return 0.

int sumFrom( int a, int b )
  sum ← 0
  i   ← a
  while (i < b)
    sum ← sum+i
    i   ← i+1
  return sum

 G, our goal, is: sum = ∑j=ab-1j 
 L∗, our loop invariant, is L1∧L2,
where L1 is sum = ∑j=ai-1j
and   L2 is i≤b. 
 C, the loop condition, is: i < b. 
 

Okay, now we're ready to begin, and it's smooth sailing.

Loop invariant holds initially
Initially we see that i=a and sum=0.  
L1 holds: ∑j=ai-1j = ∑j=aa-1j = 0 = sum
L2 holds: By the function's pre-condition, a≤b;
combined with i=a we have i≤b, which is L2.
Thus L∗=L1∧L2 holds initially.

Loop invariant maintained
That is, L∗ ∧ C → L∗′.  It suffices to show two parts:
 L1∧C→L1′
That is, we want to show L1′, that sum′ = ∑j=a′i′-1j.
We know
  sum = ∑j=ai-1j,     [from L1]
  sum′ = sum+i        [by code]
  i′   = i+1          [by code]
  a′   = a            [by code¹]
Using these, we just do some algebra to work from L1 towards L1′:
   sum   =  ∑j=ai-1j
   sum+i = (∑j=ai-1j) + i
   sum′   =  ∑j=aij = ∑j=a′i′-1j
which is exactly L1′

L2∧C → L2′
Knowing C (namely, i<b), then clearly i+1 ≤ b (by properties of integers).
Since i′=i+1 and b′=b, we have i′≤b′, which is L2′.

Here in our corrected version, we see that C really does have a part to play
in maintaining L&lowast.  Interestingly, showing L1′ doesn't 
require using C, and showing L2′ doesn't require using L2. 
Leaving the loop implies Goal That is, L∗ ∧ ¬C → G.
Between L2 (namely i≤b) and ¬C (namely ¬(i<b)), we have i=b.
In this case, L1 is
   sum = ∑j=ai-1j = ∑j=ab-1j
which is precisely our goal G.   (Whee!)

termination
We see that i is an integer (which precludes -∞),
and it increases by 1 each iteration.
By properties of integers, eventually i ≥ b must hold, which is ¬C.







Attempt 3 -- perfection!
Exercise
We can actually remove the requirement 
One approach would be to have a big two-case proof,
depending on whether a≤b initially.
But slightly more cleanly, the two cases can be subsumed within
our proof structure.
Your task:
Come up with a statement L3 -- a strengthened version 
of L∗ -- such that the proof works for this third invariant.



/** sumFrom: int, int --> int
 * Return ∑[a,b).
 * (Using half-open intervals is often handy, to avoid
 *  lots of adding-or-subtracing-by-one-to-get-interval-correct.)
 * Note that if a ≥ b, this interval is empty,
 * so we appropriately return 0.
 */
define sumFrom( int a, int b )
  sum ← 0
  i   ← a
  while (i < b)
    sum ← sum+i
    i   ← i+1
  return sum


Further practice
Lots of tweaks here, if you want to give other things a try:


Without referring to these notes, re-do this proof
but use the notation ∑j∈[a,b)j
rather than ∑j=ab-1.


Tweak this program to calculate the sum of numbers in [a,b] instead.
How does the proof change, exactly?


What if a,b can be arbitrary reals?
What should the function be returning in this case?


Make up a similar function (computing factorial, or fibonacci numbers, or ...)


More interesting, think of a loop problem that's not about numbers
(say, looping through a list rather than recurring through it).
Phrase the invariant for this loop.
(You'll find you'll need to give closer thought to the loop's goal -- but
as a good programmer, that's something you should have already described
accurately in the comments!)







¹A comment on the "obvious" fact that a′=a: Just because a
doesn't appear in the code isn't quite enough; we are also realizing
that we're not calling a different function (which might change the
value of our a.)  By the way, functions are being called -- the
built-in function is being called.   Furthermore, in languages like C++ where 
you can overload assignment (or addition), suddenly you need to prove that 
that code isn't modifying our variable.  To make things worse in C++, you can't
just argue "the other function doesn't have the variable a in scope, so it
can't modify it", because in C++ writing off the end of an array can change
arbitrary memory locations.  Proofs for C++ programs are difficult;
and it's not coincidence that buggy C++ programs are very easy to write.
[back]


²Keep in mind that it's not sufficient to say that
a value just increases w/o specifying a minimum amount:
e.g. the series 1/2,3/4,7/8,… is always increasing but
will never exceed 2. [back]