Z: Defining Operations Borrow △ Library book ?: BOOK status(book? ) =In status= status o(book?out) A Library declaration says operation modifies state of Library book? is the input A prime indicates the value after the operation The first invariant defines a pre-condition on the operation, i.e the book to be borrowed must be currently checked in The second invariant defines the semantics of borrowing i e,ok it overwrites the entry in the status function for the borrowed bo ancy Leveson, Sept. 1999Z : Defining Operations Borrow book?: BOOK Library status’ = status (book? status (book?) = In Out) Library declaration says operation modifies state of Library book? is the input A prime indicates the value after the operation The first invariant defines a pre-condition on the operation, i.e., the book to be borrowed must be currently checked in. The second invariant defines the semantics of borrowing, i.e., it overwrites the entry in the status function for the borrowed book. Copyright Nancy Leveson, Sept. 1999 c �