MACHINE
  Library
SETS
  Book;
  Copy;
  Person
VARIABLES
  stock, 
  belongs_to,
  is_lent,
  lent_by
INVARIANT
  stock <: Copy &
  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:Copy & x/:stock
      THEN 
         belongs_to := belongs_to \/ {x|->b}
       || stock := stock \/ {x}
       || c := x
      END
    END
  ;
  lend(c,p) =
    PRE c:stock & p:Person & c/:is_lent
    THEN
       is_lent := is_lent\/{c}
     || lent_by := lent_by \/ {c|->p}
    END
END