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

Helper type synonym

The imperative square-root algorithm, assuming non-negative x

   sqrt = 0                  -- set sqrt to 0
   i    = 1                  -- set i to 1, sum of j's so far
   j    = 1                  -- set j to be the first odd number i
   while i <= x              -- while the sum hasn't exceeded x yet
     sqrt = sqrt + 1              -- increase the sqrt
     j    = j + 2                 -- next odd number
     i    = i + j                 -- running sum of j's

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 be non-negative. 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: The sqrt squared must be less than or equal to x, and sqrt+1 squared must strictly exceed x.

Stability condition: Program must leave x unchanged.

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

The invariant is that at each iteration of the loop sqrt remains below or equal to the actual square-root, and i tracks the square of the next value. We also have that j is the sqrt'th odd value. Coming up with this invariant is not for the faint of heart, for details I would strongly recommend looking at Manna's seminal Mathematical Theory of Computation book (chapter 3). The j .> 0 part is needed to establish the termination.

The measure. In each iteration i strictly increases, thus reducing the differential x - i

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

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