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

Start with a one-cell, possibly unnormalized representation, then carry:

function MakeNum(t: integer): number
    require t >= 0
    new(result, 1)
    result[0] := t
    Normal(result)
    return result

Before normalization its represented value is exactly t. Carry normalization of a digit array preserves that value and grows storage when needed. Zero returns a valid nonempty representation containing zero. A negative input is outside this nonnegative-number abstraction.