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 �
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 fail
Z : 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 �
Z: Another Observing operation CheckedOut Library out!= P BOOK out!= b books status(b)=Outy Produces all the books that are currently checked out of library Returns a(possibly empty) set of books
Z : Another Observing Operation Library CheckedOut out! = P BOOK out! = { b:books | status(b) = Out} Produces all the books that are currently checked out of library Returns a (possibly empty) set of books. Copyright Nancy Leveson, Sept. 1999 c �
Z: Initialization InitLibrary Library books Still need schemas to add and remove books from the library
Z : Initialization InitLibrary Library books = Still need schemas to add and remove books from the library. Copyright Nancy Leveson, Sept. 1999 c �
