PROGRAMMER'S BOOKSHELF

Software Engineering and Z

Reginald B. Charney

Reg is president of Charney & Day. He can be reached on CompuServe at 70272,3427 or at charney@pipeline.com.

Software Development with Z, by J.B. Wordsworth, is an introduction to modern-day formal methods and their practicality for software development. Although Wordsworth uses only the Z specification language (supported by a variant of Dijkstra's guarded command language), you still get a good sense for strongly typed specification languages. The book also serves as a tutorial on formal methods in general and the Z language in particular.

While the book is easily read and understood, you do need to familiarize yourself with set theory and its notation, since Z uses more than 90 different symbols, most of which are nonmnemonic and unavailable in any normal typeface. Some operators are overloaded, and the naming conventions are not always helpful. For example, names like je1 and k1 are used instead of b1 and b2.

Software Development with Z starts out by covering the basics of discrete mathematics: sets, logic, and relationships. It then examines Z schema and the guarded command language and finally discusses design and implementation issues.

Wordsworth uses two examples throughout the book. One discusses a library, its books, and the people borrowing them, while the second is based on school classes and people enrolled in them. The examples are discussed informally at first, and are developed more rigorously as the book progresses. This approach maintains coherence and makes the book easy to follow. A complete application appears at the end of the book, less the actual code.

There are exercises at the end of each chapter, with answers for most of the questions. There's also an appendix containing a bibliography and a complete list of all special symbols used in Z.

Z Language Specification

Z lets you record software specifications, data design, and algorithmic implementation decisions. It is not a programming language, and is best used for defining specifications, rather than designs.

More specifically, Z is a mathematical software-specification language developed in the 1970s at Oxford University in England. In the early 1980s, software developers at IBM's Hursley Research Centre started working on Z, releasing commercial CICS online-transaction software for banks and airlines in the early 1990s. Wordsworth was a part of IBM's original Z development team.

Figures 1 through 4 show schema specifications in Z. The first line always declares the schema name. The remaining lines in the upper part of the schema declare data types used in the schema. The lower part of the schema consists of the predicates that must be true for the schema to be valid.

Figure 1 is a typical schema specification. It defines the starting conditions that must exist for an oil-terminal control system. The following are the interpretations of the code by line number:

  1. OTCSys is the schema name.
  2. waiting is of the type "sequence of Tankers."
  3. docked is of the type "operation of relating a Tanker to a unique Berth."
  4. known is of the type "one set out of all possible sets of Tankers."
  5. No Tanker can be waiting and docked at the same time.
  6. The number of waiting Tankers is the number of Tankers in the sequence of Tankers.
  7. If Tankers are waiting, then all Berths are filled by docked Tankers.
  8. Docked Tankers are a subset of the Berths.
  9. All known Tankers are either docked or waiting.
Figure 2 shows that the precondition for any arriving Tanker is that it is not yet known.

  1. Arrive0 is the name of the schema.
  2. The declarations used in OTCSys apply here as well.
  3. t is an input variable of the type "Tanker."
  4. t is not already known.
When a Tanker arrives at the oil terminal, either Berths are available and it is docked (see Figure 3) or all Berths are occupied and the Tanker must be queued (see Figure 4).

For Figure 3:

  1. Docked is the name of the schema.
  2. The contents of schema Arrive0 are inserted into schema Docked.
  3. b is an output variable of the type "Berth."
  4. r is an output variable of the type "Response" (there either is or is not room for the Tanker).
  5. A Berth is available.
  6. If line 5 is true, the output response is ok for this schema.
  7. An unoccupied Berth is output.
  8. The list of docked tankers is updated by appending the current tanker to the set of those already docked (x and x' represent the before and after states of variable x).
  9. There is no change in the state of those waiting.
For Figure 4:

  1. Queued is the name of the schema.
  2. The complete contents of schema Arrive0 is inserted into schema Queued.
  3. r is an output variable of type "Response."
  4. Tankers are docked at all Berths.
  5. If line 4 is true, then the response is wait.
  6. The current Tanker is appended to the sequence of waiting Tankers.
  7. There is no change in the state of the docked Tankers.

Guarded Command Language

Given these schema, you can write this logical equation in Z:ArrivedOKDocked v Queued. Because Z is only a specification language, Dijkstra's guarded command language is used to implement the specifications. This language consist of statements having two parts, a guard and a command, separated by a --> sign. The command is executed only if the guard expression is true. For example, to increment a variable x by 1, we would normally write x:=x+1. In the guarded command language, you would write x<MAX_INT-->x:=x+1, which states that the increment operation is valid only if the current value of x is less than the maximum allowable integer value.

The guarded command language has three control structures: sequence, alternation, and iteration. These control structures are made up of constructs, each of which consists of a guard expression and a body. A guard expression must be true for the body of the statement to be executed. Either the guard or the body can be omitted.

The Social Side

Wordsworth emphasizes that formal methods are part of a social process of software development, which should include a group of people representing various parts of the development cycle. Formal methods are not means for developing software without difficult decisions, says Wordsworth, but are methods for recording those decisions once made. Z documents consist principally of English text with small pieces of mathematical formalisms.

I highly recommend the beautifully written section on writing good specifications, as well as Wordsworth's description of how to verify a specification. Verification is part of the testing process. His comments on testing are reminiscent of one of Edward Yourdon's main points in Decline and Fall of the American Programmer (Prentice Hall, 1991): Tracking bugs is important, not just to fix problems, but to modify the processes that created them.

Software Development with Z achieves its three principal aims: To encourage programmers to explore the use of formal methods in perfecting their craft, to provide an insight into the practical problems of applying mathematics to real software development, and to explain the features of Z.

Software Development with Z

J.B. Wordsworth

Addison-Wesley, 1992, 334 pp.

$32.25

ISBN 0-201-627-57-4

Figure 1 Starting conditions for an oil-terminal control system.

Figure 3 Tanker is docked.

Figure 2 Condition for arriving Tankers.

Figure 4 Tanker is queued.

Copyright © 1995, Dr. Dobb's Journal