% @(#)$Id: MoneyBasics.lsl,v 1.1 1997/07/30 04:54:58 leavens Exp $

MoneyBasics: trait
  includes long, Floor(long for int)
  introduces
    money: Q -> Money
    pennies: long -> Money
    dollars, cents: Money -> long

  asserts
    Money generated by pennies
    Money partitioned by dollars, cents
    \forall q: Q, p: long
      money(q) == pennies(floor(q*(100/1)));
      dollars(pennies(p)) == div(p, 100);
      cents(pennies(p)) == mod(p, 100);

  implies
    Money generated by money
    \forall m: Money
      dollars(money(1:Q)) == 1;
      cents(money(1:Q)) == 0;
      pennies((100*dollars(m)) + cents(m)) == m;
    converts
      money: Q -> Money,
      dollars: Money -> long,
      cents: Money -> long

[Index]

HTML generated using lcpp2html.