scholarly journals A Modular SOS for Action Notation

1999 ◽  
Vol 6 (56) ◽  
Author(s):  
Peter D. Mosses
Keyword(s):  
Programming Languages ◽  
Operational Semantics ◽  
Denotational Semantics ◽  
Specification Language ◽  
Algebraic Specification ◽  
Recent Proposal ◽  
Structural Operational Semantics ◽  
The Common ◽  
Basic Concepts ◽  
Pragmatic Aspect

Modularity is an important pragmatic aspect of semantic<br />descriptions: good modularity is needed to allow the reuse of existing descriptions when extending or changing the described language. In denotational semantics, the issue of modularity has received much attention, and appropriate abstractions have been introduced, so that definitions of semantic functions may be independent of the details of how computations are modeled. In structural operational semantics (SOS), however, this issue has largely been neglected, and SOS descriptions of programming languages typically exhibit rather poor modularity; the original SOS given for Action Notation (the notation for the semantic entities used in action semantics) suffered from the same problem.<br />This paper recalls a recent proposal, called MSOS, for obtaining a high<br />degree of modularity in SOS, and presents an MSOS description of Action<br />Notation. Due to its modularity, the MSOS description pinpoints some<br />complications in the design of Action Notation, and should facilitate the<br />design of an improved version of the notation. It also provides a major<br />example of the applicability of the MSOS framework.<br />The reader is assumed to be familiar with conventional SOS and with<br />the basic concepts and constructs of Action Notation. The description<br />of Action Notation is formulated almost entirely in Casl, the common<br />algebraic specification language.

scholarly journals On the Action Semantics of Concurrent Programming Languages

1992 ◽  
Vol 21 (424) ◽  
Author(s):  
Peter D. Mosses
Keyword(s):  
Programming Languages ◽  
Operational Semantics ◽  
Denotational Semantics ◽  
Semantic Description ◽  
Paper Briefly ◽  
Action Semantics ◽  
Concurrent Programming Languages ◽  
Structural Operational Semantics ◽  
Bisimulation Equivalence ◽  
Basic Concepts

<p>Action semantics is a framework for semantic description of prograrnming languages. In this framework, actions are semantic entities, used to represent the potential behaviour of programs --- also the contributions that parts of programs make to such behaviour. The notation for expressing actions, called action notation, is combinator-based. It is used in much the same way that lambda-notation is used in denotational semantics. However, the essence of action notation is operational, rather than mathematical, and its meaning is formally defined by a structural operational semantics together with a bisimulation equivalence.</p><p>This paper briefly motivates action semantics, and explains the basic concepts. It then illustrates the use of the framework by giving an action semantic description of a small example language. This language includes a simple form of concurrency: tasks that may synchronize by means of rendezvous. The paper also discusses the operational semantics of action notation, focusing on the primitive actions that represent asynchronous message transmission and process initiation.</p>

scholarly journals On the foundations of final coalgebra semantics: non-well-founded sets, partial orders, metric spaces

1998 ◽  
Vol 8 (5) ◽  
pp. 481-540 ◽  
Author(s):  
DANIELE TURI ◽  
JAN RUTTEN
Keyword(s):  
Computer Science ◽  
Mathematical Theory ◽  
Metric Spaces ◽  
Operational Semantics ◽  
Denotational Semantics ◽  
Partial Orders ◽  
Present Survey ◽  
Induction Principle ◽  
Structural Operational Semantics ◽  
Modern Mathematics

This paper, a revised version of Rutten and Turi (1993), is part of a programme aiming at formulating a mathematical theory of structural operational semantics to complement the established theory of domains and denotational semantics to form a coherent whole (Turi 1996; Turi and Plotkin 1997). The programme is based on a suitable interplay between the induction principle, which pervades modern mathematics, and a dual, non-standard ‘coinduction principle’, which underlies many of the recursive phenomena occurring in computer science.The aim of the present survey is to show that the elementary categorical notion of a final coalgebra is a suitable foundation for such a coinduction principle. The properties of coalgebraic coinduction are studied both at an abstract categorical level and in some specific categories used in semantics, namely categories of non-well-founded sets, partial orders and metric spaces.

Casl — the Common Algebraic Specification Language

2007 ◽  
pp. 241-298 ◽  
Author(s):  
Till Mossakowski ◽  
Anne E. Haxthausen ◽  
Donald Sannella ◽  
Andrezj Tarlecki
Keyword(s):  
Specification Language ◽  
Algebraic Specification ◽  
The Common

scholarly journals Semantics, Modularity, and Rewriting Logic

