Case Study: A Digital and Analogue Watch
The MD of our local watch manufacturer has decided to use Z to describe the functionality of the latest watches in production. Given an initial abstract specification there are a number of possible implementations, and in this chapter we use a collection of different refinement techniques to verify that the implementations are correct with respect to the initial design.
Unable to display preview. Download preview PDF.