Verification of object-oriented programs: A transformational approach
The work
| Authors | Krzysztof R. Apt; Frank S. de Boer; Ernst-Rüdiger Olderog; Stijn de Gouw |
|---|---|
| Editors | |
| Type | article |
| Year | 2012 |
| Citekey | apt2012verification |
Where it appeared
| Published in | Journal of Computer and System Sciences |
|---|---|
| Volume | 78 |
| Issue | 3 |
| Pages | 823--852 |
Identifiers
| DOI | 10.1016/j.jcss.2011.08.002 |
|---|
Abstract
We show that verification of object-oriented programs by means of the assertional method can be achieved in a simple way by exploiting a syntax-directed transformation from object-oriented programs to recursive programs. This transformation suggests natural proofs rules and its correctness helps us to establish soundness and relative completeness of the proposed proof system. One of the difficulties is how to properly deal in the assertion language with the instance variables and aliasing. The discussed programming language supports arrays, instance variables, failures and recursive methods with parameters. We also explain how the transformational approach can be extended to deal with other features of object-oriented programming, like classes, inheritance, subtyping and dynamic binding.
Cite it as
@article{apt2012verification,
title = {Verification of object-oriented programs: A transformational approach},
author = {Krzysztof R. Apt and Frank S. de Boer and Ernst-Rüdiger Olderog and Stijn de Gouw},
year = {2012},
journal = {Journal of Computer and System Sciences},
volume = {78},
number = {3},
pages = {823--852},
doi = {10.1016/j.jcss.2011.08.002},
}
This record lives at https://refs.drheap.org/apt2012verification/ and will keep doing so.