In this chapter we briefly introduce and discuss three more methods. These are Z, Hehner's method, and Back's Refinement Calculus. We do not intend to describe them in as much detail as Reynolds' method and VDM in the previous two chapters. We concentrate just on the data refinement aspects of these methods and analyze quickly how they compare to the methods already discussed.

All three methods discussed in this chapter turn out to be quite different members of the L-simulation community.

Originally Z was invented as another notation for Zermelo-Fränkel set theory. However, it evolved to a development style (or method) for specifications. Although invented by academics, Z is nowadays relatively popular in industry, especially in Europe. As will turn out at the end of our discussion of Z in Section 13.1, there is not much difference between Z and VDM from the data refinement point of view. The subtle differences between these two methods apart from the notational ones are analyzed elsewhere; see e.g. [HJN93].

Hehner arrives at a strikingly simple syntax-based development method by using first order predicate logic as the specification language [Heh93]. Whereas VDM uses two predicates, namely pre- and postconditions, Hehner needs only a single predicate. Moreover he interprets his predicates in a classical twovalued model similar to ours from Section 5.2 for two sets of variables: input and output variables. As we shall see in Section 13.2, Hehner's notion of data transformer corresponds to a total L-simulation relation combined with the solution to the L-simulation problem given in Section 7.2.