-- BAMS: purely functional specification (LSB, 2006)


types

BAMS = map AccId to Account;
Account :: H: set of AccHolder
           B: Amount
inv account == (not account.H = {} ) and account.B >= 0;

AccId     = seq of char;
AccHolder = seq of char;
Amount = int;


values

sis1 : BAMS = { "c1" |-> mk_Account({"Nuno"}, 50) };

sis2 : BAMS = { "c1" |-> mk_Account({"Nuno", "Joao"}, 80), 
                "c2" |-> mk_Account({"Candida"}, 250) };


functions

Init : () -> BAMS
Init () == {|->};


OpenAccount : BAMS * AccId * set of AccHolder * Amount -> BAMS
OpenAccount(bams, n, h, m) ==
      bams munion { n |-> mk_Account(h, m) }
pre not n in set dom bams;


AddAccHolders: BAMS * AccId * set of AccHolder -> BAMS
AddAccHolders(bams, n, h) ==
      bams ++ { n |-> let a = bams(n)
                      in mk_Account(a.H union h, a.B) }
pre n in set dom bams;


Credit: BAMS * AccId * Amount -> BAMS
Credit(bams, n, m) ==
      bams ++ { n |-> let a = bams(n)
                      in mk_Account(a.H, a.B + m) }
pre n in set dom bams;

Withdraw: BAMS * AccId * Amount -> BAMS
Withdraw(bams, n, m) ==
      bams ++ { n |-> let a = bams(n)
                      in mk_Account(a.H, a.B - m) }

pre (n in set dom bams and bams(n).B >= m);


GoodCostumers: BAMS * Amount -> set of AccId
GoodCostumers(bams, m) == { n | n in set dom bams & bams(n).B >= m } ;