Verification of object-oriented programs: A transformational approach

Krzysztof R. Apt, Frank S. de Boer, Ernst-Rüdiger Olderog, Stijn de Gouw

Research output: Contribution to journalArticleAcademicpeer-review

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.
Original languageEnglish
Pages (from-to)823-852
Number of pages30
JournalJournal of Computer and System Sciences
Volume78
Issue number3
DOIs
Publication statusPublished - May 2012
Externally publishedYes

Fingerprint

Object oriented programming
Object-oriented
Computer programming languages
Recursive Method
Object-oriented Programming
Aliasing
Proof System
Soundness
Assertion
Programming Languages
Completeness
Correctness

Cite this

Apt, Krzysztof R. ; Boer, Frank S. de ; Olderog, Ernst-Rüdiger ; Gouw, Stijn de. / Verification of object-oriented programs : A transformational approach. In: Journal of Computer and System Sciences. 2012 ; Vol. 78, No. 3. pp. 823-852.
@article{a55bc476aaa1432d86fcb11760e64cb6,
title = "Verification of object-oriented programs: A transformational approach",
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.",
author = "Apt, {Krzysztof R.} and Boer, {Frank S. de} and Ernst-R{\"u}diger Olderog and Gouw, {Stijn de}",
year = "2012",
month = "5",
doi = "10.1016/j.jcss.2011.08.002",
language = "English",
volume = "78",
pages = "823--852",
journal = "Journal of Computer and System Sciences",
issn = "0022-0000",
publisher = "Academic Press Inc.",
number = "3",

}

Verification of object-oriented programs : A transformational approach. / Apt, Krzysztof R.; Boer, Frank S. de; Olderog, Ernst-Rüdiger; Gouw, Stijn de.

In: Journal of Computer and System Sciences, Vol. 78, No. 3, 05.2012, p. 823-852.

Research output: Contribution to journalArticleAcademicpeer-review

TY - JOUR

T1 - Verification of object-oriented programs

T2 - A transformational approach

AU - Apt, Krzysztof R.

AU - Boer, Frank S. de

AU - Olderog, Ernst-Rüdiger

AU - Gouw, Stijn de

PY - 2012/5

Y1 - 2012/5

N2 - 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.

AB - 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.

U2 - 10.1016/j.jcss.2011.08.002

DO - 10.1016/j.jcss.2011.08.002

M3 - Article

VL - 78

SP - 823

EP - 852

JO - Journal of Computer and System Sciences

JF - Journal of Computer and System Sciences

SN - 0022-0000

IS - 3

ER -