¹The proper specification of crediting the interest of an account should require the introduction of a real-time attribute in account objects. The interested reader may look at [105, 107] for a general methodology to specify real-time systems, including object-oriented ones, in rewriting logic.