Compare every unordered pair of distinct starting positions:
def longestRepeated(): (Int, Int, Int) = {
  require(N >= 2)
  var besti = 0
  var bestj = 1
  var bestk = 0
  var i = 0
  while (i < N - 1) {
    var j = i + 1
    while (j < N) {
      val k = longestFrom(i, j)
      if (k > bestk) {
        besti = i; bestj = j; bestk = k
      }
      j += 1
    }
    i += 1
  }
  (besti, bestj, bestk)
}
After each comparison, the stored triple attains the largest common-prefix length among pairs processed so far; its positions remain distinct. The nested while loops enumerate exactly pairs. Reversing the two positions does not change their common-prefix length, so no omitted ordered pair could improve the answer. Initialization also supplies a valid length-zero answer if no character repeats.
Write for the final maximal length. Each comparison takes time, including a possible first mismatch. Hence time is , at worst , and auxiliary space is . Writing merely would miss the case. The explicit precondition excludes arrays with fewer than two valid starting positions; the requested distinct-position triple has no answer there under this domain convention.
Use two finite integer lists , with the head of each list representing its stack top. Initially both are empty. A suitable abstract object interface is
trait DoubleStack {
  def pusha(x: Int): Unit
  def pushb(x: Int): Unit
  def popa: Int
  def popb: Int
  def isEmptya: Boolean
  def isEmptyb: Boolean
}
For the unbounded abstract data type, each push has no logical precondition. The postcondition of pusha(x) is and ; pushb(x) symmetrically gives and . The precondition of popa is , and its postcondition is return value , new state , and unchanged . The specification for popb exchanges . Each emptiness query leaves both lists unchanged and returns exactly whether its corresponding list is empty.
These frame conditions matter: an operation on one stack must preserve the other, not merely produce the right return value.
A fixed-capacity implementation needs a bounded contract: , and a push requires strict inequality. Pop preconditions and all successful-operation postconditions remain unchanged. An implementation that rejects full-array pushes cannot satisfy an unbounded specification promising every push; the capacity restriction must be part of the agreed abstract data type, or its resource-failure behavior must be specified.
Use one array and two boundaries left and right. The first stack occupies indices below left and grows rightwards; the second occupies indices at least right and grows leftwards. The representation invariant is
The abstraction function is
Both lists are top-first. The unoccupied middle interval has length right - left; a push is possible exactly when this is positive. Thus every array position can be used by either stack, avoiding a rigid half-array allocation.
Figure 1.
Original shared-array double-stack layout: two stacks grow towards a common free interval
. Details.
The implementation maintains the two boundaries from part b:
class ArrayDoubleStack(val MAX: Int) extends DoubleStack {
  require(MAX >= 0)
  private val data = new Array[Int](MAX)
  private var left = 0
  private var right = MAX

  def isEmptya: Boolean = left == 0
  def isEmptyb: Boolean = right == MAX

