TYPE 
Bag = Item -> Nat;
Item = STR;
Nat = INT;
AddressDB = User -> System-list;
System = Machine | Network;
Network :: N:System-list;
Machine :: Id:STR  T:MachineType;
MachineType = STR;
User = STR;
Table = MachineType -> Nat;
Nat = INT;
ENDTYPE

FUNC  BagIns (i:Item, n:Nat, b:Bag) : Bag
RETURNS  let (x = f(i,b)) 
         in  b + [i -> (n .+ x)];

f(i,b) = if (i in dom(b)) then b[i] else 0;


FUNC  BagRmv (i:Item, n:Nat, b:Bag) : Bag
PRE  i in dom(b)  /\  n <= b[i] 
RETURNS  if ( i in dom(b)  /\  n == b[i]  -> b\{i},
              i in dom(b)  /\  n < b[i]  -> b + [i -> (b[i] .- n)]  );

FUNC  BagRep (i:Item, b:Bag) : Nat
RETURNS  if ( i in dom(b) -> b[i],
              i notin dom(b) -> 0  );

FUNC  BagUni (b:Bag, c:Bag) : Bag
RETURNS  b\dom(c) + c\dom(b) + [x -> b[x] .+ c[x] | x <- dom(b) * dom(c)];

FUNC  BagMul (n:Nat, b:Bag) : Bag
RETURNS   [x -> n .* b[x] | x <- dom(b)];

FUNC  BagUNION (bs:Bag-set) : Bag
RETURNS   BagUni-orio([],bs);


FUNC MachinesByUser (u:User) : Table
PRE  u in dom(A)
RETURNS  BuildTable(A[u]);

FUNC BuildTable(l:System-list) : Table
;STATE h <- pp(l)
RETURNS if ( l == <>   ->  [],
             l != <>   -> 
               if ( is-Machine(hd(l)) -> BagIns(T(hd(l)),1,BuildTable(tl(l))),
                    is-Network(hd(l)) -> 
                     if ( N(hd(l)) == <> -> BuildTable(tl(l)),
                          N(hd(l)) != <> -> BagUni(BuildTable(N(hd(l))),BuildTable(tl(l)))
                        )
                   )
             );
 

a <- ["aa" -> 8, "bb" -> 6, "cc" -> 3];
b <- ["aa" -> 2, "dd" -> 6];
N2 <- Network(<Machine("a7","t5"),Machine("a5","t2"),Machine("a5","t2"),Machine("a8","t3")>);
N1 <- Network(<Machine("a1","t1"),N2>);
A <- ["luis" -> <Machine("a1","t1"),Machine("a5","t2"),N1,Machine("a2","t5")>,
      "lsb" -> <Machine("a1","t1"),Network(<Machine("a1","t1")>),Machine("a5","t2"),Machine("a2","t5")>,
       "jj" -> <N1,Machine("a1","t1"),N2> ,
       "jno" -> <>,
       "prh" -> <N2>];