home > book reviews > Gordon A. Rose
Google > Gordon A. Rose


Books

Short works

Books : reviews

Roger Duke, Gordon A. Rose.
Formal Object-oriented Specification Using Object-Z.
Macmillan. 2000

(read but not reviewed)

Software systems have become complex and critical for safety, reliability and economic reasons. An appreciation of the techniques for the rigorous description of such systems is therefore essential for emerging graduates in the field of software development. Imprecise or misunderstood description leads to unexpected or erroneous functionality of behaviour with high implicit costs for rectification.

Formal Object-Oriented Specification Using Object-Z focuses on the key role of formal specification in software or system development and advocates object-oriented structuring of specifications for clarity, modularity and ease of conversion to object-oriented programming languages. The formal specification used is Object Z, an object-oriented extension of the Oxford formal specification language Z.

Numerous and varied case studies illustrate formal specification techniques and language and the key role of specification in verification (proofs of correctness) and in implementation. Formal Object-Oriented Specification Using Object-Z illustrates various stylistic and architectural approaches, the integration of graphical techniques with formal specification, and includes the syntax of Object-Z, a glossary of its symbolism and selected examples of its semantics,