MACHINE
  Library
SETS
  Book;
  Person;
  STATUS = {ok,is_already_lent}
VARIABLES
  stock,
  belongs_to,
  is_lent,
  lent_by
INVARIANT
  stock <: NATURAL &
  belongs_to : stock --> Book &
  is_lent <: stock &
  lent_by : is_lent --> Person
INITIALISATION
  stock,belongs_to := {},{} ||
  is_lent := {} ||
  lent_by := {}
OPERATIONS
  c <-- add_book(b) = 
    PRE b:Book THEN
      ANY
        x
      WHERE 
        x:NATURAL & x/:stock
      THEN 
         belongs_to := belongs_to \/ {x|->b}
       || stock := stock \/ {x}
       || c := x
      END
    END
  ;
  status <-- lend(c,p) =
    PRE c:stock & p:Person
    THEN
      IF c/:is_lent THEN
         is_lent := is_lent\/{c}
       || lent_by := lent_by \/ {c|->p}
       || status := ok
      ELSE
         status := is_already_lent
      END
    END
END