Java Jr: Fully Abstract Trace Semantics for a Core Java Language

: Fully abstract trace semantics for a core Java language. Alan Jeffrey 1,2 and Julian Rathke3 1 Bell Labs, Lucent Technologies, Chicago, IL, USA 2 DePaul University, Chicago, IL, USA 3 University of Sussex, Brighton, UK Abstract. We introduce an expressive yet semantically clean core Java-like language, Java Jr., and provide it with a formal operational semantics based on traces of observable actions which represent interaction across package boundaries. A detailed example based on the Observer Pattern is used to demonstrate the intuitive character of the semantic model. We also show that our semantic trace equivs fully-abstract with respect to a natural notion of testing equivalence for object systems. This is the first such result for a full class-based OO-language with inheritance.

• Type: Conference
• Year: 2005
• Where: ESOP
• Authors: Alan Jeffrey, Julian Rathke
• Keywords: Abstract Trace Semantics, Core Java Language, ESOP 2005, Programming Languages, Semantic