Developing Formal Specifications in Z
Hossein Saiedian · 2007
State of the System • Every sequential system has an abstract state space which should be specified via a schema. For large systems, the abstract schema may be constructed of several other schemas using the schema calculus. • An Example: A simple library system LibSystem members : P PERSON shelved : P BOOK checked : BOOK 7 → PERSON shelved ∩ dom checked = ∅ ran checked ⊆ members ∀mem : PERSON • #(checked {mem}) ≤ MaxLoan Copyright Saiedian © 2007 (For exclusive use of EECS Software Engineering Students) EECS810: Software Engineering (University of Kansas, Fall 2007) Slide 47 A Case Study in Z: APhoneDir System • Objective: Construct a telephone directory system (called PhoneDir ), for a university to maintain a record of faculty and their telephone numbers. • System Requirements: – A faculty may have one or more telephone numbers – Some faculty may not have a telephone number yet – A number may be shared by two or more faculty – Must be able to add new faculty and/or new entries – Must be able to remove faculty and/or existing entries – Must be able to query the system for a faculty or number • Based on an example by Diller (1994). Copyright Saiedian © 2007 (For exclusive use of EECS Software Engineering Students) EECS810: Software Engineering (University of Kansas, Fall 2007) Slide 48 Present Given, User-defined Types • A type to represent individual persons [PERSON ] We are not interested in more detail about persons. • Can use natural numbers N to model telephone numbers, or as an alternative, can assume a given type: [PHONE] • Note that we could have restricted the range, e.g., PHONE == 41000 . . 49999 Copyright Saiedian © 2007 (For exclusive use of EECS Software Engineering Students) EECS810: Software Engineering (University of Kansas, Fall 2007) Slide 49 Present Given, User-defined Types (continued) • Output messages: MESSAGE ::= ‘OK’ | ‘Faculty already exists’ | ‘No such faculty’ | ‘Faculty has no number’ | ‘Invalid number’ | ‘Invalid entry’ | ‘Entry already exists’ Copyright Saiedian © 2007 (For exclusive use of EECS Software Engineering Students) EECS810: Software Engineering (University of Kansas, Fall 2007) Slide 50 Abstract State of PhoneDir System • A set of type PERSON representing the faculty: faculty : P PERSON • Abstract representation of an instance of faculty:State of PhoneDir System • A set of type PERSON representing the faculty: faculty : P PERSON • Abstract representation of an instance of faculty: ideen mary hossein chen stan Copyright Saiedian © 2007 (For exclusive use of EECS Software Engineering Students) EECS810: Software Engineering (University of Kansas, Fall 2007) Slide 51 Abstract State of PhoneDir System (continued) • We need another set representing a directory in the system: directory :???? • Abstract representation of an instance of directory:State of PhoneDir System (continued) • We need another set representing a directory in the system: directory :???? • Abstract representation of an instance of directory: Copyright Saiedian © 2007 (For exclusive use of EECS Software Engineering Students) EECS810: Software Engineering (University of Kansas, Fall 2007) Slide 52