= Solution
Every operation requires $u\in U$. The queries have <postconditions> “return $I_0(u)$” and “return $O_0(u)$” respectively, leaving both <functions> unchanged. An incoming increment additionally requires $I_0(u)<M$ and has
$$
I'(v)=\begin{cases}I_0(u)+1&v=u,\\I_0(v)&v\ne u,\end{cases}\qquad O'=O_0.
$$
The outgoing increment analogously requires $O_0(u)<M$, increments only $O(u)$, and preserves $I$. These frame conditions prevent an implementation from accidentally changing another user's count. Here a subscript zero denotes the old <program state>.
``
trait Payments {
// All methods require 1 <= user && user <= 99999999.
// Queries leave the abstract state unchanged.
def incoming(user: Int): Int
def outgoing(user: Int): Int
// Require the corresponding old count < Int.MaxValue.
// Increment only that user's named count by one.
def recordIncoming(user: Int): Unit
def recordOutgoing(user: Int): Unit
}
``
The <preconditions> and <postconditions> are part of the <formal specification>; the trait's <type signatures> alone cannot express all of them. The implementation below uses checked `require` calls for the relevant invalid operations.
Back to article page
