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 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 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 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>

scholarly journals Constructive Action Semantics for Core ML

2004 ◽  
Vol 11 (37) ◽  
Author(s):  
Jørgen Iversen ◽  
Peter D. Mosses
Keyword(s):  
Programming Languages ◽  
Tool Support ◽  
Semantic Description ◽  
Action Semantics ◽  
Language Constructs ◽  
Description Framework ◽  
The Individual ◽  
Language Construct ◽  
Language Description

Usually, the majority of language constructs found in a programming language can also be found in many other languages, because language design is based on reuse. This should be reflected in the way we give semantics to programming languages. It can be achieved by making a language description consist of a collection of modules, each defining a single language construct. The description of a single language construct should be language independent, so that it can be reused in other descriptions without any changes. We call a language description framework ``constructive'' when it supports independent description of individual constructs.<br /> <br />We present a case study in constructive semantic description. The case study is a description of Core ML, consisting of a mapping from it to BAS (Basic Abstract Syntax) and action semantic descriptions of the individual BAS constructs. The latter are written in ASDF (Action Semantics Definition Formalism), a formalism specially designed for writing action semantic descriptions of single language constructs. Tool support is provided by the ASF+SDF Meta-Environment and by the Action Environment, which is a new extension of the ASF+SDF Meta-Environment.

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.

scholarly journals The Potential Use of Action Semantics in Standards

1986 ◽  
Vol 15 (206) ◽  
Author(s):  
Peter D. Mosses ◽  
David A. Watt
Keyword(s):  
Programming Languages ◽  
Denotational Semantics ◽  
Formal Semantic ◽  
Action Semantics ◽  
Potential Use ◽  
Current Standards

Current standards for programming languages generally use informal, rather than formal, semantic descriptions. Possible reasons for this are discussed. Action Semantics, which has been developed from Denotational Semantics and Abstract Semantic Algebras, has some features that may make it more attractive for use in standards than other formal approaches. This paper describes and motivates Action Semantics, and gives some realistic examples of its use.

Domain equations for probabilistic processes

2000 ◽  
Vol 10 (6) ◽  
pp. 665-717 ◽  
Author(s):  
CHRISTEL BAIER ◽  
MARTA KWIATKOWSKA
Keyword(s):  
Metric Spaces ◽  
Operational Semantics ◽  
Denotational Semantics ◽  
Semantic Model ◽  
Transition Systems ◽  
Probabilistic Choice ◽  
Bisimulation Equivalence ◽  
Metric Semantics ◽  
Continuous Domains ◽  
Probabilistic Processes

In this paper we consider Milner's calculus CCS enriched by a probabilistic choice operator. The calculus is given operational semantics based on probabilistic transition systems. We define operational notions of preorder and equivalence as probabilistic extensions of the simulation preorder and the bisimulation equivalence respectively. We extend existing category-theoretic techniques for solving domain equations to the probabilistic case and give two denotational semantics for the calculus. The first, ‘smooth’, semantic model arises as a solution of a domain equation involving the probabilistic powerdomain and solved in the category CONT⊥ of continuous domains. The second model also involves an appropriately restricted probabilistic powerdomain, but is constructed in the category CUM of complete ultra-metric spaces, and hence is necessarily ‘discrete’. We show that the domain-theoretic semantics is fully abstract with respect to the simulation preorder, and that the metric semantics is fully abstract with respect to bisimulation.

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 The Use of Action Semantics

1986 ◽  
Vol 15 (217) ◽  
Author(s):  
Peter D. Mosses ◽  
David A. Watt
Keyword(s):  
Programming Languages ◽  
Denotational Semantics ◽  
Action Semantics ◽  
State Of Affairs ◽  
Current Standards

Formal descriptions of semantics have so far failed to match the acceptance and popularity of formal descriptions of syntax. Thus, in current standards for programming languages, syntax is usually described formally but semantics informally, despite the greater danger of impreciseness in the description of semantics. Possible reasons for this state of affairs are discussed. Action Semantics, which has been developed from Denotational Semantics and Abstract Semantic Algebras, has some features that may make it more attractive than other semantic formalisms. This paper describes and motivates Action Semantics, and gives some realistic examples of its use.

Sign in / Sign up

Export Citation Format

Share Document