  def pusha(x: Int): Unit = {
    require(left < right, "double stack is full")
    data(left) = x
    left += 1
  }
  def pushb(x: Int): Unit = {
    require(left < right, "double stack is full")
    right -= 1
    data(right) = x
  }
  def popa: Int = {
    require(left > 0, "stack a is empty")
    left -= 1
    data(left)
  }
  def popb: Int = {
    require(right < MAX, "stack b is empty")
    val answer = data(right)
    right += 1
    answer
  }
}
Initialization gives empty abstract lists. Each push consumes one free position next to the appropriate top; each pop returns that top and releases its position. The guards preserve the ordering of the two boundaries and prevent invalid indexing. The abstraction function shows directly that the untouched stack is unchanged. Keeping data private prevents clients from violating the representation invariant; this strengthens encapsulation relative to a publicly exposed implementation field without changing the six required operations.
All six operations run in time, with a fixed array of MAX integers and constant extra state. Creating and zero-initializing the array takes time, outside those operation bounds. Capacity zero gives a valid always-empty bounded structure whose pushes fail their precondition.
The precondition is n != null and , using node identity rather than datum equality. Search for its predecessor:
def delete(n: Node): Unit = {
  var previous = bagHeader
  while (previous.next ne n) {
    previous = previous.next
  }
  previous.next = n.next
  n.next = null
}
The loop invariant states that previous is the header or a preceding real node, and . The loop variant is the number of links from previous to n minus one. The precondition guarantees that this search reaches the predecessor before a null dereference. Replacing its successor by n.next bypasses exactly the requested node; clearing the removed node's link detaches it for later reuse. The order and identities of every other node remain unchanged. In abstract terms, only the multiplicity of n.datum decreases, by one. The worst-case time is linear; the pointer modification itself is constant-time.
Check that at least one real node exists, then compose the two helpers:
def deleteMin(): Int = {
  require(bagHeader.next != null, "bag is empty")
  val smallest = findMin(bagHeader.next)
  val answer = smallest.datum
  delete(smallest)
  answer
}
The precondition check makes findMin applicable. Its result belongs to the real-node sequence, satisfying delete's precondition. Consequently one minimum value is returned and exactly one occurrence is removed; duplicates remain as distinct nodes. Saving the datum before deletion also separates the return value from subsequent link mutation. Two linear traversals still give time for a multiset containing nodes, with constant auxiliary space.
Find the entry once and check the abstract membership precondition on that result:
def recall(name: String): String = {
  val entry = find(name, table(hash(name)))
  require(entry != null, "name is not in the book")
  entry.number
}
The check turns an invalid call into an explicit precondition failure rather than an accidental null dereference or an invented default number. For a valid call, the unique matching entry contains exactly the mapped value, so the stored number is returned and the map is unchanged. Testing membership by calling isInBook first would traverse the same bucket twice; retaining the found reference avoids that redundant work.
Throw an informative exception, such as NoSuchElementException, and leave the set unchanged. This makes a violated nonempty precondition visible at the point of misuse. Returning a distinguished integer would be ambiguous because every integer is a legitimate set member.
A different object interface could return an optional integer, representing failure explicitly, but that changes the declared return type. For the supplied integer-returning operation, a checked failure is useful and consistent with the stated precondition.
The abstract data type invariant constrains a total count function on integer keys as follows:
The initial state has every count zero, and . These conditions make the abstract state a multiset supported on the allowed finite key range. Since the interface returns an Int, the implementations below use representable nonnegative multiplicities; equivalently add to the invariant, where . The corresponding add precondition below prevents overflow. An idealized unbounded-integer specification can omit that machine bound.
Write for the incoming state and . Use the following explicit contracts.
For add(x), the precondition is and . The postcondition is and for every .
For remove(x), the precondition is and . The postcondition is , with every other count unchanged. This convention rejects removal of an absent occurrence rather than silently treating it as a no-op.
For count(x), the precondition is . The result is and the whole abstract state is unchanged. Counts outside the allowed range are zero in the mathematical total function, but this chosen interface requires an in-range query.
Store the number of positive buckets, initially zero:
private var distinct = 0

def size: Int = distinct
Extend the representation invariant by
The abstraction function for the multiset is unchanged. The size operation has no precondition beyond a valid receiver; it returns the cardinality of the multiset support and changes no state. Replace the modifying methods inside the class by
def add(x: Int): Unit = {
  require(inRange(x))
  require(c(x) < Int.MaxValue)
  if (c(x) == 0) distinct += 1
  c(x) += 1
}

