An operational semantics for object-oriented concepts based on the class hierarchy

Colvin, Robert (2013) An operational semantics for object-oriented concepts based on the class hierarchy. Formal Aspects of Computing, 26 3: 491-535. doi:10.1007/s00165-012-0259-y

Author Colvin, Robert
Title An operational semantics for object-oriented concepts based on the class hierarchy
Journal name Formal Aspects of Computing   Check publisher's open access policy
ISSN 0934-5043
Publication date 2013
Year available 2012
Sub-type Article (original research)
DOI 10.1007/s00165-012-0259-y
Volume 26
Issue 3
Start page 491
End page 535
Total pages 45
Place of publication London, United Kingdom
Publisher Springer
Collection year 2013
Language eng
Abstract The formalisation of object-oriented languages is essential for describing the implementation details of specific programming languages or for developing program verification techniques. However there has been relatively little formalisation work aimed at abstractly describing the fundamental concepts of object-oriented programming, separate from specific language considerations or suitability for a particular verification style. In this paper we address this issue by formalising a language that includes the core object-oriented programming language concepts of field tests and updates, methods, constructors, subclassing, multithreading, and synchronisation, built on top of standard sequential programming constructs. The abstract syntax is relatively close to the core of typical object-oriented programming languages such as Java. A novel aspect of the syntax is that objects and classes are encapsulated within a single syntactic term, including their fields and methods. Furthermore, class terms are structured according to the class hierarchy, and objects appear as subterms of their class (and method instances as subterms of the relevant object). This helps to narrow the gap between how a programmer thinks about their code and the underlying mathematical objects in the semantics. The semantics is defined operationally, so that all actions a program may take, such as testing or setting local variables and fields, or invoking methods on other objects, appear on the labels of the transitions. A process-algebraic style of interprocess communication is used for object and class interactions. A benefit of this label-based approach to the semantics is that a separation of concerns can be made when defining the rules of the different constructs, and the rules tend to be more concise. The basic rules for individual commands may be composed into more powerful rules that operate at the level of classes and objects. The traces generated by the operational semantics are used as the basis for establishing equivalence between classes.
Keyword Operational semantics
Object-oriented programming
Process algebra
Class hierarchy
Q-Index Code C1
Q-Index Status Confirmed Code
Institutional Status UQ
Additional Notes Published online: 21 August 2012

Document type: Journal Article
Sub-type: Article (original research)
Collections: Queensland Brain Institute Publications
Official 2013 Collection
Version Filter Type
Citation counts: TR Web of Science Citation Count  Cited 0 times in Thomson Reuters Web of Science Article
Scopus Citation Count Cited 0 times in Scopus Article
Google Scholar Search Google Scholar
Created: Tue, 06 Nov 2012, 14:54:58 EST by Debra McMurtrie on behalf of Queensland Brain Institute