VDM++

class Account

instance variables
  cards : map Card`CardId to Cardholder;
  balance : nat;
  transactions : seq of Transaction := [];

  inv TransactionsInvariant(transactions);

values
  dailyLimit : nat = 2000;

types
  public AccountId = nat;
  public Transaction :: date : Clock`Date
                 cardId : Card`CardId
                 amount : nat;

operations
  ValidTransaction : Transaction ==> bool
  ValidTransaction(transaction) ==
    is not yet specified;

public Create : map Card`CardId to Cardholder * nat ==> Account
  Create(cs,b) ==
    (cards := cs;
     balance := b;
     return self);

  public GetBalance : () ==> nat
  GetBalance() ==
    return balance;

  public Withdrawal : Card`CardId * nat * Clock`Date ==> bool
  Withdrawal(cardId,amount,date) ==
    let transaction = mk_Transaction(date,cardId,amount)
    in
      if balance - amount >= 0 and
         DateTotal(date,transactions^[transaction]) <= dailyLimit
      then
       (balance := balance - amount;
        transactions := transactions ^ [transaction];
        return true)
      else
        return false
  pre cardId in set dom cards;

  public MakeStatement : Card`CardId * Clock`Date ==> Letter
  MakeStatement(cardId,date) ==
    let nm = cards(cardId).GetName(),
        addr = cards(cardId).GetAddress()
    in
      (dcl letter : Letter := new Letter();
       letter.Create(nm,addr,date,transactions,balance))
  pre cardId in set dom cards;

  public GetCardIds: () ==> set of Card`CardId
  GetCardIds() ==
    return dom cards;

  public AddCard : Card`CardId * Cardholder ==> ()
  AddCard(cId,ch) ==
    cards := cards munion {cId |-> ch}
  pre cId not in set dom cards;

  public RemoveCard : Card`CardId ==> ()
  RemoveCard(cId) ==
    cards := {cId} <-: cards
  pre cId in set dom cards;

functions
  TransactionsInvariant: seq of Transaction +> bool
  TransactionsInvariant(ts) ==
    forall date in set {ts(i).date | i in set inds ts} &
      DateTotal(date,ts) <= dailyLimit;

  DateTotal : Clock`Date * seq of Transaction +> nat
  DateTotal(date,ts) ==
    Sum([ts(i).amount | i in set inds ts & ts(i).date = date]);

  Sum: seq of real +> real
  Sum(rs) ==
    if rs = [] then 0
    else
      hd rs + Sum(tl rs);

end Account