# Object-oriented small-step semantics NOT based on rewriting techniques

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 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 ;.