Z: Defining the abstract model Library books:P BOOK status: BOOK k STATUS books dom status Declaration says library has two visible parts of its state books is a set of books. which are atomic elements status is a partial function that maps a booK into a status (which is another atomic element that can take values In or out) The invariant says the set of books is precisely the same as the domain of the function status Says every book in the Library has exactly one status Two books may have the same status EXample of a legal state for Library is books=Principia Mathematica, Safeware status=(Principia Mathematica h-In Safeware r- Out Copyright Nancy Leveson, Sept. 1999Z : Defining the Abstract Model Library books: BOOK status: STATUS books = dom status P BOOK Declaration says library has two visible parts of its state: books is a set of BOOKS, which are atomic elements. status is a partial function that maps a BOOK into a STATUS (which is another atomic element that can take values In or Out) The invariant says the set of books is precisely the same as the domain of the function status. Says every book in the Library has exactly one status Two books may have the same status. Example of a legal state for Library is: books = {Principia Mathematica, Safeware} status = (Principia Mathematica In, Safeware Out} c Copyright Nancy Leveson, Sept. 1999 