Dynamic Structural Operational Semantics (preliminary version)

Abstract

We introduce Dynamic SOS as a framework for describing semantics of programming languages that include dynamic software upgrades. Dynamic SOS is built on top of theModular SOS of P.Mosses, with an underlying category theory formalization. Dynamic SOS wants to bring out the essential differences between dynamic upgrade constructs and execution constructs. The important feature of Modular SOS that we exploit in our framework is the sharp separation of the program code from the additional data structures needed at run-time. We exemplify Dynamic SOS on the C-like Proteus language and the concurrent object-oriented Creol language. On the way we introduce a construction onModular SOS useful in the setting of the concurrent objects of Creol, where the executing code is running inside the object. This “encapsulating construction” may be used in any situation where a form of encapsulation of the execution is needed.