= Solution
For each row, keep the <row run length> of the processed prefix. A false entry resets the length to zero; a true entry extends it by one.
``
val rowCount = Array.ofDim[Int](N, N)
var i = 0
while (i < N) {
var j = 0
var run = 0
while (j < N) {
if (a(i)(j)) run += 1 else run = 0
rowCount(i)(j) = run
j += 1
}
i += 1
}
``
The outer <loop invariant> states that rows before `i` have all their correct <row run lengths>. The inner <loop invariant> states that columns before `j` in row `i` are correct and that `run` is the length of the all-true suffix of `a(i)[0..j)`. Initially this suffix is empty. Updating `run` gives exactly the suffix length ending at column `j`, proving the required formula, including zero at a false entry. Every cell is visited once:
$$
\boxed{\mathrm{rowCount}(i)(j)=\begin{cases}0,&\neg a(i)(j),\\1+\mathrm{rowCount}(i)(j-1),&a(i)(j),\end{cases}\qquad O(N^2),}
$$
where the fictitious value at column $-1$ is zero. The table itself uses $O(N^2)$ storage.
Back to article page
