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

TYPE

S = A-list;
A = ANY;

ENDTYPE

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

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

FUNC TOP():Bool
PRE st != <>
RETURN hd(st);

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