Modular Completeness: Integrating the reuse of specified software in top-down program development

Job Zwiers; Willem-Paul de Roever; Ulrich Hannemann; Frank Stomp; Yassine Lakhneche

doi:10.1007/3-540-60973-3_109

Modular Completeness: Integrating the reuse of specified software in top-down program development

Job Zwiers, Willem-Paul de Roever, Ulrich Hannemann, Frank Stomp, Yassine Lakhneche

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

4 Citations (Scopus)

149 Downloads (Pure)

Abstract

Reuse of correctly specified software is crucial in bottomup program development. Compositional specification formalisms have been designed to reduce the specification of a syntactically composed construct to specifications of its components, and therefore support topdown development methodology. Thus, the integration of reuse of correctly specified software components in a compositional setting calls for adaptation of a given specification to specifications needed in particular circumstances (depending on their application). Proof systems in which such adaptation steps can be performed whenever they are valid are called modular complete [Z89]. We present a generic way of constructing such systems for sequential and concurrent Hoare logics.

Original language	English
Title of host publication	FME'96: Industrial Benefit and Advances in Formal Methods
Subtitle of host publication	Third International Symposium of Formal Methods Europe Co-Sponsored by IFIP WG 14.3 Oxford, UK, March 18–22, 1996 Proceedings
Editors	Marie-Claude Gaudel, James Woodcock
Place of Publication	Berlin
Publisher	Springer
Pages	595-608
ISBN (Electronic)	978-3-540-49749-3
ISBN (Print)	978-3-540-60973-5
DOIs	https://doi.org/10.1007/3-540-60973-3_109
Publication status	Published - 8 Feb 1996

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	1051
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Keywords

METIS-119248

Access to Document

10.1007/3-540-60973-3_109

Zwiers1996modularFinal published version, 814 KB

Cite this

Zwiers, J., de Roever, W.-P., Hannemann, U., Stomp, F., & Lakhneche, Y. (1996). Modular Completeness: Integrating the reuse of specified software in top-down program development. In M.-C. Gaudel, & J. Woodcock (Eds.), FME'96: Industrial Benefit and Advances in Formal Methods: Third International Symposium of Formal Methods Europe Co-Sponsored by IFIP WG 14.3 Oxford, UK, March 18–22, 1996 Proceedings (pp. 595-608). (Lecture Notes in Computer Science; Vol. 1051). Springer. https://doi.org/10.1007/3-540-60973-3_109

Zwiers, Job ; de Roever, Willem-Paul ; Hannemann, Ulrich et al. / Modular Completeness : Integrating the reuse of specified software in top-down program development. FME'96: Industrial Benefit and Advances in Formal Methods: Third International Symposium of Formal Methods Europe Co-Sponsored by IFIP WG 14.3 Oxford, UK, March 18–22, 1996 Proceedings. editor / Marie-Claude Gaudel ; James Woodcock. Berlin : Springer, 1996. pp. 595-608 (Lecture Notes in Computer Science).

@inproceedings{c03aa469b36b4d4293e9c729023ec480,

title = "Modular Completeness: Integrating the reuse of specified software in top-down program development",

abstract = "Reuse of correctly specified software is crucial in bottomup program development. Compositional specification formalisms have been designed to reduce the specification of a syntactically composed construct to specifications of its components, and therefore support topdown development methodology. Thus, the integration of reuse of correctly specified software components in a compositional setting calls for adaptation of a given specification to specifications needed in particular circumstances (depending on their application). Proof systems in which such adaptation steps can be performed whenever they are valid are called modular complete [Z89]. We present a generic way of constructing such systems for sequential and concurrent Hoare logics.",

keywords = "METIS-119248",

author = "Job Zwiers and {de Roever}, Willem-Paul and Ulrich Hannemann and Frank Stomp and Yassine Lakhneche",

year = "1996",

month = feb,

day = "8",

doi = "10.1007/3-540-60973-3_109",

language = "English",

isbn = "978-3-540-60973-5",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "595--608",

editor = "Marie-Claude Gaudel and James Woodcock",

booktitle = "FME'96: Industrial Benefit and Advances in Formal Methods",

address = "Germany",

}

