Given an integer x >= 0, the integer square root of x is the greatest integer i satisfying i * i <= x. An implementation of the integer square root function is given as follows based on the method of binary search:
fun isqrt ( x: int ) : int = let // fun search ( x: int, l: int, r: int ) : int = let val diff = r - l in case+ 0 of | _ when diff > 0 => let val m = l + (diff / 2) in // x < m * m can overflow easily if x / m < m then search(x, l, m) else search(x, m, r) // end of [if] end // end of [if] | _ (* diff <= 0 *) => l (* the result is found *) end // end of [search] // in search(x, 0, x) end // end of [isqrt]
l * l <= x and x <= r * r must hold when search(x, l, r) is called.
Assume l * l <= x < r * r for some integers x, l, r. If a recursive call search(x, l1, r1) for some integers l1 and r1 is encountered in the body of search(x, l, r), then r1-l1 < r-l must hold. This invariant implies that search is terminating.
fun isqrt {x:nat} ( x: int x ) : int = let // fun search {x,l,r:nat | l < r} .<r-l>. ( x: int x, l: int l, r: int r ) : int = let val diff = r - l in case+ 0 of | _ when diff > 1 => let val m = l + half(diff) in if x / m < m then search(x, l, m) else search(x, m, r) // end of [if] end // end of [if] | _ (* diff <= 1 *) => l (* the result is found *) end // end of [search] // in if x > 0 then search(x, 0, x) else 0 end // end of [isqrt]
By being precise and being able to enforce precision effectively, the programmer will surely notice that his or her need for run-time debugging is diminishing rapidly.