#include FFUN.cam

; Creation date: Thu Dec 11 19:55:23 WET 1997

STATE st: A->B-set;

FUNC JOIN(a: A, b: B): VOID
STATE  st <- st + [ a -> { b} U (if a in dom(st) then st[a] else {}) ];

FUNC LEAVE(a: A, b: B): VOID
PRE    a in dom(st)
STATE  st <- st + [ a -> st[a]  - { b } ];