= Solution
\b[`start == null` if and only if `end == null`.] Otherwise there is a finite list of distinct <software objects> $v_0,\ldots,v_{m-1}$, with `start eq v0`, `end eq v(m-1)`, `v0.left == null`, and `v(m-1).right == null`. For every valid adjacent pair, `v(i).right eq v(i+1)` and `v(i+1).left eq v(i)`. These are exactly the entries reachable through the list links, so there is no extra cycle or branch. All counts are positive, all words are non-null, and words strictly increase from `start` to `end`.
This is the <representation invariant> for a null-terminated <doubly linked list> without a <list header>. The <abstraction function> reads the ordered word-count pairs from left to right. Conversion additionally requires the output entries, counts and words to be precisely those of the input <binary search tree>; that preservation property is an operation <postcondition>, rather than an invariant of an arbitrary list by itself.
Back to article page
