Some problems present us with a large collection of facts and rules, but no underlying theory that we can use to design a compact algorithm for calculating a solution. Examples of such problems include medical diagnosis and treatment planning, scheduling jobs in a machine shop, diagnosis and repair of malfunctioning machinery, and determining customers' eligibility for financial credit. In these areas there are no simple first principles from which everything follows; instead, there are a lot of empirical observations and rules gleaned from hard experience or laid down by fiat. Sometimes you can find an acceptable solution by searching for relevant facts and applying the pertinent rules. Rule-based programming mechanizes this style of problem solving.

Rule-based programs are sometimes called expert systems and are said to display artificial intelligence, but they are just computer programs that employ some specialized techniques that have been found useful for certain kinds of problems. If such a program is intended for a serious purpose, it must meet the same standards of quality and correctness required of other programs. How can we tell if a rule-based program has computed the right answer?

Rule-based programs are often evaluated by submitting some sample results to a panel of human experts. This kind of validation can be helpful but it does not provide sufficient coverage to detect every incorrect result nor does it provide any guidance for design and implementation.

Object-oriented programming is a method for creating programs that use a particular kind of model. Object-oriented programming languages such as Smalltalk and C++ can implement these models, but a simpler notation that is independent of any programming language is more useful when you are creating and analyzing the models. Z can serve as that notation. You can do object-oriented design in ordinary Z, and there are several Z dialects that are intended to provide better support for object-oriented programming.

The object-oriented model and Z

The data in an object-oriented program are encapsulated in record-like data structures called objects. Objects belong to types called classes. You change or examine the data in an object, called its attributes or instance variables, by invoking one of the methods defined for the object's class.

Z is a good match to this object-oriented model. A Z state schema together with the operation schemas on that state define a class. The state variables in the state schema are the attributes or instance variables of that class; the operation schemas are the methods. Bindings, which are instances of the state schema type, are objects, which are instances of the class.

The cyclotron control sytem model in Chapter 23 can be considered an object-oriented design in this sense. All the data are encapsulated in objects, and the only way to read or change any data is by invoking a method.

We have already learned how Z can be used to describe data structures. Sometimes the solution to a problem is just a data structure that has some particular properties. In that case, the description of the data structure is the central element in the whole specification. A well-known example is the problem of the eight queens.

Many books on programming show how to solve the problem of the eight queens (for example, see Wirth [1976]). Here is the problem statement in English:

Figure 18.1 illustrates one solution to the problem.

This is not a problem of great practical significance, but it does illustrate some common difficulties of prose specifications: They usually turn out to be imprecise and incomplete. The English problem statement is usually considered sufficient because “everybody knows what it means.” When we write real specifications, usually everybody does not know what is needed. When we write the program, we can't appeal to visual impressions and intuitions. Could you explain the eight queens problem to somebody who had never seen a chessboard? What if you had to communicate by telephone and couldn't refer to a picture?

Z is a set of conventions for presenting mathematical text, chosen to make it convenient to use simple mathematics to describe computing systems. I say computing systems because Z has been used to model hardware as well as software.

Z is a mature notation. Conceived in the late 1970s, it developed through the 1980s in collaborative projects between Oxford University and industrial partners, including IBM and Inmos (a semiconductor producer). The first Z reference manual to be widely published benefited from this long experience when it finally appeared in 1989. At this writing a draft Z standard (including a formal semantics) is being considered by the American National Standards Institute (ANSI), the British Standards Institute (BSI) and the International Organization for Standardization (ISO). Z has served as the basis for other notations, including several variants adapted for object-oriented programming.

Z is a model-based notation. In Z you usually model a system by representing its state — a collection of state variables and their values — and some operations that can change its state. A model that is characterized by the operations it describes is called an abstract data type (ADT). This modelling style is a good match to imperative, procedural programming languages that provide a rich collection of data types, and also to some physical systems (such as digital electronics) that include storage elements. Z is also a natural fit to object-oriented programming.

This chapter shows how to use schemas to define new data types. It also explains the mathematical meaning or semantics of schemas. This will help you use schemas expressively and reason about Z texts.

Schema types

