The state for the division program, parameterized over a base type a.

Helper type synonym

The imperative division algorithm, assuming non-negative x and strictly positive y:

   r = x                     -- set remainder to x
   q = 0                     -- set quotient  to 0
   while y <= r              -- while we can still subtract
     r = r - y                    -- reduce the remainder
     q = q + 1                    -- increase the quotient

Note that we need to explicitly annotate each loop with its invariant and the termination measure. For convenience, we take those two as parameters for simplicity.

Precondition for our program: x must non-negative and y must be strictly positive. Note that there is an explicit call to abort in our program to protect against this case, so if we do not have this precondition, all programs will fail.

Postcondition for our program: Remainder must be non-negative and less than y, and it must hold that x = q*y + r:

Stability: x and y must remain unchanged.

A program is the algorithm, together with its pre- and post-conditions.

The invariant is simply that x = q * y + r holds at all times and r is strictly positive. We need the y > 0 part of the invariant to establish the measure decreases, which is guaranteed by our precondition.

The measure. In each iteration r decreases, but always remains positive. Since y is strictly positive, r can serve as a measure for the loop.

Check that the program terminates and the post condition holds. We have:

>>> correctness
Total correctness is established.
Q.E.D.