types

BAMS = map AccId to Account
inv x == forall mk_Account(h,a) in set rng x &
         card h > 0 and a >= 0;

Account :: H: set of AccHolder
           B: Amount;

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

values

ac1 = mk_Account({"paulo"}, 1000);
ac2 = mk_Account({"tiago", "paulo"}, 2000);

banco = { "1" |-> ac1, "2" |-> ac2 }


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) and card h > 0;

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 (let mk_Account(-, a) = bams(n) in m <= a);

GoodCostumers: BAMS * Amount -> set of AccId
GoodCostumers (bams, m) ==
        { c | c in set dom bams & let mk_Account(-, a) = bams(c) in a > m }