So far we have treated schemas as nothing more than macros that we can use to abbreviate blocks of mathematical text. In this view, schemas and the schema calculus are just conveniences: They save us a lot of writing, but they don't introduce any new concepts. This modest view provides practical benefits — but it isn't very ambitious.

Schemas are more than just abbreviations. They are objects in their own right. Schema definitions declare new data types called schema types. The instances of schema types are objects called bindings. Schema references denote sets of bindings. Schema types and bindings are new kinds of mathematical objects.

So far we have defined only three kinds of fundamental data types — all of the others are built up from these: basic types, declared as in [X], whose instances are individuals; set types, declared as in ℙ X, whose instances are sets; and Cartesian product types, declared as in X × Y, whose instances are tuples. Schema types and their instances, bindings, are the fourth (and last) kind of data type in Z.

A binding is the formal realization, in Z, of what we have been calling a situation or a state: an assignment of particular values to a collection of named variables.

From Chapter 6

The state machine model did not specify the initial state. The only reasonable choice is the PATIENTS state.

From Chapter 10

beam = on ↔ door = closed means the beam is on when the door is closed and the beam is off when the door is open. This is a bad requirement because the beam will turn on the moment the door is closed.

beam = on ∧ door = closed means the beam is always on and the door is always closed. Obviously useless.

beam = on ∨ door = open means the beam is on or the door is open, or both. This is a bad requirement because it allows the beam to be on when the door is open.

beam = off ∨ door = closed means the beam is off or the door is closed, or both. This is a good requirement, and means exactly the same thing as beam = on ⇒ door = closed, according to the law p ⇒ q ⇔ ¬ p ∨ q.

x ∈ dom f ⇒ f x = y is true when x ∈ dom f is false, otherwise it has the same truth value as f x = y.

From Chapter 11

Represent each triangle as a tuple whose components are the lengths of its three sides. These tuples are called Pythagorean triples because their components are related by the Pythagorean theorem; (3, 4, 5) is a Pythagorean triple because 32 + 42 = 52.

In this chapter we pursue the safety issues introduced in the therapy machine study from Chapter 6. To ensure that patients are treated as directed by their prescriptions, many machine settings must be set properly. The radiation beam should only be allowed to turn on when the correct settings have been achieved. This chapter presents a formal specification for the control software that permits the beam to turn on. It is an example of a safety-critical protection system because it prevents some potentially hazardous action from occurring unless particular safety requirements are satisfied.

This study also illustrates how Z can express two important design strategies: partitioning a complex system into largely independent subsystems or modules and refining from an abstract model to a detailed design.

Partition

First we develop a more detailed model of the therapy machine system Machine that we introduced in Chapter 21. Much of the apparent complexity of the therapy machine arises from the interaction of several subsystems which, by themselves, are simpler. We partition the system into subsystems and describe simple operations on each. For each operation on the system as a whole, we define a separate operation on each affected subsystem. The complex behaviors of the whole system emerge when we compose these simpler operations together.

The advantages of this approach arise because many operations involve only a few of the subsystems, and many complex operations can emerge when simpler operations appear together in different combinations.

We have described a universe that is richly populated with individuals, sets, tuples, relations, functions, and sequences. We can extend our univetse indefinitely by using operators to build up ever more complex structures. But we need something more.

We need a way to classify the profusion of structures we can create. We need to divide the wheat from the chaff, the sheep from the goats, the bogus from the bona fide. We will make an essentially binary distinction between the answer we are looking for — the objects we wish to model — and everything else. Our tool for distinguishing the two is called logic. The concept of a purely binary classification may seem crude, but with logic we can express distinctions that are exceedingly fine.

Basic predicates

The textual unit of logic is the predicate. There are just a few kinds of basic predicates. All the others are built up from these.

The simplest predicates are true and false. We say true and false are the two logical constants or truth values. In fact, every predicate has one value or the other, true or false. There are many rules for simplifying predicates or otherwise inferring whether any predicate, no matter how complicated, is true or false.

The next basic predicate is equals, =. The predicate e1 = e2 is true when the two expressions e1 and e2 have the same value, and is false otherwise.