def remove(x: Int): Unit = {
  require(inRange(x))
  require(c(x) > 0)
  c(x) -= 1
  if (c(x) == 0) distinct -= 1
}
Only transitions from zero to one or from one to zero change the support. Additions to an already positive bucket and removals leaving it positive preserve distinct. Thus size takes time, independently of MAX, and the other operations retain constant-time array access. Initialization still takes time.
Use a finite sequence as abstract state, initially empty. One Scala interface is
trait DoubleEndedQueue {
  def isEmpty: Boolean
  def addLeft(x: Int): Unit
  def getLeft(): Int
  def addRight(x: Int): Unit
  def getRight(): Int
}
The emptiness query has no precondition; its result is and its postcondition is . Adding on the left has no precondition and gives . Adding on the right gives . Both return Unit.
Each removal requires a nonempty incoming sequence. getLeft() returns its first entry and leaves the remaining final sequence; getRight() returns its last entry and leaves the remaining initial sequence. These contracts remove exactly one occurrence, so duplicate values are permitted and do not collapse the sequence into a set.
Add this method inside the concrete class:
def display: Unit = {
  print("[")
  var current = first
  var separator = ""
  while (current != null) {
    print(separator)
    print(current.datum)
    separator = ", "
    current = current.next
  }
  println("]")
}
Its precondition is a valid receiver, including an empty one. Its postcondition leaves and prints the entries of from left to right in the displayed bracket format, followed by a newline. The loop invariant says that the printed entries are precisely the chain before current; the not-yet-printed entries are the chain starting there. Advancing along the acyclic chain terminates after its length. Printing changes the output stream, but it changes neither links nor payloads.
The missing preconditions are for insertion and for deletion and indexing. The inclusive endpoint permits appending; deletion or access at the length is invalid. Specify the initial state, for example , as well as the read-only frame conditions: indexing returns the indicated character and preserves , while length returns and preserves .
The insertion and deletion clauses already describe the new sequence, but their returned values and effects should be interpreted against the old state. For a machine-sized length, insertion also requires . These clauses complete the document abstract data type without prescribing one storage representation.
Reuse the machinery with the digit interval:
trait DigitCountPlugIn extends CharCountPlugin {
  override protected def firstCounted: Char = '0'
  override protected def numberCounted: Int = 10
}
Its count precondition is now '0' <= ch && ch <= '9'. It counts digits while permitting all characters to be stored. This is an alternative configured counter, rather than a second independent lowercase counter in the same object; simultaneous independent alphabets would require separate counters or a combined mapping.
Read and advance the cursor only when the iterator is asked for its next value:
def asIter[T](cur: Cursor[T]): Iter[T] = new Iter[T] {
  def hasNext: Boolean = cur.hasCurrent
  def next(): T = {
    require(cur.hasCurrent, "empty iterator")
    val answer = cur.current
    cur.next()
    answer
  }
}
The two abstract sequences are identical. A next call returns the old head and removes it, while hasNext only queries availability. No element is read at construction or during an availability test, and no later element is read while returning the current one. Thus the adapter is not too eager. The source's Cursor.current clause needs the implicit precondition that its sequence is nonempty; taking the head of an empty sequence is undefined. The checks above satisfy that requirement even without relying on the client convention.
Cache only a requested current element. Merely constructing the cursor, or asking whether it is nonempty, must not fetch a value from the iterator:
def asCursor[T](it: Iter[T]): Cursor[T] = new Cursor[T] {
  private var cached: Option[T] = None

  def hasCurrent: Boolean = cached.nonEmpty || it.hasNext

  def current: T = {
    if (cached.isEmpty) {
      require(it.hasNext, "empty cursor")
      cached = Some(it.next())
    }
    cached.get
  }

  def next(): Unit = {
    if (cached.nonEmpty) cached = None
    else {
      require(it.hasNext, "empty cursor")
      it.next()
      ()
    }
  }
}
The abstraction function for the adapter is it.seq when no value is cached and [cachedValue] ++ it.seq otherwise. Fetching current removes one underlying iterator value but saves it, so the cursor's abstract sequence is unchanged; repeated reads return the same value. Advancing either discards that cache or consumes one uncached iterator value. No following element is prefetched.
A too-eager implementation could call it.next() at construction, or fetch a new element immediately after every advance, even when the client never requests it. That can trigger unnecessary work or nontermination on a difficult stream. This lazy iterator-to-cursor adapter avoids both behaviors and checks the underlying access preconditions itself. The wrapped iterator is assumed to be used exclusively through the adapter; independent external consumption would invalidate the shared-state abstraction.
A complete multiset is a finite-support signed count function. An absent key has count zero; negative counts are allowed. One simple default implementation uses a protected immutable association list with unique keys and nonzero values. Its default is empty, and optimized subclasses may override the public queries.
trait CompleteMultiSet[T] {
  // Representation contract: finite, immutable, unique keys, nonzero counts.
  protected def entries: List[(T, Int)] = Nil

  def count(t: T): Int =
    entries.find { case (key, _) => key == t }.map(_._2).getOrElse(0)

  lazy val present: Seq[T] = entries.map(_._1)

  private def combine(other: CompleteMultiSet[T],
                      op: (Int, Int) => Int): CompleteMultiSet[T] = {
    val keys = (present.toList ++ other.present.toList).distinct
    val resultRows = keys.flatMap { t =>
      val n = op(count(t), other.count(t))
      if (n == 0) Nil else List((t, n))
    }
    new CompleteMultiSet[T] {
      override protected val entries: List[(T, Int)] = resultRows
    }
  }

  def +(other: CompleteMultiSet[T]): CompleteMultiSet[T] =
    combine(other, (a, b) => java.lang.Math.addExact(a, b))

  def -(other: CompleteMultiSet[T]): CompleteMultiSet[T] =
    combine(other, (a, b) => java.lang.Math.subtractExact(a, b))

  def max(other: CompleteMultiSet[T]): CompleteMultiSet[T] =
    combine(other, (a, b) => math.max(a, b))

