Z specifications are structured as a set of schemas—a boxlike structure that introduces variables and specifies the relationship between th...

Z specifications are structured as a set of schemas—a boxlike structure that introduces variables and specifies the relationship between these variables. A schema is essentially the formal specification analog of the programming language subroutine or procedure. In the same way that procedures and subroutines are used to structure a system, schemas are used to structure a formal specification.

We use the Z specification language to model the block handler example, A summary of Z language notation is presented in Table 25.1. The following example of a schema describes the state of the block handler and the data invariant:

**TABLE 25.1 Summary of Z Notation**

Z notation is based on typed set theory and first-order logic. Z provides a construct, called a schema, to describe a specification’s state space and operations. A schema groups variable declarations with a list of predicates that constrain the possible value of a variable. In Z, the schema X is defined by the form

———X–––––––––––———————————————

declarations

————————————————————————

predicates

————————————————————————

Global functions and constants are defined by the form

declarations

————————————————————————

predicates

————————————————————————

predicates

The declaration gives the type of the function or constant, while the predicate gives it value. Only an abbreviated set of Z symbols is presented in this table.

**Sets:**

S : X Sis declared as a set of Xs.

x S xis a member of S.

x S xis not a member of S.

S T Sis a subset of T: Every member of S is also in T.

S T The union of S and T: It contains every member of S or T or both.

S T The intersection of S and T: It contains every member of both S and T.

S \ T The difference of S and T: It contains every member of S except those also in T.

Empty set: It contains no members.

{x} Singleton set: It contains just x.

The set of natural numbers 0, 1, 2, ....

S : X Sis declared as a finite set of Xs.

max (S) The maximum of the nonempty set of numbers S.

**Functions:**

f:X >→Y fis declared as a partial injection from X to Y

dom f The domain of f: the set of values x for which f (x) is defined.

ran f The range of f: the set of values taken by f (x) as x varies over the domain of f.

f {x → y} A function that agrees with f except that x is mapped to y.

{x} – f A function like f, except that x is removed from its domain.

**Logic:**

**P Q Pand Q: It is true if both P and Q are true.**

P =>Q Pimplies Q: It is true if either Q is true or P is false.

S’ = S No components of schema S change in an operation.

———BlockHandler——————————————

used, free : BLOCKS

BlockQueue : seq BLOCKS

———————————————————————

used free =

used free = AllBlocks

i : dom BlockQueue . BlockQueue i used

i, j : dom BlockQueue . i ≠ j =>

BlockQueue i BlockQueue j =

————————————————————————

used, free : BLOCKS

BlockQueue : seq BLOCKS

———————————————————————

used free =

used free = AllBlocks

i : dom BlockQueue . BlockQueue i used

i, j : dom BlockQueue . i ≠ j =>

BlockQueue i BlockQueue j =

————————————————————————

———BlockHandler——————————————

used, free : BLOCKS

BlockQueue : seq BLOCKS

———————————————————————

used free =

used free = AllBlocks

i : dom BlockQueue . BlockQueue i used

i, j : dom BlockQueue . i ≠ j =>

BlockQueue i BlockQueue j =

————————————————————————

The schema consists of two parts. The part above the central line represents the variables of the state, while the part below the central line describes the data invariant. Whenever the schema representing the data invariant and state is used in another schema it is preceded by the symbol. Therefore, if the preceding schema is used in a schema that, for example, describes an operation, then it would be written as Block- Handler. As the last sentence implies, schemas can be used to describe operations.

used, free : BLOCKS

BlockQueue : seq BLOCKS

———————————————————————

used free =

used free = AllBlocks

i : dom BlockQueue . BlockQueue i used

i, j : dom BlockQueue . i ≠ j =>

BlockQueue i BlockQueue j =

————————————————————————

The schema consists of two parts. The part above the central line represents the variables of the state, while the part below the central line describes the data invariant. Whenever the schema representing the data invariant and state is used in another schema it is preceded by the symbol. Therefore, if the preceding schema is used in a schema that, for example, describes an operation, then it would be written as Block- Handler. As the last sentence implies, schemas can be used to describe operations.

The following example of a schema describes the operation that removes an element from the block queue:

———RemoveBlock———————————————

BlockHandler

————————————————————————

#BlockQueue > 0,

used' = used \ head BlockQueue

free’ = free head BlockQueue

BlockQueue' = tail BlockQueue

—————————————————————————

The inclusion of BlockHandler results in all variables that make up the state being available for the RemoveBlock schema and ensures that the data invariant will hold before and after the operation has been executed.

The second operation, which adds a collection of blocks to the end of the queue, is represented as

———AddBlock—————————————————

BlockHandler

Ablocks? : BLOCKS

—————————————————————————

Ablocks? used

BlockQueue' = BlockQueue Ablocks?

used' = used

free' = free

——————————————————————————

By convention in Z, an input variable that is read from and does not form part of the state is terminated by a question mark. Thus, Ablocks?, which acts as an input parameter, is terminated by a question mark.