Z: Another Observing operation CheckedOut Library out!= P BOOK out!= b books status(b)=Outy Produces all the books that are currently checked out of library Returns a(possibly empty) set of booksZ : Another Observing Operation Library CheckedOut out! = P BOOK out! = { b:books | status(b) = Out} Produces all the books that are currently checked out of library Returns a (possibly empty) set of books. Copyright Nancy Leveson, Sept. 1999 c �