0
$\begingroup$

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?

$\endgroup$

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.