Z: Proving Properties EXample: After a borrow operation, the set of books in the library remains unchanged books'= books books'= dom status [from invariant of Library dom (status o (book? H Out]) [from post-condition of Borrow] dom(status v (book? H Outy) dom status v dom ((book?H+ Out]) Follow from mathematics book book? book [ true because first invariant of Borrow implies that book is an element of booksZ : Proving Properties Example: After a borrow operation, the set of books in the library remains unchanged. books’ = books books’ = dom status’ [from invariant of Library] = dom (status {book? Out}) [from post-condition of Borrow] = dom (status {book? Out}) = dom status dom ({book? Out}) Follow from mathematics = book book? = book [true because first invariant of Borrow implies that book? is an element of books] Copyright c Nancy Leveson, Sept. 1999 