Z: Defining Observing Operations Find status Library book?: BOOK status!: STATUS book?∈book status!= status(book? E indicates state is not changed by operation(a lookup op) status is an output variable The first invariant says that schema only defined if the book is known. Therefore, function application in second invariant cannot failZ : Defining Observing Operations book?: BOOK Library status! : STATUS book? status! = status (book?) books Find Status indicates state is not changed by operation (a lookup op) status! is an output variable The first invariant says that schema only defined if the book is known. Therefore, function application in second invariant cannot fail. c Copyright Nancy Leveson, Sept. 1999 