Past exam of the year 1 of the computer science course of the University of Oxford / 2005 / Functional programming, data structures and algorithms, procedural programming, and digital hardware / 8 / a / Solution

Use an Oberon record containing an active coefficient count and a bounded array of coefficients in ascending power order. A count of zero represents the zero polynomial; a count $n+1$ represents $a_0+\cdots +a_n{x}^n$. Trailing zero coefficients are allowed, so the count need not be the degree of a polynomial plus one.

CONST Capacity = 1024;
TYPE Polynomial = RECORD
  len: INTEGER;
  coeff: ARRAY Capacity OF REAL
END;

PROCEDURE Horner(VAR p: Polynomial; x: REAL): REAL;
  VAR i: INTEGER; value: REAL;
BEGIN
  i := p.len; value := 0.0;
  WHILE i > 0 DO
    i := i-1;
    value := p.coeff[i] + x*value
  END;
  RETURN value
END Horner;

The representation invariant is $0\le \text{len}\le \text{Capacity}$, with only indices below len significant. The parameter is passed by reference to avoid a full record copy; the procedure does not modify it.

Let $L$ be the original coefficient count. At each guard test the loop invariant isThe empty sum is zero initially. If the old index is $i>0$, after decrementing and updating,which preserves the loop invariant. The loop variant is $i$, decreasing by one until zero. At exit,This is exactly the right-to-left nesting of Horner's method, matching the supplied right fold. It uses $O(L)$ arithmetic operations and $O(1)$ additional scalar storage. REAL gives ordinary floating-point evaluation; the displayed identities specify the ideal arithmetic calculation, with the usual rounding in an actual floating-point implementation.