@inproceedings{ec12dcd4bdb340e29c91ed8fa7dc891a,
title = "Data refinement refined",
abstract = "We consider the original work of Hoare and Jones on data refinement in the light of Dijkstra and Smyth{\textquoteright}s treatment of nondeterminism and of Milner and Park{\textquoteright}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.",
author = "J. He and Hoare, \{C. A.R.\} and Sanders, \{J. W.\}",
note = "Publisher Copyright: {\textcopyright} 1986. Springer Verlag, All rights reserved.; European Symposium on Programming, ESOP 1986 ; Conference date: 17-03-1986 Through 19-03-1986",
year = "1986",
doi = "10.1007/3-540-16442-1\_14",
language = "英语",
isbn = "9783540164425",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "187--196",
editor = "Reinhard Wilhelm and Bernard Robinet",
booktitle = "ESOP 86 - European Symposium on Programming, Proceedings",
address = "德国",
}