Every operation requires . The queries have postconditions “return ” and “return ” respectively, leaving both functions unchanged. An incoming increment additionally requires and hasThe outgoing increment analogously requires , increments only , and preserves . 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. Articles by others on the same topic
There are currently no matching articles.