Paper Info
Title
True small-step reduction for imperative object oriented languages
Abstract
Traditionally, formal semantic models of Java-like languages use an explicit model of the store which mimics pointers and ram. These low level models hamper understanding of the semantics, and development of proofs about ownerships and other encapsulation properties, since the real (graph) structure of the data is obscured by the encoding. Such models are also inadequate for didactic purposes since they rely on run-time structures that do not exist in the source program --- in order to understand the meaning of an expression in the middle of the execution one is required to visualize the memory structure which is hard to relate to the abstract program state. We present a semantic model for Java-like languages where data is encoded as part of the program rather than as a separate resource. This means that execution can be modelled more simply by just rewriting source code terms, as in semantic models for functional programs. The major challenges that need to be addressed are aliasing, circular object graphs, exceptions and multiple return methods. In this initial proposal we use local variable declarations in order to tackle aliasing and circular object graphs.
Year
DOI
Venue
2013
10.1145/2489804.2489805
FTfJP@ECOOP
Field
DocType
Citations 
Pointer (computer programming),Programming language,Object-oriented programming,Computer science,Source code,Imperative programming,Theoretical computer science,Rewriting,Local variable,Semantics,Semantic data model
Conference
3
PageRank 
References 
Authors
0.41
10
2
Name
Order
Citations
PageRank
Marco Servetto16111.51
Lindsay Groves238826.10