Refinement Laws for Verifying Library Subroutine Adaptation

C. Fidge, P. Robinson, S. Dunne

Research output: Contribution to conferencePaperpeer-review

145 Downloads (Pure)


In Component-Based Software Engineering programs are constructed from pre-defined software library modules. However, if the library's subroutines do not exactly match the programmer's requirements, the subroutines' code must be adapted accordingly. For this process to be acceptable in safety or mission-critical applications, where all code must be proven correct, it must be possible to verify the correctness of the adaptations themselves. In this paper we show how refinement theory can be used to model typical adaptation steps and to define the conditions that must be proven to verify that a library subroutine has been adapted correctly.
Original languageEnglish
Publication statusPublished - 1 Apr 2005
EventThe Australian Software Engineering Conference 2005 - Brisbane, Australia
Duration: 29 Mar 20051 Apr 2005


ConferenceThe Australian Software Engineering Conference 2005
Abbreviated titleASWEC 2005

Bibliographical note

Author can archive publisher's version/PDF. For full details see [Accessed 30/03/2010]


Dive into the research topics of 'Refinement Laws for Verifying Library Subroutine Adaptation'. Together they form a unique fingerprint.

Cite this