I am looking for a formalized (imperative and possibly statement based) small-step semantics of a subset of an object oriented programming language that it is not based on rewriting techniques.
(e.g., the statement
x = 5 + y; should be computed in a single step, similarly to Nielson and Nielson SOS semantics).
In my research I read about:
- K-Java: the formalization of Java 1.4 with the K-Framework. It is based on rewriting techniques.
- Featherweight Java (FJ): it is expression-based and based on rewriting of expressions
- Middleweight Java (MJ): it looks promising because it is statement-based, but the expressions are computed with rewriting techniques.
In particular I would like to know how to treat object creation and method call cases, which are "promotable expressions" (c.f., MJ), i.e., expressions that can be promoted to a statement by appending a
Are there other small-step semantics with the desired characteristics?