Algorithm and Program Correctness
=================================
Let's turn our reasoning about / and % into an algorithm.

  For all m, n in N, m > 0 ->
    -]q in N, -]r in N, n = qm + r /\ r < m

So for m, n in N with m > 0 there are q and r with a certain
 property. We'll just calcuate one of them: r.

  For m, n in N with m > 0,
   returns an r in N with r < m and n = qm + r for some q in N.

  remainder(n, m)
    r = n
    while r >= m
      r = r - m
    return r

So it starts with the r from n = 0m + n, and decreases it by m
 until it is < m.

Does it work?

Program Specifications
----------------------
A program specification is a Precondition and Postcondition.

We say that a program is correct with respect to the
 specification iff when the Precondition is true and the
 program is Executed, the program Terminates and the
 Postcondition is true:

  Pre /\ Execute -> Term /\ Post.

When talking about Term and Post we will always assume we've
 executed the program, so from now Execute will not be mentioned.
 So we consider it implicit in Pre -> Term /\ Post.

It may seem that similarly Term is an implicit part of Post,
 but we separate it out because it is something we need to remember
 to prove.

For remainder we have
  Pre: m, n in N, m > 0.
  Post: returns r in N with r < m and n = qm + r for some q in N.

Loop Invariants
---------------
To reason about remainder we need to reason about the loop in it.
We mentioned before how to deal with changing variables: index
 their values by the number of iterations so far.

A loop invariant decsribes what is true about all the values.
It describes what the loop is accomplishing, why the loop was
 written, why the loop is making progress towards Post (which
 is ultimately the point of it).

Students can find it hard to come up with, because:

  it is as hard and varied as programming itself,
   requiring the same creativity
  
  some students write their code by trial and error, without
   clear reasons

  someone else may have written the program

For remainder, we are counting down the remainders: so it should
 be that every r_k is a remainder.

For n in N let I(k) be:
  There is a q in N such that n = qm + r_k.

What if we don't actually have k iterations? We really should write
 I(k) as:

  If there are at least k iterations then there is a q in N
   such that n = qm + r_k.

We will prove the Loop Invariant:

  Pre -> \-/k in N, I(k)

We will prove "Partial Correctness":

  Pre /\ Term -> Post

But by the Loop Invariant we really only need to prove

  Pre /\ Term after iteration t /\ I(t) -> Post

And since Term(t) -> ~Condition(t) (where Condition is the
 loop condition), we only need to prove

  Pre /\ Term after iteration t /\ I(t) /\ ~Condition(t)
    -> Post

Finally we will prove Termination:

  [Pre /\ \-/k in N, I(k)] -> Term

Putting these together (consider it a CSC165 exercise), we will
 have proven Correctness: Pre -> Term /\ Post.

Since Pre is assumed in all of this, we will assume it implicitly
 from now on.

Partial Correctness
-------------------
Let's start with Partial Correctness, so we can see if the
 Invariant is strong enough for its purpose.

Suppose the program terminates after t iterations of the loop,
 with I(t) and ~Condition(t):

  So there is a q in N with n = qm + r_t.
  Also r_t < m.

  Since r_t = n - qm, r_t is in Z. But is it in N? I.e. is r_t >= 0?

  If t = 0, then r_t = n >= 0.
  If t > 0, then r_t = r_(t-1) - m, and since we had a tth iteration
   we had Condition(t-1) and so r_(t-1) >= m. Thus r_t >= 0.

  [We could also have taken the approach of putting r_k >=0 into
   the loop invariant.]

  Therefore Pre.

Loop Invariant
--------------
We proceed by induction.

Base Case: k = 0

  Then r_k = n = 0m + n, so q = 0 in N demonstrates I(0).

Inductive Step

  Let k in N and suppose I(k).

  Suppose there are at least k+1 iterations (hypothesis in I(k+1)).
  Then there are at least k iterations (hypothesis in I(k)).
  By the IH, n = qm + r_k for some q in N (conclusion in I(k)).

  The logic of the last three steps is always the same in loop
   invariant proofs, so we will leave it out from now on.
  Similarly, we won't do what I said we "really should" do,
   instead we will state our loop invariants without explicitly
   mentioning that we require a certain number of iterations.

  Now, r_(k+1) = r_k - m from the code, so r_k = r_(k+1) + m.
  Thus n = qm + r_(k+1) + m (using what we got from the IH)
         = (q+1)m + r_k+1, where q+1 in N since q in N.
  Thus I(k+1).

Termination
-----------
We make a Loop *Variant*: a natural number that decreases
 with each iteration.

We assume there are an infinite number of iterations,
 contradicting one of our inductive principlies, so the number
 of iterations must be finite.

The point of r is to decrease to the smallest value, so we use it.

Since r_(k+1) = r_k - m and Pre -> m > 0: r_(k+1) < r_k.
Thus the sequence of r_k's is decreasing.

Each r_k is an integer, since r_k = n - qm, with n, q, m in Z.
Since we are assuming an infinite number of iterations,
 Condition(k) is true for every k, so r_k >= m > 0.
Thus each r_k is a natural number.