Repeated integer division by two generates the binary digits from least significant to most significant. Reverse the accumulated characters once, and treat zero separately.
def binaryCon(n: Int): String = {
require(n >= 0, "n must be nonnegative")
if (n == 0) return "0"
var remaining = n
val digits = new StringBuilder
while (remaining > 0) {
digits.append(if (remaining % 2 == 0) '0' else '1')
remaining /= 2
}
digits.reverse.toString
}Zero produces
"0"; positive inputs produce a binary number without leading zeros. No library routine performs the number-to-base conversion. Appending to the builder and reversing once gives linear work in the number of binary digits and uses that much output storage.Validate the complete input before doing the addition. The arrays use most-significant-digit-first positional notation. The result has one extra leading position, which contains either zero or the final carry.
def binaryAddition(x: Array[Int], y: Array[Int]): Array[Int] = {
require(x != null && y != null, "arrays must not be null")
require(x.length == y.length, "lengths must match")
val n = x.length
var k = 0
while (k < n) {
require((x(k) == 0 || x(k) == 1) &&
(y(k) == 0 || y(k) == 1), "digits must be 0 or 1")
k += 1
}
val answer = new Array[Int](n + 1)
var carry = 0
var j = n - 1
while (j >= 0) {
val column = x(j) + y(j) + carry
answer(j + 1) = column % 2
carry = column / 2
j -= 1
}
answer(0) = carry
answer
}A failed
require throws IllegalArgumentException, covering mismatched lengths, invalid binary digits and null arrays. The largest column sum is three, so the carry always lies in . The binary-addition carry invariant says that the already processed input suffixes equal the written result suffix plus the carry shifted to the next column. After the final column, placing that carry at position zero proves the returned value is the sum. Neither input array is modified. Equal empty inputs are accepted as zero and return Array(0); the specification imposes no positive-length restriction. Running time and result storage are .Under exact integer arithmetic, the intended result is , using the ceiling function. A sufficient loop invariant isInitially , and the final disjunction is true. If the guard holds, the old value is below . Incrementing
i and doubling y therefore preserves and makes the new lower bound true. At exit . If , positivity of forces ; otherwise . Both cases establish the claimed postcondition. Doubling eventually reaches or exceeds any fixed positive , proving algorithm termination in this arithmetic model. This is the doubling-loop ceiling logarithm argument.The printed Scala implementation is not correct for its entire stated
Int domain. Its y is an Int. For , it reaches , wraps to on the next doubling, then becomes zero and stays zero. The guard remains true forever. The loop invariant above is valid for the printed code only when . Scala documents Int as a signed 32-bit value equivalent to Java's primitive int.[ref]A corrected implementation for every positive
Int input widens the doubling variable before any multiplication:def ceilingLog2(x: Int): Int = {
require(x > 0)
var i = 0
var y = 1L
while (y < x.toLong) {
i += 1
y *= 2L
}
i
}Now at most 31 iterations are needed and , safely within
Long. The same loop invariant proves total correctness without the overflow gap.The algorithmic intention is exponentiation by squaring to compute for . With exact arithmetic, its loop invariant isInitially
result = 1, y = x, and i = n. For an even integer , squaring y and replacing i by preserves the product. For an odd integer , first multiply result by y; then . The nonnegative loop variant i decreases by halving whenever positive. At exit , so the loop invariant yields result = x^n. There are multiplication steps.Two qualifications are essential for the actual source. There is no requirement that
n be nonnegative: for every n <= 0 the printed function simply returns 1.0. Also, var y = x infers Int, so y *= y uses wrapping integer arithmetic, while the accumulator uses floating-point arithmetic. For example, anotherfunc(50000, 2L) returns -1794967296.0, rather than 2500000000.0. An exact-power loop invariant cannot prove a false claim about that execution.More precisely, for positive
n, after iterations the remaining exponent is , and the Int base is the signed 32-bit representative of modulo . The accumulator multiplies those signed representatives for the set bits of n, in increasing bit order, with a floating-point rounding after each multiplication. This describes the actual code even when the intended power law fails. In an exact implementation, use a nonnegative-exponent precondition and arbitrary-precision integers, for example:def powerExact(x: Int, n: Long): BigInt = {
require(x > 0 && n >= 0)
var result = BigInt(1)
var y = BigInt(x)
var i = n
while (i > 0) {
if (i % 2 == 1) result *= y
y *= y
i /= 2
}
result
}The displayed loop invariant applies exactly to this version. It performs logarithmically many arbitrary-precision multiplications; their bit cost grows with operand size, so that statement is not an bit-complexity bound. Merely making the accumulator a
Double does not widen the separate Int base variable.To preserve the actual printed function, including its handling of nonpositive exponents and wrapping
Int bases, use a tail-recursive accumulator with the same multiplication order:def anotherfuncRec(x: Int, n: Long): Double = {
require(x > 0)
@scala.annotation.tailrec
def loop(y: Int, i: Long, result: Double): Double = {
if (i <= 0) result
else {
val nextResult = if (i % 2 == 1) result * y else result
loop(y * y, i / 2, nextResult)
}
}
loop(x, n, 1.0)
}Each recursive call corresponds to one source iteration and carries exactly its next program state. Hence it reproduces the printed numerical behavior, rather than silently repairing it. For positive
n, both routines use steps; for nonpositive n, both take constant time. The recursive call is in tail position, so Scala's tail-call optimization avoids a growing call stack; the annotation asks the compiler to check that condition.If the intended exact power is required instead, change the base and accumulator parameters of this same recurrence to
BigInt and require n >= 0, as in part (d). Its mathematical loop invariant becomes a recursion invariant, with the same logarithmic number of multiplication steps. Articles by others on the same topic
There are currently no matching articles.