1998 ◽  
Vol 5 (42) ◽  
Author(s):  
Peter D. Mosses
Keyword(s):  
Operational Semantics ◽  
Denotational Semantics ◽  
Rewriting Logic ◽  
Semantic Description ◽  
Semantic Framework ◽  
Action Semantics ◽  
Strong Indicator ◽  
Hybrid Framework ◽  
Structural Operational Semantics ◽  
Modular Monadic Semantics

A complete formal semantic description of a practical programming language (such as Java) is likely to be a lengthy document, regardless of which semantic framework is being used. Good modularity of the description is important to the person(s) developing it, to facilitate reuse, change, and extension. Unfortunately, the conventional versions<br />of the major semantic frameworks have rather poor modularity.<br /> In this paper, we first recall some approaches that improve the modularity of denotational semantics, namely action semantics, modular monadic semantics, and a hybrid framework that combines these: modular monadic action semantics. We then address the issue of modularity in operational semantics, which appears to have received comparatively little attention so far, and report on some preliminary investigations of how one might achieve the same kind of modularity in structural operational semantics as the use of monad transformers<br />can provide in denotational semantics|this is the main technical contribution of the paper. Finally, we briefly consider the representation of structural operational semantics in rewriting logic, and speculate on the possibility of using it to interpret programs in the described language. Providing powerful meta-tools for such semantics-based interpretation<br />is an interesting potential application of rewriting logic;<br />good modularity of the semantic descriptions may be crucial for the practicality of using the tools.<br />Much of the paper consists of (very) simple examples of semantic descriptions in the various frameworks, illustrating the degree of reformulation needed when extending the described language|a strong indicator of modularity. Throughout, it is assumed that the reader has some familiarity with the concepts and notation of denotational and structural operational semantics. Familiarity with the basic notions of monads and monad transformers is not a prerequisite.

scholarly journals Structural Operational Semantics

1999 ◽  
Vol 6 (30) ◽  
Author(s):  
Luca Aceto ◽  
Willem Jan Fokkink ◽  
Chris Verhoef
Keyword(s):  
Programming Languages ◽  
Operational Semantics ◽  
The Sixties ◽  
Structural Operational Semantics ◽  
High Level

The importance of giving precise semantics to programming and specification<br />languages was recognized since the sixties with the development of the<br />first high-level programming languages (cf. e.g. [30, 206] for some early accounts).<br />The use of operational semantics - i.e. of a semantics that explicitly<br />describes how programs compute in stepwise fashion, and the possible<br />state-transformations they perform - was already advocated by McCarthy<br />in [147], and elaborated upon in references like [142, 143]. Examples of full-blown<br />languages that have been endowed with an operational semantics are<br />Algol 60 [140], PL/I [173], and CSP [178].

scholarly journals CASL: the Common Algebraic Specification Language

2002 ◽  
Vol 286 (2) ◽  
pp. 153-196 ◽  
Author(s):  
Egidio Astesiano ◽  
Michel Bidoit ◽  
Hélène Kirchner ◽  
Bernd Krieg-Brückner ◽  
Peter D. Mosses ◽  
...  
Keyword(s):  
Specification Language ◽  
Algebraic Specification ◽  
The Common

scholarly journals Denotational semantics of recursive types in synthetic guarded domain theory

2018 ◽  
Vol 29 (3) ◽  
pp. 465-510 ◽  
Author(s):  
RASMUS E. MØGELBERG ◽  
MARCO PAVIOTTI
Keyword(s):  
Programming Languages ◽  
Type Theory ◽  
Operational Semantics ◽  
Lambda Calculus ◽  
Denotational Semantics ◽  
Domain Theory ◽  
Logical Relation ◽  
Dependent Type Theory ◽  
Semantics Of Programming Languages ◽  
Dependent Type

Just like any other branch of mathematics, denotational semantics of programming languages should be formalised in type theory, but adapting traditional domain theoretic semantics, as originally formulated in classical set theory to type theory has proven challenging. This paper is part of a project on formulating denotational semantics in type theories with guarded recursion. This should have the benefit of not only giving simpler semantics and proofs of properties such as adequacy, but also hopefully in the future to scale to languages with advanced features, such as general references, outside the reach of traditional domain theoretic techniques.Working inGuarded Dependent Type Theory(GDTT), we develop denotational semantics for Fixed Point Calculus (FPC), the simply typed lambda calculus extended with recursive types, modelling the recursive types of FPC using the guarded recursive types ofGDTT. We prove soundness and computational adequacy of the model inGDTTusing a logical relation between syntax and semantics constructed also using guarded recursive types. The denotational semantics is intensional in the sense that it counts the number of unfold-fold reductions needed to compute the value of a term, but we construct a relation relating the denotations of extensionally equal terms, i.e., pairs of terms that compute the same value in a different number of steps. Finally, we show how the denotational semantics of terms can be executed inside type theory and prove that executing the denotation of a boolean term computes the same value as the operational semantics of FPC.

