貸出操作スキーマ
今回は，操作スキーマを定義する．これまでのデータスキーマは，時間によって変化しないものを示している．操作スキーマが与えるのは，操作による動的な変化である．
貸出操作（CheckOut）スキーマ
操作スキーマでも，既に定義しているデータスキーマを利用することができる．但し，先頭に新たな記号が付くことになる．∆は，操作によってスキーマ中の状態が変化することを示している．
例を見てみよう．述語部に，以下の記述がある（p4）．
Available’ = Available \ {bc?}
統合左側のプライムは，変化後の値を持つことを示している．本を貸し出すと，貸出可能な本の集合から（Available），貸し出した本（bc）分は減ることになる．Availableは，LibraryShelvesで定義しているのだが，それはLibrarySystemに包含されているので，その状態が変化するとして，∆の記号を持つ．状態変化を伴わない場合は，Ξの記号を用いる (d2, d3)．
記述部のうち，最初の3つ（p1〜p3）は，事前条件に相当する．後半の3つ (p4-p6) は，先に見たように状態変数の変化を示している．この部分は，事後条件に相当する．
さて，順番に見ていく．
疑問符が付いている状態変数は，入力を示している(d4,d5)．ここでは，借りに来る人（p）とその人が持っている本（bc）を示す変数である．借りに来る人は，利用者として登録している人か，或いは図書館のスタッフである（即ち，それ以外の人は対象外である）(p1)．本は当然利用可能でなくてはならない（貸出中であれば，持っているハズがない）(p2)．
(p3) は少し問題がある．以前にも出てきた▷は，値域制限（range restriction）である．BorrowedByは，LibraryShelvesスキーマで，BookCopyからPersonへの部分関数であり，貸出数に制約を与えるが，不変条件の記述と矛盾しているので，実際には不要である．
(p4) は，先に説明した．(p5) では，貸出を行うので，貸出中（OnLoan）が，貸し出した分だけ増えることを示している．
(p6) 誰に貸しているか関係では，本と借りた人の関係を新たに追加している．
(nil）