Java
Jr: Full abstraction for large scale object systems.
Julian Rathke
Abstract
We propose that operational semantics may be used as an
effective modelling tool even for large scale object systems. In order
to demonstrate this principle we introduce an expressive, yet
semantically clean, core Java-like language, Java Jr. and provide it
with an operational semantics which describes interaction across
package boundaries using labelled transitions. We claim that the trace
semantics generated by these labelled transitions is fully abstract
for a natural notion of may testing for object systems and provide a
detailed example to demonstrate the intuitive character of the
semantic model.