; ENROLLMENT CONTROL SYSTEM
; version 1        92.10.27

; -------------------------------------------------------------------- 
; SORTS
; -------------------------------------------------------------------- 

TYPE
  Course = SId -> Inf;
  SId = STR;
  Inf = [Mark];
  Mark = INT;
ENDTYPE

; -------------------------------------------------------------------- 
; FUNCTIONS
; -------------------------------------------------------------------- 

FUNC DefineCourse () : Course
RETURNS [];


FUNC InsStu (n:SId,c:Course) : Course
PRE  n notin dom(c)  
RETURNS  c + [n -> nil];


FUNC InsMark (n:SId,p:Mark,c:Course) : Course
PRE  n in dom(c)  
RETURNS  c + [n -> p];


FUNC RemStu (n:SId,c:Course) : Course
PRE  n in dom(c)  
RETURNS  c\{n};


FUNC Vacancies (c:Course) : INT
RETURNS  50 .- #(dom(c));


FUNC PosMark (c:Course) : SId-set 
PRE  all(x <- dom(c) : is-Mark(c[x]))   
RETURNS  { x | x <- dom(c) : c[x] >= 10};


FUNC DidBetter (c:Course,m:Mark) : SId-set 
PRE  all(x <- dom(c) : is-Mark(c[x]))  -> "Sorry: Marks not yet available"   
RETURNS  { x | x <- dom(c) : c[x] >= m};


FUNC MinMark (c:Course) : SId-set
PRE  all(x <- dom(c) : is-Mark(c[x]))   
RETURNS  let (mc = m-orio(999,ran(c)))
         in  {x | x <- dom(c) : c[x] == mc};

m(a,b) = if (a<b) then a else b;

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