Data refinement refined

J. He; C. A.R. Hoare; J. W. Sanders

doi:10.1007/3-540-16442-1_14

Data refinement refined

J. He, C. A.R. Hoare, J. W. Sanders

University of Oxford

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

73 Scopus citations

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.

Original language	English
Title of host publication	ESOP 86 - European Symposium on Programming, Proceedings
Editors	Reinhard Wilhelm, Bernard Robinet
Publisher	Springer Verlag
Pages	187-196
Number of pages	10
ISBN (Print)	9783540164425
DOIs	https://doi.org/10.1007/3-540-16442-1_14
State	Published - 1986
Externally published	Yes
Event	European Symposium on Programming, ESOP 1986 - Saarbrucken, Germany Duration: 17 Mar 1986 → 19 Mar 1986

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	213 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	European Symposium on Programming, ESOP 1986
Country/Territory	Germany
City	Saarbrucken
Period	17/03/86 → 19/03/86

Access to Document

10.1007/3-540-16442-1_14

Cite this

He, J., Hoare, C. A. R., & Sanders, J. W. (1986). Data refinement refined. In R. Wilhelm, & B. Robinet (Eds.), ESOP 86 - European Symposium on Programming, Proceedings (pp. 187-196). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 213 LNCS). Springer Verlag. https://doi.org/10.1007/3-540-16442-1_14

@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.\}",

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 = "德国",

}

He, J, Hoare, CAR & Sanders, JW 1986, Data refinement refined. in R Wilhelm & B Robinet (eds), ESOP 86 - European Symposium on Programming, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 213 LNCS, Springer Verlag, pp. 187-196, European Symposium on Programming, ESOP 1986, Saarbrucken, Germany, 17/03/86. https://doi.org/10.1007/3-540-16442-1_14

Data refinement refined. / He, J.; Hoare, C. A.R.; Sanders, J. W.
ESOP 86 - European Symposium on Programming, Proceedings. ed. / Reinhard Wilhelm; Bernard Robinet. Springer Verlag, 1986. p. 187-196 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 213 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Data refinement refined

AU - He, J.

AU - Hoare, C. A.R.

AU - Sanders, J. W.

PY - 1986

Y1 - 1986

N2 - 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.

AB - 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.

UR - https://www.scopus.com/pages/publications/85034864446

U2 - 10.1007/3-540-16442-1_14

DO - 10.1007/3-540-16442-1_14

M3 - 会议稿件

AN - SCOPUS:85034864446

SN - 9783540164425

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 187

EP - 196

BT - ESOP 86 - European Symposium on Programming, Proceedings

A2 - Wilhelm, Reinhard

A2 - Robinet, Bernard

PB - Springer Verlag

T2 - European Symposium on Programming, ESOP 1986

Y2 - 17 March 1986 through 19 March 1986

ER -

Data refinement refined

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this