Homepage>Publikationen>PublikationsDetail

Interactive Verification Environments for Object-Oriented Languages

In: Journal of Universal Computer Science. volume 5, number 3, p. 208--225, Available, 1999

Authors

Jörg Meyer
Arnd Poetzsch-Heffter

Abstract

Formal specification and verification techniques can improve the quality of object-oriented software by enabling semantic checks and certification of properties. To be applicable to object-oriented programs, they have to cope with subtyping, aliasing via object references, as well as abstract and recursive methods. For mastering the resulting complexity, mechanical aid is needed. The article outlines the specific technical requirements for the specification and verification of object-oriented programs. Based on these requirements, it argues that verification of OO-programs should be done interactively and develops an modular architecture for this task. In particular, it shows how to integrate interactive program verification with existing universal interactive theorem provers, and explains the new developed parts of the architecture. To underline the general approach, we describe interesting features of our prototype implementation.

Full Text

PDF: jucs99.pdf
PS.GZ: jucs99.ps.gz

BibTeX

@Article{Meyer.Poetzsch-Heffter99interactive, 
   author = {Jörg Meyer and Arnd Poetzsch-Heffter}
   title = {Interactive Verification Environments for Object-Oriented Languages},
   journal = {Journal of Universal Computer Science},
   number = {3},
   pages = {208--225},
   note = {Available},
   year = {1999},
}

Einloggen