% @(#)$Id: MutableMoneyHom.lsl,v 1.2 1997/07/31 20:59:42 leavens Exp $

MutableMoneyHom: trait
  assumes MutableMoneyTrait
  asserts
    \forall mm, mm1, mm2: MutableMoney, q: Q
      dollars(mm) == dollars(toMoney(mm));
      cents(mm) == cents(toMoney(mm));
      toMoney(money(q)) == money(q);
      toMoney(mm1 + mm2) == toMoney(mm1) + toMoney(mm2);
      toMoney(mm1 - mm2) == toMoney(mm1) - toMoney(mm2);
      toMoney(q * mm) == q * toMoney(mm);
      (mm1 > mm2) == toMoney(mm1) > toMoney(mm2);
      (mm1 < mm2) == toMoney(mm1) < toMoney(mm2);
      (mm1 >= mm2) == toMoney(mm1) >= toMoney(mm2);
      (mm1 <= mm2) == toMoney(mm1) <= toMoney(mm2);
      inRange(mm) == inRange(toMoney(mm));

[Index]

HTML generated using lcpp2html.