Structured Operational Semantics (SOS) is a popular method for defining semantics by means of transition rules. An important feature of SOS rules is negative premises, which are crucial in the definitions of such phenomena as priority mechanisms and time-outs. However, the inclusion of negative premises in SOS rules also introduces doubts as to the preferred meaning of SOS specifications.
Orderings on SOS rules were proposed by Phillips and Ulidowski as an alternative to negative premises. Apart from the definition of the semantics of positive GSOS rules with orderings, the meaning of more general types of SOS rules with orderings has not been studied hitherto. This paper presents several candidates for the meaning of general SOS rules with orderings and discusses their conformance to our intuition for such rules.
We take two general frameworks (rule formats) for SOS with negative premises and SOS with orderings, and present semantics-preserving translations between them with respect to our preferred notion of semantics. Thanks to our semantics-preserving translation, we take existing congruence meta-results for strong bisimilarity from the setting of SOS with negative premises into the setting of SOS with orderings. We further compare the expressiveness of rule formats for SOS with orderings and SOS with negative premises. The paper contains also many examples that illustrate the benefits of SOS with orderings and the properties of the presented definitions of meaning.
While studying the specification of the operational semantics of different programming languages and formalisms, one can observe the following three facts. First, Plotkin's style of Structural Operational Semantics has become a standard in defining operational semantics. Second, congruence with respect to some notion of bisimilarity is an interesting property for such languages and it is essential in reasoning. Third, there are numerous languages that contain an explicit data part in the state of the operational semantics. The first two facts have resulted in a line of research exploring syntactic formats of operational rules to derive the desired congruence property for free. However, the third point (in combination with the first two) is not sufficiently addressed and there is no standard congruence format for operational semantics with an explicit data state. In this article, we address this problem by studying the implications of the presence of a data state on the notion of bisimilarity. Furthermore, we propose a number of formats for congruence. © 2005 Elsevier Inc. All rights reserved.