  def min(other: CompleteMultiSet[T]): CompleteMultiSet[T] =
    combine(other, (a, b) => math.min(a, b))

  def <=(other: CompleteMultiSet[T]): Boolean =
    (present.toList ++ other.present.toList).distinct.forall { t =>
      count(t) <= other.count(t)
    }

  override def toString: String =
    present.distinct.filter(t => count(t) != 0)
      .map(t => s"$t:${count(t)}").mkString("{", ", ", "}")
}
The representation invariant and abstraction function assign the association-list value at a stored key and zero elsewhere. Every operation preserves both operands and returns a fresh immutable value. The finite-support pointwise operations principle makes the support union sufficient because every operation sends to zero. It is necessary for signed counts: the empty value is not at most a value having count at one key, although the empty left support alone would give a vacuous true comparison. Likewise, pointwise minimum can retain a negative count appearing only in the other operand.
present == List() represents the all-zero, empty complete multiset. The list-backed default count takes time for a first-entry hit or an empty list, and in the worst case for a missing or final key, assuming constant-cost key equality. The default binary operations can consequently take quadratic time; they are deliberately simple defaults, not optimized implementations. The lazy present avoids an early call to a subclass's representation during initialization.
Counts use Int, so addition and subtraction explicitly throw ArithmeticException when the mathematical result is unrepresentable instead of silently wrapping. Equivalently, their mathematical precondition requires representable result counts. This machine-size restriction is separate from permitting negative counts.
Nonnegative count functions form a valid subtype of the immutable value interface, but they are not closed under its exact subtraction. Preserve the inherited result type rather than silently changing the subtraction contract:
trait MultiSet[T] extends CompleteMultiSet[T] {
  // Additional invariant: count(t) >= 0 for every t.
  // Inherited arithmetic still returns CompleteMultiSet[T].
}

class MultiSetImp[T](initial: Map[T, Int])
    extends CompleteMultiSetImp[T](initial) with MultiSet[T] {
  require(initial.values.forall(_ >= 0), "negative multiplicity")
}

def ms[T](ts: T*): MultiSet[T] =
  new MultiSetImp[T](ts.distinct.map(t => (t, 1)).toMap)
The invariant guarantees nonnegative multiplicities in every MultiSet object, and the factory gives each supplied element exactly one occurrence. Since the objects are immutable, inherited operations cannot invalidate that invariant in the receiver. Their declared result is a complete multiset, which can legitimately contain negative counts; for example, subtracting a positive count from zero produces a signed result.
If an ordinary multiset-only difference is desired, introduce a separate operation with count , or an interface whose subtraction explicitly has that contract. Replacing the parent's exact difference by truncated difference under the same signature would violate behavioral subtyping; strengthening its precondition to forbid negative results would also fail to implement the parent's unrestricted mathematical contract. Retaining the complete result type above reuses every correct default without that substitution error.
The algorithmic intention is exponentiation by squaring to compute for . With exact arithmetic, its loop invariant is
Initially result = 1, y = x, and i = n. For an even integer , squaring y and replacing i by preserves the product. For an odd integer , first multiply result by y; then . The nonnegative loop variant i decreases by halving whenever positive. At exit , so the loop invariant yields result = x^n. There are multiplication steps.
Two qualifications are essential for the actual source. There is no requirement that n be nonnegative: for every n <= 0 the printed function simply returns 1.0. Also, var y = x infers Int, so y *= y uses wrapping integer arithmetic, while the accumulator uses floating-point arithmetic. For example, anotherfunc(50000, 2L) returns -1794967296.0, rather than 2500000000.0. An exact-power loop invariant cannot prove a false claim about that execution.
More precisely, for positive n, after iterations the remaining exponent is , and the Int base is the signed 32-bit representative of modulo . The accumulator multiplies those signed representatives for the set bits of n, in increasing bit order, with a floating-point rounding after each multiplication. This describes the actual code even when the intended power law fails. In an exact implementation, use a nonnegative-exponent precondition and arbitrary-precision integers, for example:
def powerExact(x: Int, n: Long): BigInt = {
  require(x > 0 && n >= 0)
  var result = BigInt(1)
  var y = BigInt(x)
  var i = n
  while (i > 0) {
    if (i % 2 == 1) result *= y
    y *= y
    i /= 2
  }
  result
}
The displayed loop invariant applies exactly to this version. It performs logarithmically many arbitrary-precision multiplications; their bit cost grows with operand size, so that statement is not an bit-complexity bound. Merely making the accumulator a Double does not widen the separate Int base variable.