[CTTCS 47] Data Refinment. Model-Oriented Proof Methods and parison [Cambridge Tracts in puter Science] (CUP 1998).pdf

Data Refinement:
Model-Oriented Proof Methods and parison
The goal of this book is to provide prehensive and systematic
introduction to the important and highly applicable method of data refine-
ment and the simulation methods used for proving its correctness. The
authors concentrate in the first part on the general principles needed to prove
data refinement correct. They begin with an explanation of the fundamental
notions, showing that data refinement proofs reduce to proving simulation.
The topics of Hoare Logic and the Refinement Calculus are introduced and a
general theory of simulations is developed and related to them. Accessibility
prehension are emphasised in order to guide ers to the area.
The book's second part contains a detailed survey of important methods in
this field, such as VDM, and the methods due to Abadi & Lamport, Hehner,
Lynch and Reynolds, Back's refinement calculus and Z. All these methods
are carefully analysed, and shown to be either plete, with counter-
examples to their application, or to be always applicable whenever data
refinement holds. This is shown by proving, for the first time, that all these
methods can be described and analysed in terms of two simple notions:
forward and backward simulation.
The book is self-contained, going from advanced undergraduate level and
taking the reader to the state of the art in methods for proving simulation.
Willem-Paul de Roever is Professor of Software Technology at the Institute
puter Science and Applied Mathematics, Christian Albrechts
University in Kiel.
Kai Engelhardt is Postdoctoral Research Fellow at the School puting
Science, University of Technology, Sydney.
Cambridge Tracts in puter Science
Editorial Board
S. Abramsky, Department puting Science, University of Edinburgh
P. H. Aczel, Department puter Science, University of Manchester
J. W. de Bakker, Centrum voor Wiskunde en Informatica, Amsterdam
Y. Gurevich, Department of Electrical Eng