Applications and Methodology of ?Z

In this chapter, we describe a specification logic called ?Z. This is a Z-like formal method in which specifications are theories, not simply definitions. We examine simple applications and discuss some methodological issues that these illustrate. The chapter is introductory, and should be comprehensible to a reader with a knowledge of predicate logic and some familiarity with the ideas of computer system specification