WHILE STATEMENT: AN EXAMPLE

The following program produces the sum of N numbers 1, 2, ..., N.

  i := 0;
  sum := 0;
  while i < N
  do i := i + 1;
     sum := sum + i  end_do

We want to show that { sum = 0.5 i (i+1) } is an invariant. In order to show this, we need to prove the following:

  Pre-condition: { sum = 0.5 i (i+1) }
  do i := i + 1;
     sum := sum + i  end_do
  Post-condition: { sum = 0.5 i (i+1) }

In other words, the Pre-condition and the Post-condition are the same and therefore it is an invariant. Use backward substitution to prove it.