At last we reach code. This chapter shows how to derive code from formulas taken from a Z specification and demonstrate that the code does what the formulas require. Program derivation is the systematic derivation of code from a formal specification. A proof of correctness demonstrates agreement between code and its specification. Such a proof is a by-product of every program derivation. It is also possible to attempt a formal verification to prove the correctness of an already completed block of code.

Almost all code in use today was produced by traditional informal methods, which are based on adapting code from previously solved problems and making modifications guided by programmers' intuitions about what happens when a computer executes a program. Thinking about what happens in the computer is called operational reasoning (in contrast to formal reasoning, which only considers the program text). Operational reasoning is fallible because it requires programmers to imagine how the values of variables evolve through time as execution takes one path or another through the code. For any but the smallest programs, there are far too many variables, values, and paths to consider, so programmers often resort to running their code to see if it behaves as they intend. This is a trial-and-error process, so it can take a great deal of effort to produce an acceptable product.

Formal program derivation proposes a radical alternative: A program is a formula. It can be derived from a specification, and its properties can be checked by calculation.

Z can describe data structures. In this chapter we'll use Z to define the fundamental objects of computer graphics and computational geometry: points, line segments, contours, and polygons.

Consider the distinction between a contour, which is any sequence of connected line segments, and a polygon, which is a closed contour that has an inside and an outside (Figure 19.1). Your eye can see the difference immediately, and the distinction is vital for many computations of great practical importance.

Figure 19.2 is a computer graphic that shows a view of a patient's anatomy and radiation beam geometry, used to plan this patient's radiation treatment for cancer. Cross-sections of anatomical structures must be polygons, not just contours, and the physics calculations that compute the radiation dose depend on this. If some contours are not closed, or cross over themselves, the dose calculations may be incorrect.

The difference between contours and polygons is vital, but there is no way to express this distinction in most programming languages: You have to represent both as mere sequences (arrays or lists) of points. Data types in programming languages correspond closely to the way data are represented in computer memory: If two objects are stored in the same format, they belong to the same data type. Z is far more expressive because we can distinguish data types based on their values and constraints between the values of their components. This enables us to define data types that capture such requirements as “a closed contour that doesn't cross over itself.”

The intention of this chapter is to present a notation for specifying programs to be written later in imperative programming languages such as PASCAL, C, MODULA, ADA, BASIC, or even in assembly code. Put together, the elements of this notation form a very simple pseudo-programming language.

The pseudo-programs that we shall write using this notation will not be executed on a computer nor, a fortiori, be submitted to any kind of tests. Rather, and more importantly, they will be able to be submitted to a mathematical analysis and this will be made possible because each construct of the notation receives a precise axiomatic definition. For doing so, we shall use the technique of the weakest pre-condition as introduced by Dijkstra.

The notation contains a number of constructs that look like the ones encountered in every imperative programming language, namely assignment and conditionals. But it also contains unusual features such as pre-condition, multiple assignment, bounded choice, guard, and even unbounded choice, which are very important for specifying and designing programs although, and probably because, they are not always executable or even implementable.

Although it might seem strange at first glance, the notation does not contain any form of sequencing or loop. Yet the use of such features forms the basis of any decent imperative program. The reason for not having these constructs here is that our problem is not, for the moment, that of writing programs, rather it is that of specifying them: sequencing and loop certainly pertain to the how domain which characterizes programs, but not to the what domain which characterizes specifications.

When doing mathematics, people prove assertions. This is accomplished with the implicit or explicit help of some rules of reasoning admitted, for quite a long time, to be the correct rules of reasoning. Our goal, in this chapter, is to make absolutely precise what such rules are, so that, in principle, if not in practice, the activity of proving could be made checkable by a robot.

