Specification and Verification of Object-Oriented Programs

Habilitation thesis, Technical University of Munich, Available, January, 1997

Authors

• Arnd Poetzsch-Heffter

Abstract

"Interface specifications should express program properties in a formal, declarative, and implementation-independent way. To achieve implementation-independency, interface specifications have to support data abstraction. Program verification should enable to prove implementations correct w.r.t. such interface specifications. The presented work bridges the gap between existing specification and verification techniques for object-oriented programs. The integration is done within a formal framework for interface specifications and programming language semantics. Interface specification techniques are enhanced to support the specification of data structure sharing and destructive updating of shared variables. These extensions are necessary for the specification of real life software libraries. Moreover this generalization is needed for intermediate steps in correctness proofs. For verification, Hoare logic is extended to capture recursive classes and subtyping. Based on this extended logic, techniques are presented for proving typing properties, class and method invariants. The new techniques are developed as a foundation for programming environments supporting specification and verification of programs. A major application will be the specification and verification of reusable class libraries. That is one of the reasons why the work focuses on object-oriented languages, even though the techniques are applicable to other imperative languages as well."

Full Text

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

BibTeX

@PhDThesis{Poetzsch-Heffter97specification, 
   author = {Arnd Poetzsch-Heffter}
   title = {Specification and Verification of Object-Oriented Programs},
   school = {Habilitation thesis, Technical University of Munich},
   note = {Available},
   month = {January},
   year = {1997},
}