Yes: the mutable specification omits important state and frame clauses. Queries do not explicitly preserve the receiver, so an implementation could clear its state during
present, return an empty sequence, and satisfy the displayed coverage condition in the resulting state. Arithmetic does not explicitly preserve a distinct operand, so it could corrupt that operand as well as update the receiver. No initial value or independence requirement for copy is stated.The missing old-state annotation on the other operand is particularly serious under reference aliasing. If
other is the receiver, the printed addition equation becomes , which is impossible for a nonzero old count. Self-subtraction becomes rather than the intended zero; self-maximum admits arbitrarily increased counts. Specify instead, for every key,with both operands evaluated in their pre-states. Queries preserve all states; updates change only the receiver's abstract value and preserve a distinct operand; copy produces an independent snapshot of the argument's pre-state. Specify an empty initial state and checked representable arithmetic, or use unbounded counts.The fact that
present may contain duplicates or zero-count keys is not itself a violation: the printed condition expressly requires only a support-covering sequence. An implementation may strengthen this to an exact, duplicate-free support. Efficiency also needs a cost model or explicit bounds if it is to be a formal guarantee rather than an informal aspiration.Keep a private immutable hash-map value in a mutable variable. Each update computes a complete replacement from snapshots and commits it once; this handles self-aliasing and arithmetic failure without partially modifying the receiver.
class MultiSetVarImp[T] extends MultiSetVar[T] {
private var table = Map.empty[T, Int]
def count(t: T): Int = table.getOrElse(t, 0)
def present: Seq[T] = table.keys.toVector
def copy(other: CompleteMultiSet[T]): Unit = {
val saved = other.present.distinct.iterator
.map(t => (t, other.count(t))).filter(_._2 != 0).toMap
table = saved
}
private def snapshot(other: MultiSetVar[T]): Map[T, Int] =
other.present.distinct.iterator
.map(t => (t, other.count(t))).filter(_._2 != 0).toMap
private def update(other: MultiSetVar[T], op: (Int, Int) => Int): Unit = {
val left = table
val right = snapshot(other)
val keys = left.keySet ++ right.keySet
val builder = Map.newBuilder[T, Int]
keys.foreach { t =>
val n = op(left.getOrElse(t, 0), right.getOrElse(t, 0))
if (n != 0) builder += ((t, n))
}
val replacement = builder.result()
table = replacement
}
def +(other: MultiSetVar[T]): Unit =
update(other, (a, b) => java.lang.Math.addExact(a, b))
def -(other: MultiSetVar[T]): Unit =
update(other, (a, b) => java.lang.Math.subtractExact(a, b))
def max(other: MultiSetVar[T]): Unit =
update(other, (a, b) => math.max(a, b))
def min(other: MultiSetVar[T]): Unit =
update(other, (a, b) => math.min(a, b))
def <=(other: CompleteMultiSet[T]): Boolean = {
val left = table
(left.keySet ++ other.present).forall { t =>
left.getOrElse(t, 0) <= other.count(t)
}
}
}The representation invariant is a finite map of nonzero counts with no representation exposed to callers. The abstraction function adds implicit zero elsewhere.
getOrElse implements that default; keys enumerates stored keys; distinct removes repeated input support entries; toMap builds an independent immutable map; and the builder accumulates the next representation before it is assigned. The private immutable snapshots remain stable while the new state is computed.For self-addition, both snapshots contain the same old counts, so they double; self-subtraction yields empty support; self-max and self-min leave the value unchanged. A distinct operand is never assigned or mutated. An overflow exception during building occurs before the final assignment, so the receiver remains unchanged. These are instances of snapshot-before-update semantics.
Lookup is expected under standard hash assumptions. Enumerating
present takes for support size . Combining two instances of this implementation takes expected time and temporary storage, including snapshot construction. For an arbitrary argument implementation, add the costs of its count calls: copying a default list-backed complete multiset can require , whereas copying the hash-backed version is expected linear. No generic interface can guarantee another implementation's query cost. Inputs are assumed to have finite, complete support enumerations and stable counts during an operation; concurrent mutation would need a separate synchronization contract. Articles by others on the same topic
There are currently no matching articles.