Past exam of the year 1 of the computer science course of the University of Oxford / 2013 / Imperative programming / 1

Evaluate the mixed radix representation from its most significant end, using Horner's method. There is no need to compute the positional weights separately.

def digsToInt(xs: Array[Int], bs: Array[Int]): Int = {
  require(xs.length == bs.length)
  val N = xs.length
  var i = N
  var acc = 0
  while (i > 0) {
    i -= 1
    acc = xs(i) + bs(i) * acc
  }
  acc
}

The digit conditions

0 \leq x s (i) < b s (i)

are additional preconditions. The loop invariant at the loop test is

0 \leq i \leq N, a cc = \sum_{k = i}^{N - 1} x s (k) \prod_{j = i}^{k - 1} b s (j) .

(1)

An empty sum is zero and an empty product is one, so initialization at

i = N

is correct. For the next digit, writing

i^{'} = i - 1

gives

x s (i^{'}) + b s (i^{'}) a cc = \sum_{k = i^{'}}^{N - 1} x s (k) \prod_{j = i^{'}}^{k - 1} b s (j),

(2)

which preserves the loop invariant. The loop variant is

i

. At termination

i = 0

, giving

a cc = x s \otimes b s .

(3)

The code executes exactly

N

multiplications, meeting the bound, and uses

O (1)

auxiliary space. When

N = 0

it returns zero. For the time representation in the source, it computes

s + 60 (m + 60 h)

b

 0  0

Solution

 0  0

A suitable precondition, including the empty array case, is

b s (i) \geq 1 (0 \leq i < N), 0 \leq n < i = 0 \prod N - 1 b s (i) .

(1)

A base of one is allowed: its only valid digit is zero. The empty product is one, so

N = 0

permits exactly

n = 0

. Each Euclidean division extracts the next least significant digit.

def intToDigs(n: Int, bs: Array[Int]): Array[Int] = {
  // Pre: every base is positive, and 0 <= n < product(bs).
  val N = bs.length
  val xs = new Array[Int](N)
  var i = 0
  var q = n
  while (i < N) {
    xs(i) = q % bs(i)
    q = q / bs(i)
    i += 1
  }
  xs
}

The expensive precondition is a caller obligation, rather than a separately computed product inside the conversion. Define

P_{i} = \prod_{j = 0}^{i - 1} b s (j)

. The loop invariant is

0 \leq i \leq N, n = \sum_{k = 0}^{i - 1} x s (k) P_{k} + q P_{i}, 0 \leq q < \prod_{j = i}^{N - 1} b s (j),

(2)

together with

0 \leq x s (k) < b s (k)

for each processed digit. The Euclidean division identity

q = (q mod b s (i)) + b s (i) ⌊ q / b s (i)⌋

proves preservation of the reconstruction equality. Positivity of the bases gives the digit bounds and the next bound on the quotient. The loop variant is