Modular Structural Operational Semantics with Strategies ⋆ Abstract

Strategies are a powerful mechanism to control rule application in rule-based systems. For instance, different transition relations can be defined and then combined by means of strategies, giving rise to an effective tool to define the semantics of programming languages. We have endowed the Maude MSOS Tool (MMT), an executable environment for modular structural operational semantics, with the possibility of defining strategies over its transition rules, by combining MMT with the Maude strategy language interpreter prototype. The combination was possible due to Maude’s reflective capabilities. One possible use of MMT with strategies is to execute Ordered SOS specifications. We show how a particular form of strategy can be defined to represent an OSOS order and therefore execute, for instance, SOS specifications with negative premises. In this context, we also discuss how two known techniques for the representation of negative premises in OSOS become simplified in our setting