|
Refinement in Z & Object Z
Refinement is one of the cornerstones of the formal approach to software engineering, and its use in various domains has led to research on new applications and generalisation. This book brings together this important research in one volume, with the addition of examples drawn from different application areas. It covers four main themes: data refinement
and its application to Z; generalisations of refinement that change the interface and atomicity of operations; refinement in Object-Z; and modelling state and behaviour by combining Object-Z with CSP. Refinement in Z and Object-Z: Foundations and Advanced Applications provides an invaluable overview of recent research for academic and industrial researchers, lecturers teaching formal specification and development, industrial practitioners using formal methods in their work, and postgraduate and advanced undergraduate students.
Contents:
Preface I: Refining Z Specifications:1
An Introduction to Z2
Simple Refinement3
Data Refinement and Simulations4
Refinement in Z5
Calculating Refinements6
Promotion7
Testing and Refinement8
A Single Simulation RuleII
Interfaces and Operations - ADTs Viewed in an Environment:9
Refinement, Observation and Modification10
IO Refinement11
Weak Refinement12
Non-Atomic Refinement13
Case Study - A Digital and Analog Watch14
Further GeneralisationsIII
Object-Oriented Refinement15
An Introduction to Object-Z16
Refinement in Object-Z17
Class RefinementIV
Modelling State and Behaviour18
Combining CSP and Object-Z19
Refining CSP and Object-Z Specifications20
ConclusionsGlossary.-Bibliography.-Index.
|