scholarly journals A Modular SOS for ML Concurrency Primitives

1999 ◽  
Vol 6 (57) ◽  
Author(s):  
Peter D. Mosses
Keyword(s):  
Programming Languages ◽  
Functional Programming ◽  
Denotational Semantics ◽  
Modular Approach ◽  
Functional Programming Languages ◽  
Standard Ml ◽  
Pragmatic Aspect ◽  
Transition Rules

Modularity is an important pragmatic aspect of semantic<br />descriptions. In denotational semantics, the issue of modularity has <br />received much attention, and appropriate abstractions have been <br />introduced, so that definitions of semantic functions may be independent of<br />the details of how computations are modeled. In structural operational<br />semantics (SOS), however, this issue has largely been neglected, and<br />SOS descriptions of programming languages typically exhibit rather poor<br />modularity| - for instance, extending the described language may entail<br />a complete reformulation of the description of the original constructs.<br />A proposal has recently been made for a modular approach to SOS, called<br />MSOS. The basic definitions of the Modular SOS framework are recalled<br />here, but the reader is referred to other papers for a full introduction.<br />This paper focuses on illustrating the applicability of Modular SOS, by<br />using it to give a description of a sublanguage of Concurrent ML (CML);<br />the transition rules for the purely functional constructs do not have to be<br />reformulated at all when adding references and/or processes. The paper<br />concludes by comparing the MSOS description with previous operational<br />descriptions of similar languages.<br />The reader is assumed to be familiar with conventional SOS, with the<br />concepts of functional programming languages such as Standard ML, and<br />with fundamental notions of concurrency.

scholarly journals Categorical model of structural operational semantics for imperative language

2016 ◽  
Vol 40 (2) ◽  
pp. 203-219 ◽  
Author(s):  
William Steingartner ◽  
Valerie Novitzká
Keyword(s):  
Programming Languages ◽  
Operational Semantics ◽  
Mathematical Structure ◽  
Program Behavior ◽  
Elementary Steps ◽  
Categorical Model ◽  
Structural Operational Semantics ◽  
State Changes ◽  
Definition Of ◽  
Graphical Illustration

Definition of programming languages consists of the formal definition of syntax and semantics. One of the most popular semantic methods used in various stages of software engineering is structural operational semantics. It describes program behavior in the form of state changes after execution of elementary steps of program. This feature makes structural operational semantics useful for implementation of programming languages and also for verification purposes. In our paper we present a new approach to structural operational semantics. We model behavior of programs in category of states, where objects are states, an abstraction of computer memory and morphisms model state changes, execution of a program in elementary steps. The advantage of using categorical model is its exact mathematical structure with many useful proved properties and its graphical illustration of program behavior as a path, i.e. a composition of morphisms. Our approach is able to accentuate dynamics of structural operational semantics. For simplicity, we assume that data are intuitively typed. Visualization and facility of our model is not only a new model of structural operational semantics of imperative programming languages but it can also serve for education purposes.

scholarly journals From CML to process Algebras

1993 ◽  
Vol 22 (433) ◽  
Author(s):  
Flemming Nielson ◽  
Hanne Riis Nielson
Keyword(s):  
Programming Languages ◽  
Programming Language ◽  
Process Algebra ◽  
Operational Semantics ◽  
Concurrent Programming ◽  
Process Algebras ◽  
Standard Ml ◽  
Concurrent Programming Languages ◽  
Structural Operational Semantics ◽  
Communication Behaviours

<p>Reppy's language CML extends Standard ML of Milner et al. with primitives for communication. It thus inherits a notion of strong polymorphic typing and may be equipped with a structural operational semantics. We formulate an effect system for statically expressing the communication behaviours of CML programs as these are not otherwise reflected in the types.</p><p>We then show how types and behaviours evolve in the course of computation: types may decrease and behaviours may loose alternatives as well as decrease. It will turn out that the syntax of behaviours is rather similar to that of a process algebra; our main results may therefore be viewed as regarding the semantics of a process algebra as an <em>abstraction</em> of the semantics of an underlying programming language. This establishes a new kind of connection between ''realistic'' concurrent programming languages and ''theoretical'' process algebras.</p>

Sign in / Sign up

Export Citation Format

Share Document