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.
|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|
|Publication status||Published - 8 Feb 1996|
|Name||Lecture Notes in Computer Science|