Past exam of the year 1 of the computer science course of the University of Oxford / 2014 / Imperative programming / 4 / b / Solution

The representation invariant is $N\ge 0$, rows.length == N, and every rows(i) is a nonnull finite list of entries $(j,x)$ satisfyingStrict increase excludes repeated columns. The abstraction function gives $A_{ij}=x$ when the unique entry $(j,x)$ occurs in rows(i), and $A_{ij}=0$ otherwise. Thus omitted positions represent zero; omission does not mean an unknown matrix entry.