class System

instance variables

private Purses: map Purse`CardId to Purse;
inv forall p in set dom Purses & Purses(p).GetCardNo() = p;
private Log: seq of Transaction := [];

types

public Transaction :: 
         fromId : Purse`CardId
         toId   : Purse`CardId
         sum    : nat;

operations

public Transfer: Purse`CardId * Purse`CardId * nat ==> ()
Transfer(fromId, toId, sum) == 
( Purses(fromId).DecreaseBal(sum);
  Purses(toId).IncreaseBal(sum);
)
pre {fromId, toId} subset dom Purses and 
    fromId <> toId and
    Purses(fromId).GetBalance() >= sum;

public System: set of Purse ==> System
System(PurseSet) ==
  Purses := {p.GetCardNo() |-> p | p in set PurseSet}
pre forall p,q in set PurseSet & p <> q => p.GetCardNo() <> q.GetCardNo();

public TotalTransferred:() ==> nat
TotalTransferred() == 
  return TotalSum(Log);

functions

TotalSum: seq of Transaction -> nat
TotalSum(tseq) ==
  if tseq = [] 
  then 0
  else let tx = hd tseq 
       in 
         tx.sum + TotalSum(tl tseq)
measure Len;

Len: seq of Transaction -> nat
Len(l) ==
  len l;

end System