Zwiers, J, de Roever, W-P, Hannemann, U, Stomp, F & Lakhneche, Y 1996, Modular Completeness: Integrating the reuse of specified software in top-down program development. in M-C Gaudel & J Woodcock (eds), FME'96: Industrial Benefit and Advances in Formal Methods: Third International Symposium of Formal Methods Europe Co-Sponsored by IFIP WG 14.3 Oxford, UK, March 18–22, 1996 Proceedings. Lecture Notes in Computer Science, vol. 1051, Springer, Berlin, pp. 595-608. https://doi.org/10.1007/3-540-60973-3_109

Modular Completeness: Integrating the reuse of specified software in top-down program development. / Zwiers, Job; de Roever, Willem-Paul; Hannemann, Ulrich et al.
FME'96: Industrial Benefit and Advances in Formal Methods: Third International Symposium of Formal Methods Europe Co-Sponsored by IFIP WG 14.3 Oxford, UK, March 18–22, 1996 Proceedings. ed. / Marie-Claude Gaudel; James Woodcock. Berlin: Springer, 1996. p. 595-608 (Lecture Notes in Computer Science; Vol. 1051).

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

TY - GEN

T1 - Modular Completeness

T2 - Integrating the reuse of specified software in top-down program development

AU - Zwiers, Job

AU - de Roever, Willem-Paul

AU - Hannemann, Ulrich

AU - Stomp, Frank

AU - Lakhneche, Yassine

PY - 1996/2/8

Y1 - 1996/2/8

N2 - Reuse of correctly specified software is crucial in bottomup program development. Compositional specification formalisms have been designed to reduce the specification of a syntactically composed construct to specifications of its components, and therefore support topdown development methodology. Thus, the integration of reuse of correctly specified software components in a compositional setting calls for adaptation of a given specification to specifications needed in particular circumstances (depending on their application). Proof systems in which such adaptation steps can be performed whenever they are valid are called modular complete [Z89]. We present a generic way of constructing such systems for sequential and concurrent Hoare logics.

AB - Reuse of correctly specified software is crucial in bottomup program development. Compositional specification formalisms have been designed to reduce the specification of a syntactically composed construct to specifications of its components, and therefore support topdown development methodology. Thus, the integration of reuse of correctly specified software components in a compositional setting calls for adaptation of a given specification to specifications needed in particular circumstances (depending on their application). Proof systems in which such adaptation steps can be performed whenever they are valid are called modular complete [Z89]. We present a generic way of constructing such systems for sequential and concurrent Hoare logics.

KW - METIS-119248

U2 - 10.1007/3-540-60973-3_109

DO - 10.1007/3-540-60973-3_109

M3 - Conference contribution

SN - 978-3-540-60973-5

T3 - Lecture Notes in Computer Science

SP - 595

EP - 608

BT - FME'96: Industrial Benefit and Advances in Formal Methods

A2 - Gaudel, Marie-Claude

A2 - Woodcock, James

PB - Springer

CY - Berlin

ER -

Zwiers J, de Roever WP, Hannemann U, Stomp F, Lakhneche Y. Modular Completeness: Integrating the reuse of specified software in top-down program development. In Gaudel MC, Woodcock J, editors, FME'96: Industrial Benefit and Advances in Formal Methods: Third International Symposium of Formal Methods Europe Co-Sponsored by IFIP WG 14.3 Oxford, UK, March 18–22, 1996 Proceedings. Berlin: Springer. 1996. p. 595-608. (Lecture Notes in Computer Science). doi: 10.1007/3-540-60973-3_109

Modular Completeness: Integrating the reuse of specified software in top-down program development

Abstract

Publication series

Keywords

Access to Document

Fingerprint

Cite this