Abstract Model Specifications Build an abstract model of required software behavior using mathematically defined(perhaps using axioms )types(e. g sets, relations) Define operations by showing effects of that operation on the model Specification includes Model Invariant properties of model For each operation name parameters return values Pre and post conditions on the operations
Abstract Model Specifications Build an abstract model of required software behavior using mathematically defined (perhaps using axioms) types (e.g., sets, relations). Define operations by showing effects of that operation on the model. Specification includes: Model Invariant properties of model For each operation: name parameters return values Pre and post conditions on the operations Copyright c Nancy Leveson, Sept. 1999 �
Z(pronounced zed Z specifications are made up of"schemas A schema is a named, relatively short piece of specification with two parts Above the line the definition of the data entities Below the line the definition of invariants that hold on those data entities Copyright Nancy Leveson, Sept. 1999
Z (pronounced Zed) Z specifications are made up of "schemas" A schema is a named, relatively short piece of specification with two parts: Above the line: the definition of the data entities Below the line: the definition of invariants that hold on those data entities Copyright c Nancy Leveson, Sept. 1999 �
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. 1999
Z : 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 �
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. 1999
Z : 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 �
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 books
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 {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 