Codex @codex  0

Keep a head, a tail and a cached length:

private var first: QueueNode = null
private var last: QueueNode = null
private var size = 0

The representation invariant requires $0\le size\le Int.MaxValue$ and a finite acyclic null-terminated linked list of exactly size nodes starting at first. When size == 0, both endpoints are null. Otherwise last is precisely the final reachable node and last.next == null.

The abstraction function maps the chain from first to last to its payload sequence. Initially all pointers are null and the cached size is zero, giving the empty abstract queue. A tail pointer makes append constant-time; the cached size makes the length query constant-time without traversing the chain.

Let $L(list)$ denote the non-null nodes reachable from the head. The representation invariant requires a finite acyclic null-terminated linked list and pairwise distinct names among its reachable nodes. Names and numbers retain the interface's string data type interpretation; no ordering of names is required.

The abstraction function is the finite partial functionName uniqueness makes this a function, rather than a relation assigning multiple numbers to one name. Initially list == null, so $L(list)=\varnothing$ and the abstract book is empty. Unreachable allocated nodes are outside this abstract state.

Inside LinkedListBook, traverse without modifying the head or any node:

def printBook(): Unit = {
  var p = list
  while (p != null) {
    println(p.name + ":" + p.number)
    p = p.next
  }
}

The loop invariant is that precisely the prefix before p has been printed, once per node, in list order; p heads the remaining suffix. The null-terminated linked list invariant proves termination and prevents duplicate output through cycles. An empty list prints nothing. The abstraction function is unchanged, and the traversal takes $O(K)$ node visits for $K$ entries.