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?


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.