#include SEQ.cam
;--------------------------------------------------------------------
; RSC-REPOSITORY                                             FLIST/96
;--------------------------------------------------------------------
;                         Copyright@1996 by F. Luis Neves
;
; Author(s):              JNO (Jose N. Oliveira), FLN (F. Luis Neves)
; Revisions:              25.Mar.96 Rev: 
;                                   Rev:
;
;--------------------------------------------------------------------
;
;
; Comments: Finite List Component
; 
; (a) Filiation: FLIST < RSC
; (b) Interface:
;                        -----------
;                       |           |
;             INIT ---> |           | TEST(A):Bool --->
;                       |           |
;           INS(A) ---> |   FLIST   |
;                       |           |
;            <--- GET:A |           | <--- REM(A)
;                       |           |
;                        -----------
;
; (c) State: S = A-list
; (d) Model:
;
;--------------------------------------------------------------------
;

TYPE

S = A-list;
A = ANY;

ENDTYPE

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

FUNC INS(a:A)
STATE st <- cons(a,st);

FUNC REM(a:A)
STATE st <- < x | x <- st : neq(x,a) > ;

FUNC TEST(a:A):Bool
RETURN a in elems(st);

FUNC GET():Bool
PRE st != <>
RETURN head(st)
STATE st <- tail(st);