The length of a longest repeated substring equals the maximum longest-common-prefix length over adjacent suffixes in lexicographic order. Suffixes beginning with a fixed string form a consecutive interval: a string outside that string prefix software class differs earlier or ends sooner, putting it strictly to one side. Two occurrences of a longest repeated substring therefore bound an interval in which every adjacent pair shares that string prefix. At least one adjacent pair attains its length, and no pair can exceed the global maximum. This proves the result even when occurrences overlap; a text with fewer than two suffixes needs a separate empty-result convention.
Longest common prefix 2026-10-25
The longest common prefix of two strings is the longest string that is a string prefix of both. Its length is the number of matching initial characters before the first mismatch or the end of a string. A direct scan maintains equality of the processed prefixes and takes time linear in that length plus one. For suffixes represented by indices in a shared array, no character copying is needed.
Scan the two suffixes until a mismatch or an endpoint:
def longestFrom(i: Int, j: Int): Int = {
  require(0 <= i && i <= N && 0 <= j && j <= N)
  var k = 0
  while (k < N - i && k < N - j && a(i + k) == a(j + k)) {
    k += 1
  }
  k
}
The loop invariant is and equality of the two array segments of length . The loop variant is , which decreases whenever the while loop runs. Short-circuit evaluation checks both bounds before indexing. On exit either a string suffix has ended or the next characters differ, so no longer common string prefix is possible. Thus the returned value is the longest common prefix length. Overlap is allowed: the code only reads the array, so the two matching segments need not occupy disjoint storage.
All suffixes beginning with a fixed string form an interval in lexicographic order. To see this, suppose two suffixes start with a string , while a string suffix between them fails to start with . At its first differing character it must be either smaller than both or larger than both; if it ends before does, it is smaller than both. Either possibility contradicts its position between them.
Now take a longest repeated substring . Its two occurrences are prefixes of two distinct suffixes. Every string suffix between them also begins with , so at least one adjacent pair in that interval has a common string prefix of length at least . A greater length would contradict maximality of . Therefore the maximum common-prefix length over adjacent sorted suffixes equals the longest repeated-substring length. If the maximum is zero, any adjacent pair still attains it. The argument does not assume nonoverlapping occurrences.
Figure 1.
Original suffix-array example for banana: an interval of suffixes shares the repeated prefix ana
. Details.
Reuse the verified longest-common-prefix scan, handling equality before scanning:
def before(i: Int, j: Int): Boolean = {
  require(0 <= i && i < N && 0 <= j && j < N)
  if (i == j) false
  else {
    val k = longestFrom(i, j)
    if (j + k == N) false
    else if (i + k == N) true
    else a(i + k) < a(j + k)
  }
}
There is no additional while loop: the helper's loop invariant is that the first k characters agree and both indices remain in bounds. If the second string suffix ends first, the first cannot precede it; if the first ends first, it is a proper string prefix and precedes the second. Otherwise the first mismatching characters decide lexicographic order. Distinct suffixes cannot both end after the same number of characters, since their lengths differ.
The i == j case ensures a strict comparator, returning false for a string suffix compared with itself, in constant time. For distinct suffixes its running time is , where is the longest repeated-substring length of the full array.
For a finite acyclic linked list define the node sequence, retaining software object identities, by
Then scan without changing any links:
def findMin(first: Node): Node = {
  require(first != null)
  var best = first
  var cursor = first.next
  while (cursor != null) {
    if (cursor.datum < best.datum) best = cursor
    cursor = cursor.next
  }
  best
}
At each while loop head, write . The loop invariant says is nonempty, best belongs to , and its datum is no larger than that of every node in . Initially contains only first; comparing the next node extends the processed string prefix and preserves minimality. The loop variant strictly decreases. At exit the whole list is processed, so the returned reference identifies a minimum node. Ties retain the earliest minimum. Time is linear in the number of nodes and auxiliary space is constant.
Let and describe the entry state. The postcondition is: the multiset is empty; the returned chain is sorted nondecreasingly; its node sequence is a permutation of . Thus it has exactly the original multiset of data and preserves all duplicates. Strict increase is impossible when the multiset contains repeated values.
def getAllSorted(): Node = {
  var head: Node = null
  var tail: Node = null
  while (bagHeader.next != null) {
    val nextSmallest = findMin(bagHeader.next)
    delete(nextSmallest)
    nextSmallest.next = null
    if (head == null) head = nextSmallest
    else tail.next = nextSmallest
    tail = nextSmallest
  }
  head
}
The loop invariant partitions the original node identities into the remaining multiset and the returned-prefix chain. The latter is sorted, its last node is tail, and every datum in it is no larger than every remaining datum. Selecting a minimum and appending that detached node preserves all these facts. The loop variant is the number of real nodes remaining in the multiset, decreasing by one. When it reaches zero the string prefix contains the entire original node set, proving the postcondition. An initially empty multiset returns null.
This is linked-list selection sort. Its time is in general, from successive scans of lengths , and it uses constant auxiliary space: it relinks original nodes instead of allocating a new node for each item.
Use null to indicate that the requested key is absent:
private def find(name: String, head: Entry): Entry = {
  var cursor = head
  while (cursor != null && cursor.name != name) {
    cursor = cursor.next
  }
  cursor
}
The loop invariant is that the skipped string prefix contains no entry with the requested name and cursor starts the unsearched string suffix of the unchanged bucket. Its remaining length is a loop variant. Short-circuit evaluation prevents accessing a null entry. On exit, either cursor is null and the whole bucket has been ruled out, or its name equals the key. No list links or stored numbers are modified. String comparison here uses value equality; node deletion elsewhere uses reference identity.
Selection sort 2026-10-24
Selection sort repeatedly chooses a minimum element from the unprocessed collection and moves it to the next output position. After each step the output string prefix is sorted and no larger than any remaining element. Repeated linear minimum scans give quadratic worst-case time. A linked list implementation can detach and append existing nodes using constant auxiliary space while preserving duplicate elements. The sorted result is nondecreasing, not strictly increasing when duplicates occur.