The reason why we insist, in this first chapter, on the very precise definition of what mathematical reasoning is, must be clear. Our eventual aim is to have a significant part of software systems constructed in a way that is guaranteed by proofs. Most of the time such proofs are, mathematically speaking, not very deep; however, there will be many of them. Hence, it will be quite easy to introduce errors in doing them, in very much the same way as people introduce errors in writing programs. There is, clearly, no gain in just shifting the production of errors from programs to proofs. Fortunately, however, there exists an important distinction between programs and proofs. Both are formal texts, but, provided the foundation for proofs is sufficiently elaborate (hence this chapter), then proofs can always be checked mechanically for correctness, whereas programs cannot.

This chapter is organized as follows. In the first section, we introduce the way mathematical conjectures are presented and the way such conjectures can be eventually proved. This is done independently of any precise mathematical domain.

This book is a very long discourse explaining how, in my opinion, the task of programming (in the small as well as in the large) can be accomplished by returning to mathematics.

By this, I first mean that the precise mathematical definition of what a program does must be present at the origin of its construction. If such a definition is lacking, or if it is too complicated, we might wonder whether our future program will mean anything at all. My belief is that a program, in the absolute, means absolutely nothing. A program only means something relative to a certain intention, that must predate it, in one form or another. At this point, I have no objection with people feeling more comfortable with the word “English” replacing the word “mathematics”. I just wonder whether such people are not assigning themselves a more difficult task.

I also think that this “return to mathematics” should be present in the very process of program construction. Here the task is to assign a program to a well-defined meaning. The idea is to accompany the technical process of program construction by a similar process of proof construction, which guarantees that the proposed program agrees with its intended meaning.

Simultaneous concerns about the architecture of a program and that of its proof are surprisingly efficient. For instance, when the proof is cumbersome, there are serious chances that the program will be too; and ingredients for structuring proofs (abstraction, instantiation, decomposition) are very similar to those for structuring programs.

This chapter is devoted to the study of various theoretical developments concerning Generalized Substitutions and Abstract Machines. Our ultimate goal is to construct some set-theoretic models for Abstract Machines and Generalized Substitutions. By doing so, we shall be able to conduct further developments of Abstract Machines (i.e. loop and refinement in chapters 9 and 11 respectively) on these models rather than on the notation itself. This will prove to be very convenient.

In section 6.1, we prove that any generalized substitution defined in terms of the basic constructs of the previous chapter can be put into a certain normalized form. An outcome of this result is that any proof involving a generalized substitution can be done by assuming, without any loss of generality, that the substitution in question is in normalized form.

In section 6.2, we prove two convenient properties of generalized substitutions: namely, that the establishment of a post-condition distributes through conjunction and that it is monotonic under universal implication. The first will have a clear practical impact whereas the second is useful for theoretical developments. These properties were named by E.W. Dijkstra the Healthiness Conditions.

In section 6.3, we study the problem of termination and that of feasibility. We give a simple characterization of these properties. We also explain how the Generalized Substitution Language has exactly the same expressive power as the Before-after Predicates as introduced in section 4.4.

In this chapter our intention is to present three large examples of abstract machines. In each of them, we would like to put the emphasis on a particular aspect of specifying.

The goal of the first example, the Invoice System, is to show how to build the technical specification of a data processing system in an incremental fashion. Another important aspect is that of defining how the errors can be trapped in a systematic way. Here, clearly, the intention is to build abstract machines whose operations are viewed as a “repertoire of instructions” for building further machines on top of them, and so on.

The second example (inspired by) is a Telephone Exchange System. The goal here is to show how the concept of abstract machine can be used to model a system where “concurrent” activities take place. The machine we shall specify is intended to be an abstract model of the entire activity of a telephone exchange, where all the telephone conversations are handled simultaneously. Clearly, the mental image of the operations of such a machine does not correspond to “buttons” that can be pressed or to “instructions” that can be invoked. The idea is rather to consider that the operations are events that may occur for some reason. The pre-conditions of such operations are then viewed as the “firing conditions” of such events. In a first approximation, the “real” reason for the occurence of such events, once the firing conditions are met, are not our concerns. Sometimes, it can be the consequence of physical events like someone lifting a telephone hand-set. Sometimes, it is rather a “spontaneous” decision of the system.