#include FFUN.cam
;--------------------------------------------------------------------
; RSC-REPOSITORY                                              QFUN/96
;--------------------------------------------------------------------
;                         Copyright@1996 by F. Luis Neves
;
; Author(s):              FLN (F. Luis Neves)
; Revisions:              22.Fev.96 Rev: 
;                                   Rev:
;
;--------------------------------------------------------------------
;
;
; Comments: Quocient Function Component
; 
; (a) Filiation: QFUN < FFUN
; (b) Interface:
;                        ------------
;             INIT ---> |            |
;                       |            | EMPTY:Bool --->
;       INS(A,B,C) ---> |            |
;                       |    QFUN    | <--- DEL(A,B)
;      <--- FIND(A,B):C |            |
;                       |            | <--- REM(A)
;      <--- GET(A):B->C |            |
;                        ------------
;
; (c) State:

STATE st: A -> (B -> C);

; (d) Model:
;
;--------------------------------------------------------------------
;

TYPE

S = A -> (B -> C);
A = ANY;
B = ANY;
C = ANY;

ENDTYPE

;--------------------------------------------------------------------
;

FUNC INS(a:A,b:B,c:C):VOID
PRE if a in dom(st) then b notin dom(st[a]) else true
STATE st <- if (a notin dom(st) -> st + [a -> [b -> c]])
           otherwise (st + [a -> st[a] + [b->c]]);

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

FUNC REM(a:A)
PRE st[a] == []
STATE st <- st \ {a};

FUNC FIND(a:A,b:B):C
PRE a in dom(st) && b in dom(st[a])
RETURN st[a][b];