REFINEMENT
  LibraryR1
REFINES
  Library
VARIABLES
  stock,
  belongs_to,
  lent_by
INVARIANT
  1=1
INITIALISATION
  stock,belongs_to := {},{} ||
  lent_by := {}
OPERATIONS
  c <-- add_book(b) =
    ANY
      x
    WHERE 
      x:NATURAL & x/:stock
    THEN 
       belongs_to := belongs_to \/ {x|->b}
     || stock := stock \/ {x}
     || c := x
    END
  ;
  status <-- lend(c,p) =
    IF c/:dom(lent_by)
    THEN
         lent_by := lent_by \/ {c|->p}
      || status := ok
    ELSE
      status := is_already_lent
    END
END