These selections from the tool-kit are based on the Reference Manual. They include all the operators used in this book and a few more that are needed to define them.

The definitions in the tool-kit require some Z constructs we have not used elsewhere. It uses generic definitions very heavily: X, Y, and Z stand for any type, S and T are sets of any type, and Q and R are binary relations between any two types. The tool-kit also makes extensive use of patterns in abbreviation definitions, for example it defines the binary relation symbol by X ↔ Y == ℙ(X × Y).

In a few places I've used English paraphrases for predicates, where the formal definition uses constructs or concepts not discussed in this book.

Formal methods apply logic and simple mathematics to programming. They work best where traditional programming methods don't work very well: problems that are too difficult to solve by intuition or too novel to solve by modifying some existing program or design. They can help you create new programs, or analyze and document programs that are already written. Using formal methods requires creativity and judgment, but once you have created or analyzed a program formally, you can document your work as a sequence of steps that you or anyone else can check. You must be able to do this if you need to convince yourself or others that a program meets requirements for safety, accuracy, security, or any other critical property. It is also worth doing if you simply want to understand how the program works.

What are formal methods?

Formal methods are methods that use formulas.

A formula is a text or diagram constructed from predefined symbols combined according to explicit rules. A good working definition of formula is anything whose appearance or syntax can be checked by a computer. According to this definition, every computer program is a formula.

It's a little odd for programmers to speak of formal methods as if they were something special – as if formality were an option. If you want to program a computer, you really don't have any choice. Computation is formula evaluation.

All of our examples so far have been small: They have only a few state variables. In this chapter we tackle a large system that has hundreds of state variables. Z provides several structuring techniques that make this feasible. The system is large but the Z description is concise. It is built up from components, subsystems, conditions, and modes that are developed separately, but also accounts for behaviors that emerge at the system level. The description illustrates several useful idioms of the Z notation, including one called promotion.

The case study in this chapter is the control system for a cyclotron, a type of particle accelerator. A radiation therapy machine includes an accelerator that produces a radiation beam and therapy equipment that uses the beam. In Chapters 6, 21, and 22 we described some of the controls for the therapy equipment. Now we turn to the controls for the accelerator.

Our system is built up from many components, and most of its size derives from repetition of similar components. We can make our specification much shorter and easier to grasp by identifying the components, describing them separately, and then combining them. We will define a schema type for each kind of component. The system contains multiple copies of most kinds of components, so the system model contains multiple bindings of those schema types. Many features are common to several kinds of components, and these can be concisely represented by schemas that are included elsewhere.

I learned Z (pronounced zed) when I got tired of programming by trial and error.

I write large programs for a serious purpose. I work in a clinical department in a research hospital. My first project here was a program that assists in planning radiation therapy treatments for cancer, by performing physics simulations – radiation dose calculations – with 3-D interactive graphics. Our planning system took more than two years to develop and comprised 40,000 lines of code. We spent plenty of time on design, coded carefully, and ran lots of tests.

Like most software, our system usually worked. It did most of what the users asked for – and some things that they didn't. It handled most cases correctly – then every so often it did the wrong thing, locked up, or crashed. We, the developers, were as surprised by the bizarre behavior as anyone else. Fortunately, the computations were done before patients' treatments began and every result was reviewed thoroughly. We could detect and work around the problems. We could live with it – though it wasn't always convenient.

We had to do better. Our next project was the computer control system for a unique radiation therapy machine at our clinic. Typical software quality wasn't good enough. We had recently learned of another therapy control system that had killed people!

I surveyed every development method I could find, including many packaged as software products with nice facilities for drawing diagrams and producing documents.

So far we have been using Z to name objects, describe their structure, and state some of their properties. For each property of an object, we added another formula to the description. But this is not always necessary. We don't have to spell out each property explicitly. Once we have stated a few properties, we can infer many more by using formal reasoning. This ability to infer new facts by applying simple rules is one of the distinguishing features of a formal method.

Reasoning enables us to use a formal model as a nonexecutable prototype or oracle. Formal reasoning plays somewhat the same role for mathematical models that testing does for code. Just as you can experiment with code by running it, you can investigate the behavior of a nonexecutable prototype by reasoning. You can check important system properties before you write a single line of code. Moreover, an exercise in formal reasoning often establishes the behavior for a whole class of situations, not just a single test case.

We can use formal reasoning to validate a mathematical model against requirements. A model is valid if its properties satisfy the intent of the requirements. Requirements are usually not expressed formally, but we can translate almost any reasonable requirement to a predicate. We can then attempt to determine whether this predicate follows from the predicates in our model. If it does, the model is valid with respect to that requirement.

Why study formal methods? This chapter describes the predicament that formal methods were invented to solve and presents a vision of what programming should be.

Software frequently disappoints us. As users, we find that many programs are a poor match to our real needs and frustrate us with unrepaired defects. As programmers, our disappointment is especially keen. We expect to find the joy of creation in our work and the satisfaction of providing something useful. But all too often our expectations are dashed, our joy is spoiled, and our job becomes a dispiriting slog, churning out shapeless code and patching up bugs.

What's wrong? Is there something inherent in the nature of software that makes our troubles as inevitable as bad weather?

I argue that creating software is not intrinsically more difficult than any other kind of engineering. Many of our difficulties result from avoidable mistakes and poor programming practices.

A central problem is that people feel it is acceptable to create software without fully understanding what they are doing — they believe they can produce software and then understand it later by running tests and observing users' experience. It is this attitude, rather than any inherent difficulty in the task, that results in so many software problems.

This error can be made at any stage. Designers specify products when they don't fully understand customers' real needs. Programmers write code when they don't fully understand what it will do, and so on.

This chapter introduces the three basic constructs that appear everywhere in Z texts: declarations, expressions, and predicates. Declarations, introduce variables. Expressions describe the values that variables might have. Predicates express constraints that determine which values the variables actually do have.

Sets and types, declarations, and variables

The systems that we need to model might contain vast numbers of things. How can we possibly deal with them all? We gather similar objects into collections and treat each collection as a single object in its own right. These collections are called sets. Sets are central in Z.

Displaying sets

The obvious way to describe a set is to list or enumerate all of its members or elements. This is called a set display. In Z we follow the ordinary mathematical convention and write sets with braces, separating elements by commas. Here is a display of the set of lamps in a traffic light:

Elements in a set are not ordered, so the order you write elements in a set display is not significant. Here is another (equally good) display of the same set:

Sets contain no duplicate elements, and mentioning the same element more than once is redundant but innocuous.