university website

K.R. Apt (Krzysztof), F.S. de Boer (Frank), E.R. Olderog (Ernst-Rüdiger) and C.P.T. de Gouw (Stijn)

2011-08-01

Verification of object-oriented programs: A transformational approach

Publication

Publication

Journal of Computer and System Sciences

We present proof systems for (strong) partial correctness of object-oriented programs. We show relative completeness of the systems by transformation to recursive programs. The transformation preserves semantics, correctness, and proofs in a homomorphic way. The completeness result considers programs with variables over abstract data types. The transformational approach carries over to inheritance and subtype polymorphism.
Additional Metadata
Keywords Object-oriented programs, Null references, Aliasing, Inheritance, Subtyping, Syntax-directed transformation, Recursive programs, Program verification, Strong partial correctness, Relative completeness
THEME Logistics (theme 3), Software (theme 1)
Publisher Elsevier
Journal Journal of Computer and System Sciences
Organisation Networks and Optimization
Citation
Apt, K., de Boer, F., Olderog, E.-R., & de Gouw, S. (2011). Verification of object-oriented programs: A transformational approach. Journal of Computer and System Sciences.
Full Text ( Final Version , 341kb ) cover


User Publication Person Organisation Collection
Close