Interface Specifications for Program Modules Supporting Selective Updates and Sharing and their Use in Correctness Proofs

In: G. Sneltinged., Softwaretechnik 95. Available, 1995

Authors

• Arnd Poetzsch-Heffter

Abstract

A new formal specification technique for imperative/object-oriented programs is presented, and its application to program verification is demonstrated. The technique supports the abstract specification of the functional as well as the sharing properties of program modules. In particular, procedures that make selective updates available to clients of modules can be specified in an implementation independent way. Interface specifications of program modules can be used not only for documentation purposes, but as well for formal verification tasks. Therefore, the presented specification technique is designed so that specifications can be directly applied as logical rules in Hoare-style correctness proofs. As an example, we prove the correctness of a sort procedure that exploits selective updates. Finally, implementations of interface specifications are discussed

Full Text

• PDF: specimpro.pdf
• PS.GZ: specimpro.ps.gz

BibTeX

@InProceedings{Poetzsch-Heffter95interface, 
   author = {Arnd Poetzsch-Heffter}
   title = {Interface Specifications for Program Modules Supporting Selective Updates and Sharing and their Use in Correctness Proofs},
   booktitle = {Softwaretechnik 95},
   note = {Available},
   year = {1995},
}