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 proceedingConference contributionAcademicpeer-review

    4 Citations (Scopus)
    70 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 languageEnglish
    Title of host publicationFME'96: Industrial Benefit and Advances in Formal Methods
    Subtitle of host publicationThird International Symposium of Formal Methods Europe Co-Sponsored by IFIP WG 14.3 Oxford, UK, March 18–22, 1996 Proceedings
    EditorsMarie-Claude Gaudel, James Woodcock
    Place of PublicationBerlin
    PublisherSpringer
    Pages595-608
    ISBN (Electronic)978-3-540-49749-3
    ISBN (Print)978-3-540-60973-5
    DOIs
    Publication statusPublished - 8 Feb 1996

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer
    Volume1051
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349

    Keywords

    • METIS-119248

    Cite this