A graph-based operational semantics of OO programs

Wei Ke, Zhiming Liu, Shuling Wang, Liang Zhao

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

11 Citations (Scopus)

Abstract

We present a mathematical model of class graphs, object graphs and state graphs which naturally capture the essential oo features. A small-step operational semantics of oo programs is defined in the style of classical structural operational semantics, in which an execution step of a command is defined as a transition from one state graph to another obtained by simple operations on graphs. To validate this semantics, we give it an implementation in Java. This implementation can also be used for simulation and validation of oo programs, with the visualization of state graph transitions during the execution. A distinct feature of this semantics is location or address independent. Properties of objects and oo programs can be described as properties of graphs in terms of relations of navigation paths (or attribute strings).

Original languageEnglish
Title of host publicationFormal Methods and Software Engineering - 11th International Conference on Formal Engineering Methods, ICFEM 2009, Proceedings
Pages347-366
Number of pages20
DOIs
Publication statusPublished - 2009
Event11th International Conference on Formal Engineering Methods, ICFEM 2009 - Rio de Janeiro, Brazil
Duration: 9 Dec 200912 Dec 2009

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume5885 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference11th International Conference on Formal Engineering Methods, ICFEM 2009
Country/TerritoryBrazil
CityRio de Janeiro
Period9/12/0912/12/09

Keywords

  • OO programs
  • Object graphs
  • Operational semantics
  • State graphs

Fingerprint

Dive into the research topics of 'A graph-based operational semantics of OO programs'. Together they form a unique fingerprint.

Cite this