Lesson 10: Introduction to Z- Method :Lesson 10: Introduction to Z- Method INTRODUCTION TO Z - METHOD


Specifying with Z :Specifying with Z Z is a notation for describing the behavior of sequential processes. The Z notation is based on the elementary set theory and logic, and was introduced in the early 1980s as part of a project sponsored by the IBM United Kingdom Laboratories. A Z description of the functionality of a software system consists of a collection of structures called schemas. A schema describes the static (states, invariant relationships) and dynamic (operations, relationships between input and output, state changes that can happen) features of a system. A schema has the form shown in Figure 1. A schema declaration has syntax given in Figure 2.


Steps in Constructing a Z Specification :Steps in Constructing a Z Specification Decide on the basic sets, operations, and invariant relationships needed to describe the behavior of software to be developed. Introduce a schema to define the state space for the software. Decide what operations are needed to introduce state changes. Identify inputs to and outputs from the system. Introduce schema to induce state changes. For each schema in step 5, give the necessary conditions (pre- and postconditions) that must be satisfied.


Structure of a Z Schema :Structure of a Z Schema ------ Schema Identifier ---------------------------- | Declaration-Part | {status} State space identifier | Variable declaration | Function declaration |------------------------------------ | Optional pre-condition | Optional post-condition ------------------------------------------------------------ Figure 1: Structure of a Z schema


Syntax for a Z Schema Declaration :Syntax for a Z Schema Declaration SchemaDeclaration ::= {status} Identifier Identifier: set_type | Identifier: domain  range | Identifier {? | !}: set_type Status ::= Δ | Ξ --Status indicates if state space is changed or not --Variable declaration --Function declaration --Input operation (?) or output operation (!) --Δ (schema describes state change) --Ξ (state space does not change after operation) Figure 2: Syntax for a Z schema declaration


Example: Z Specification for tATC :Example: Z Specification for tATC In this section, Z is used to specify a record-keeping system for airspace configurations for a training program of air traffic controllers (the tATC system). Let Display be a set of displays (each showing a different air traffic controller’s view of an airspace). Each display is associated with its own name and icons (graphics of an airspace display). Let known be a set of recorded airspace displays, and let airspace be the name of a function that maps a known airspace to a display.


Example (Cont.) :Example (Cont.) The following schema defines the state space of the tATC display_handling utility: The idea behind this schema is to give a concise description of available airspace configurations, and how to establish an indexing system for these configurations. ------ AirspaceCofig ------------------------- | known: ¶ Name × Icon | airspace: Name × Icon  Display |------------------------------------ | known = dom airspace ----------------------------------------------------


Example (Cont.) :Example (Cont.) Now we can begin defining “methods” for initializing, changing the set of airspace configurations, drag-and-drop as well as click-and-see operations in an interactive tATC training program. The following schema describes the initial state of the tATC system: ------ initAirspaceConfig ----------------------------- | AirspaceConfig |-------------------------------- | known = ø ------------------------------------------------------------


Example (Cont.) :Example (Cont.) In addition, the symbols ? (input) and ! (output) carry over from CSP in specifying input/output operations in Z. The operation to add a new configuration is specified with the AddAirspaceConfig schema: ------ AddAirspaceConfig ------------------------------- | Δ AirspaceConfig | config?: Name × Icon | display?: Display |------------------------------- | known {config?  display} = ø | airspace’ = airspace {config?  display?} ---------------------------------------------------------------


Example (Cont.) :Example (Cont.) The AddAirspaceConfig schema induces a state change. By convention, unprimed variables denote a state before an operation has been performed while primed variables denote the state of a system after an operation has been performed. The input of a new configuration (config?) results in the replacement of the set named airspace with a new set of known airspace configurations named known’. This result can be expressed succinctly by asserting known’ = known {config?}


Example (Cont.) :Example (Cont.) For simplicity, it is assumed that there are two types of icons in an airspace display: buttons to control the display, and graphics representing airspace features. The following schema can be used to specify a click-and-see operation: ------ clickAndseeAirspace ------------------ | Δ AirspaceConfig | config?: Name × Icon | button?: Icon | click: Name × Icon × Icon  Name × Icon |---------------------------------- | known {config?} ø Λ | {button?} ø Λ | click(config?, button?) airspace ----------------------------------------------------


Example (Cont.) :Example (Cont.) The click operation maps these inputs to a new airspace. It is assumed that some of the graphics in a display can be moved(repositioned) by an air traffic control trainee. This makes it possible for a trainee to customize or tailor a display. Introduce a schema to describe a drag-and-drop operation: ------ dragAnddropAirspace ------------------------------------- | Δ AirspaceConfig | config?: Name × Icon | drag: Name × Icon  Name × Icon | drop: Name × Icon  Display |------------------------------------ | known {config?} ø Λ | known {drag(config?)} ø Λ | known {drop(config?)} ø Λ | {drag(config?)} ø Λ | airspace’ = airspace – {drag(config?)} Λ | airspace” = airspace {drop(config?)}  Display ------------------------------------------------------------------------


Example (Cont.) :Example (Cont.) The drag AnddropAirspace schema says the drag and drop operations result in a state change, provided that the value of input by config? is know and the drag operation is non-empty. There are preconditions for a state change. Performing a drag operation results in the deletion of an old configuration of the airspace (the new set of configurations is named airspace’). The new configuration of airspace resulting from the drop is added to known’ (the new set of configurations is named airspace”).


Example (Cont.) :Example (Cont.) A description of the tATC display-handling facility can include an operation to save a copy of a display to a file. This is done with the SaveAirspaceConfig schema. ------ SaveAirspaceConfig ---------------- | Ξ AirspaceConfig | config?: Name × Icon | copy!: Name × Icon |------------------------------ | config? Known | copy! = airspace(config?) ------------------------------------------------