Abstract
We consider the original work of Hoare and Jones on data refinement in the light of Dijkstra and Smyth's treatment of nondeterminism and of Milner and Park's definition of the simulation of Communicating Systems. Two proof methods are suggested which we hope are simpler and more general than those in current use. They are proved to be individually sufficient for the correctness of refinement and together necessary for it. The proof methods can be employed to derive the weakest specification of an implementation from its abstract specification.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
E.W. Dijkstra A Discipline of Programming, Prentice-Hall, Englewood Cliffs, N.J., 1976.
H3MS4 Data Refinement Refined, Draft 1, PRG preprint, May, 1985.
He, Jifeng, C.A.R. Hoare and J.W. Sanders Data Refinement Refined, to appear.
C.A.R. Hoare Proof of correctness of data representations, Acta Informatica, 1, 271–281, 1972.
C.A.R. Hoare and He, Jifeng The weakest prespecification, Technical Monograph, PRG-44, June, 1985.
C.B. Jones Software Development: A Rigorous Approach, Prentice-Hall International, Englewood Cliffs, N.J., 1980.
A.J.R.G.Milner Lectures on a calculus for communicating systems, Lecture notes from the International Summer School on Control Flow and Data Flow, Munich, 1984.
T. Nipkow Nondeterministic data types: models and implementations, University of Manchester preprint, March, 1985.
D. Park Concurrency and automata on infinite sequences, in LNCS, 104, 167–183, 1981.
M.B. Smyth Effectively given domains, TCS, 5, 257–274, 1977.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1986 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
He, J., Hoare, C.A.R., Sanders, J.W. (1986). Data refinement refined resume. In: Robinet, B., Wilhelm, R. (eds) ESOP 86. ESOP 1986. Lecture Notes in Computer Science, vol 213. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-16442-1_14
Download citation
DOI: https://doi.org/10.1007/3-540-16442-1_14
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-16442-5
Online ISBN: 978-3-540-39782-3
eBook Packages: Springer Book Archive