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

STATE st: A->B;

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

FUNC INIT()
STATE st <- [];

FUNC INS(a:A,b:B)
PRE a notin dom(st)
STATE st <- st + [a->b];

FUNC REM(a:A)
STATE st <- st \ {a};

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

FUNC EMPTY():Bool
RETURN st == [];