#include FFUN.cam

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

; STATE st: A->B*C

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

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

FUNC SELR(a:A):C
PRE a in dom(st)
RETURN p2(st[a]);

FUNC INS(a: A, b: B, c: C): VOID
PRE    ~(a in dom(st))
STATE  st <- st + [ a -> < b,c > ];